Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-rgn.opb |
MD5SUM | e7e8123aa394c0918878e05410d4daeb |
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 | 1236.27 |
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 wulflinc28 THE 2005-09-20 04:37:05 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3390 boxname=wulflinc28 idbench=1046 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: e7e8123aa394c0918878e05410d4daeb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-rgn.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-rgn.opb IDLAUNCH: 3390 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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: 887192 kB Buffers: 25976 kB Cached: 92364 kB SwapCached: 660 kB Active: 33288 kB Inactive: 87552 kB HighTotal: 131008 kB HighFree: 35196 kB LowTotal: 903652 kB LowFree: 851996 kB SwapTotal: 2097640 kB SwapFree: 2096408 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5820 kB Slab: 20892 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:57:15 (client local time) WITH STATUS 10 IN 1208.71 SECONDS stats: 3390 7 1208.71 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/21619/stat): 21619 (minisat+_script) R 21618 21619 20115 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855720588 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/21619/statm): 174 3 169 147 0 27 0 [pid=21619] 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=21620 New process pid=21621 New process pid=21622 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 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 One traced child (pid=21621) exited with status: 0 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=21622) exited with status: 0 One traced child (pid=21620) exited with status: 0 New process pid=21623 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-rgn.opb [startup+10.0029 s] Raw data (loadavg): 0.82 0.93 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 2289 0 0 0 971 11 0 0 25 0 1 0 1855720593 9605120 2218 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 2345 2218 145 145 0 2200 0 [pid=21623] vsize: 9380 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 11504 [startup+20.0046 s] Raw data (loadavg): 0.85 0.93 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 2945 0 0 0 1962 14 0 0 25 0 1 0 1855720593 12386304 2874 4294967295 134512640 135094434 3221224448 3221223120 134555855 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21623/statm): 3024 2874 145 145 0 2879 0 [pid=21623] vsize: 12096 Current children cumulated CPU time (s) 19.77 Current children cumulated vsize (Kb) 14220 [startup+30.0063 s] Raw data (loadavg): 0.87 0.93 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3274 0 0 0 2956 17 0 0 25 0 1 0 1855720593 13709312 3203 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 3347 3203 145 145 0 3202 0 [pid=21623] vsize: 13388 Current children cumulated CPU time (s) 29.74 Current children cumulated vsize (Kb) 15512 [startup+40.007 s] Raw data (loadavg): 0.89 0.93 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3302 0 0 0 3956 17 0 0 25 0 1 0 1855720593 13840384 3231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 3379 3231 145 145 0 3234 0 [pid=21623] vsize: 13516 Current children cumulated CPU time (s) 39.74 Current children cumulated vsize (Kb) 15640 [startup+50.0076 s] Raw data (loadavg): 0.90 0.93 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3361 0 0 0 4956 18 0 0 25 0 1 0 1855720593 14082048 3290 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 3438 3290 145 145 0 3293 0 [pid=21623] vsize: 13752 Current children cumulated CPU time (s) 49.75 Current children cumulated vsize (Kb) 15876 [startup+60.0083 s] Raw data (loadavg): 0.92 0.94 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3647 0 0 0 5953 19 0 0 25 0 1 0 1855720593 15290368 3576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 3733 3576 145 145 0 3588 0 [pid=21623] vsize: 14932 Current children cumulated CPU time (s) 59.73 Current children cumulated vsize (Kb) 17056 [startup+70.01 s] Raw data (loadavg): 0.93 0.94 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3676 0 0 0 6953 19 0 0 25 0 1 0 1855720593 15421440 3605 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 3765 3605 145 145 0 3620 0 [pid=21623] vsize: 15060 Current children cumulated CPU time (s) 69.73 Current children cumulated vsize (Kb) 17184 [startup+80.0107 s] Raw data (loadavg): 0.94 0.94 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4302 0 0 0 7944 22 0 0 25 0 1 0 1855720593 17965056 4231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 4386 4231 145 145 0 4241 0 [pid=21623] vsize: 17544 Current children cumulated CPU time (s) 79.67 Current children cumulated vsize (Kb) 19668 [startup+90.0114 s] Raw data (loadavg): 0.95 0.94 0.90 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4401 0 0 0 8943 23 0 0 25 0 1 0 1855720593 18620416 4330 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 4546 4330 145 145 0 4401 0 [pid=21623] vsize: 18184 Current children cumulated CPU time (s) 89.67 Current children cumulated vsize (Kb) 20308 [startup+100.012 s] Raw data (loadavg): 0.96 0.94 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4425 0 0 0 9943 23 0 0 25 0 1 0 1855720593 18735104 4354 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 4574 4354 145 145 0 4429 0 [pid=21623] vsize: 18296 Current children cumulated CPU time (s) 99.67 Current children cumulated vsize (Kb) 20420 [startup+110.013 s] Raw data (loadavg): 0.96 0.94 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4488 0 0 0 10942 24 0 0 25 0 1 0 1855720593 19030016 4417 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 4646 4417 145 145 0 4501 0 [pid=21623] vsize: 18584 Current children cumulated CPU time (s) 109.67 Current children cumulated vsize (Kb) 20708 [startup+120.013 s] Raw data (loadavg): 0.97 0.94 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4621 0 0 0 11941 24 0 0 25 0 1 0 1855720593 19570688 4550 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 4778 4550 145 145 0 4633 0 [pid=21623] vsize: 19112 Current children cumulated CPU time (s) 119.66 Current children cumulated vsize (Kb) 21236 [startup+130.014 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4622 0 0 0 12942 24 0 0 25 0 1 0 1855720593 19570688 4551 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 4778 4551 145 145 0 4633 0 [pid=21623] vsize: 19112 Current children cumulated CPU time (s) 129.67 Current children cumulated vsize (Kb) 21236 [startup+140.015 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4730 0 0 0 13941 24 0 0 25 0 1 0 1855720593 20070400 4659 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 4900 4659 145 145 0 4755 0 [pid=21623] vsize: 19600 Current children cumulated CPU time (s) 139.66 Current children cumulated vsize (Kb) 21724 [startup+150.015 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5382 0 0 0 14931 30 0 0 25 0 1 0 1855720593 22769664 5311 4294967295 134512640 135094434 3221224448 3221222368 134562749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 5559 5311 145 145 0 5414 0 [pid=21623] vsize: 22236 Current children cumulated CPU time (s) 149.62 Current children cumulated vsize (Kb) 24360 [startup+160.015 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5382 0 0 0 15932 30 0 0 25 0 1 0 1855720593 22769664 5311 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 5559 5311 145 145 0 5414 0 [pid=21623] vsize: 22236 Current children cumulated CPU time (s) 159.63 Current children cumulated vsize (Kb) 24360 [startup+170.016 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5428 0 0 0 16932 30 0 0 25 0 1 0 1855720593 22974464 5357 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 5609 5357 145 145 0 5464 0 [pid=21623] vsize: 22436 Current children cumulated CPU time (s) 169.63 Current children cumulated vsize (Kb) 24560 [startup+180.017 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5516 0 0 0 17931 30 0 0 25 0 1 0 1855720593 23396352 5445 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 5712 5445 145 145 0 5567 0 [pid=21623] vsize: 22848 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 24972 [startup+190.017 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5898 0 0 0 18926 33 0 0 25 0 1 0 1855720593 24907776 5827 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6081 5827 145 145 0 5936 0 [pid=21623] vsize: 24324 Current children cumulated CPU time (s) 189.6 Current children cumulated vsize (Kb) 26448 [startup+200.018 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5899 0 0 0 19926 33 0 0 25 0 1 0 1855720593 24907776 5828 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6081 5828 145 145 0 5936 0 [pid=21623] vsize: 24324 Current children cumulated CPU time (s) 199.6 Current children cumulated vsize (Kb) 26448 [startup+210.019 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5899 0 0 0 20927 33 0 0 25 0 1 0 1855720593 24907776 5828 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6081 5828 145 145 0 5936 0 [pid=21623] vsize: 24324 Current children cumulated CPU time (s) 209.61 Current children cumulated vsize (Kb) 26448 [startup+220.02 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 21927 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221222992 134779266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0 [pid=21623] vsize: 24388 Current children cumulated CPU time (s) 219.61 Current children cumulated vsize (Kb) 26512 [startup+230.021 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 22927 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0 [pid=21623] vsize: 24388 Current children cumulated CPU time (s) 229.61 Current children cumulated vsize (Kb) 26512 [startup+240.021 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 23927 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0 [pid=21623] vsize: 24388 Current children cumulated CPU time (s) 239.61 Current children cumulated vsize (Kb) 26512 [startup+250.021 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 24928 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0 [pid=21623] vsize: 24388 Current children cumulated CPU time (s) 249.62 Current children cumulated vsize (Kb) 26512 [startup+260.022 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 25928 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0 [pid=21623] vsize: 24388 Current children cumulated CPU time (s) 259.62 Current children cumulated vsize (Kb) 26512 [startup+270.023 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6352 0 0 0 26920 37 0 0 25 0 1 0 1855720593 26791936 6281 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6541 6281 145 145 0 6396 0 [pid=21623] vsize: 26164 Current children cumulated CPU time (s) 269.58 Current children cumulated vsize (Kb) 28288 [startup+280.023 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6386 0 0 0 27920 37 0 0 25 0 1 0 1855720593 26955776 6315 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6581 6315 145 145 0 6436 0 [pid=21623] vsize: 26324 Current children cumulated CPU time (s) 279.58 Current children cumulated vsize (Kb) 28448 [startup+290.024 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6447 0 0 0 28921 37 0 0 25 0 1 0 1855720593 27283456 6376 4294967295 134512640 135094434 3221224448 3221223120 134556543 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6661 6376 145 145 0 6516 0 [pid=21623] vsize: 26644 Current children cumulated CPU time (s) 289.59 Current children cumulated vsize (Kb) 28768 [startup+300.025 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6481 0 0 0 29921 37 0 0 25 0 1 0 1855720593 27545600 6410 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6725 6410 145 145 0 6580 0 [pid=21623] vsize: 26900 Current children cumulated CPU time (s) 299.59 Current children cumulated vsize (Kb) 29024 [startup+310.025 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6534 0 0 0 30921 37 0 0 25 0 1 0 1855720593 27807744 6463 4294967295 134512640 135094434 3221224448 3221223120 134556257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6789 6463 145 145 0 6644 0 [pid=21623] vsize: 27156 Current children cumulated CPU time (s) 309.59 Current children cumulated vsize (Kb) 29280 [startup+320.026 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6536 0 0 0 31921 37 0 0 25 0 1 0 1855720593 27807744 6465 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 6789 6465 145 145 0 6644 0 [pid=21623] vsize: 27156 Current children cumulated CPU time (s) 319.59 Current children cumulated vsize (Kb) 29280 [startup+330.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6778 0 0 0 32918 39 0 0 25 0 1 0 1855720593 28794880 6707 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7030 6707 145 145 0 6885 0 [pid=21623] vsize: 28120 Current children cumulated CPU time (s) 329.58 Current children cumulated vsize (Kb) 30244 [startup+340.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6786 0 0 0 33918 39 0 0 25 0 1 0 1855720593 28827648 6715 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7038 6715 145 145 0 6893 0 [pid=21623] vsize: 28152 Current children cumulated CPU time (s) 339.58 Current children cumulated vsize (Kb) 30276 [startup+350.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6794 0 0 0 34919 39 0 0 25 0 1 0 1855720593 28860416 6723 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7046 6723 145 145 0 6901 0 [pid=21623] vsize: 28184 Current children cumulated CPU time (s) 349.59 Current children cumulated vsize (Kb) 30308 [startup+360.029 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 6942 0 0 0 35916 40 0 0 25 0 1 0 1855720593 29474816 6871 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7196 6871 145 145 0 7051 0 [pid=21623] vsize: 28784 Current children cumulated CPU time (s) 359.57 Current children cumulated vsize (Kb) 30908 [startup+370.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7492 0 0 0 36908 43 0 0 25 0 1 0 1855720593 31703040 7421 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7740 7421 145 145 0 7595 0 [pid=21623] vsize: 30960 Current children cumulated CPU time (s) 369.52 Current children cumulated vsize (Kb) 33084 [startup+380.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7492 0 0 0 37909 43 0 0 25 0 1 0 1855720593 31703040 7421 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7740 7421 145 145 0 7595 0 [pid=21623] vsize: 30960 Current children cumulated CPU time (s) 379.53 Current children cumulated vsize (Kb) 33084 [startup+390.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7502 0 0 0 38909 43 0 0 25 0 1 0 1855720593 31768576 7431 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7756 7431 145 145 0 7611 0 [pid=21623] vsize: 31024 Current children cumulated CPU time (s) 389.53 Current children cumulated vsize (Kb) 33148 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7727 0 0 0 39905 45 0 0 25 0 1 0 1855720593 32690176 7656 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 7981 7656 145 145 0 7836 0 [pid=21623] vsize: 31924 Current children cumulated CPU time (s) 399.51 Current children cumulated vsize (Kb) 34048 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 11639 0 0 0 40873 60 0 0 23 0 1 0 1855720593 49553408 11442 4294967295 134512640 135094434 3221224448 3221184220 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/21623/statm): 12098 11442 145 145 0 11953 0 [pid=21623] vsize: 48392 Current children cumulated CPU time (s) 409.34 Current children cumulated vsize (Kb) 50516 [startup+420.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13394 0 0 0 41855 68 0 0 25 0 1 0 1855720593 59834368 13197 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 14608 13197 145 145 0 14463 0 [pid=21623] vsize: 58432 Current children cumulated CPU time (s) 419.24 Current children cumulated vsize (Kb) 60556 [startup+430.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13570 0 0 0 42852 69 0 0 25 0 1 0 1855720593 60555264 13373 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 14784 13373 145 145 0 14639 0 [pid=21623] vsize: 59136 Current children cumulated CPU time (s) 429.22 Current children cumulated vsize (Kb) 61260 [startup+440.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13694 0 0 0 43850 70 0 0 25 0 1 0 1855720593 61059072 13497 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 14907 13497 145 145 0 14762 0 [pid=21623] vsize: 59628 Current children cumulated CPU time (s) 439.21 Current children cumulated vsize (Kb) 61752 [startup+450.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13762 0 0 0 44849 71 0 0 25 0 1 0 1855720593 61341696 13565 4294967295 134512640 135094434 3221224448 3221223072 134557724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 14976 13565 145 145 0 14831 0 [pid=21623] vsize: 59904 Current children cumulated CPU time (s) 449.21 Current children cumulated vsize (Kb) 62028 [startup+460.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13917 0 0 0 45847 71 0 0 25 0 1 0 1855720593 61943808 13720 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 15123 13720 145 145 0 14978 0 [pid=21623] vsize: 60492 Current children cumulated CPU time (s) 459.19 Current children cumulated vsize (Kb) 62616 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 14280 0 0 0 46841 74 0 0 25 0 1 0 1855720593 63430656 14083 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/21623/statm): 15486 14083 145 145 0 15341 0 [pid=21623] vsize: 61944 Current children cumulated CPU time (s) 469.16 Current children cumulated vsize (Kb) 64068 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 14670 0 0 0 47834 77 0 0 25 0 1 0 1855720593 65019904 14473 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 15874 14473 145 145 0 15729 0 [pid=21623] vsize: 63496 Current children cumulated CPU time (s) 479.12 Current children cumulated vsize (Kb) 65620 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 14978 0 0 0 48829 79 0 0 25 0 1 0 1855720593 66281472 14781 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 16182 14781 145 145 0 16037 0 [pid=21623] vsize: 64728 Current children cumulated CPU time (s) 489.09 Current children cumulated vsize (Kb) 66852 [startup+500.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 15219 0 0 0 49825 81 0 0 25 0 1 0 1855720593 67248128 15022 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 16418 15022 145 145 0 16273 0 [pid=21623] vsize: 65672 Current children cumulated CPU time (s) 499.07 Current children cumulated vsize (Kb) 67796 [startup+510.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 15500 0 0 0 50821 83 0 0 25 0 1 0 1855720593 68362240 15303 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 16690 15303 145 145 0 16545 0 [pid=21623] vsize: 66760 Current children cumulated CPU time (s) 509.05 Current children cumulated vsize (Kb) 68884 [startup+520.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 15807 0 0 0 51816 85 0 0 25 0 1 0 1855720593 69632000 15610 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 17000 15610 145 145 0 16855 0 [pid=21623] vsize: 68000 Current children cumulated CPU time (s) 519.02 Current children cumulated vsize (Kb) 70124 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 16605 0 0 0 52802 91 0 0 25 0 1 0 1855720593 72855552 16408 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/21623/statm): 17787 16408 145 145 0 17642 0 [pid=21623] vsize: 71148 Current children cumulated CPU time (s) 528.94 Current children cumulated vsize (Kb) 73272 [startup+540.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17308 0 0 0 53791 95 0 0 25 0 1 0 1855720593 76238848 17111 4294967295 134512640 135094434 3221224448 3221222912 134781066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 18613 17111 145 145 0 18468 0 [pid=21623] vsize: 74452 Current children cumulated CPU time (s) 538.87 Current children cumulated vsize (Kb) 76576 [startup+550.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17442 0 0 0 54789 96 0 0 25 0 1 0 1855720593 76779520 17245 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 18745 17245 145 145 0 18600 0 [pid=21623] vsize: 74980 Current children cumulated CPU time (s) 548.86 Current children cumulated vsize (Kb) 77104 [startup+560.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17651 0 0 0 55785 98 0 0 25 0 1 0 1855720593 77627392 17454 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 18952 17454 145 145 0 18807 0 [pid=21623] vsize: 75808 Current children cumulated CPU time (s) 558.84 Current children cumulated vsize (Kb) 77932 [startup+570.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17912 0 0 0 56782 99 0 0 25 0 1 0 1855720593 78708736 17715 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 19216 17715 145 145 0 19071 0 [pid=21623] vsize: 76864 Current children cumulated CPU time (s) 568.82 Current children cumulated vsize (Kb) 78988 [startup+580.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18337 0 0 0 57775 103 0 0 25 0 1 0 1855720593 80437248 18140 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 19638 18140 145 145 0 19493 0 [pid=21623] vsize: 78552 Current children cumulated CPU time (s) 578.79 Current children cumulated vsize (Kb) 80676 [startup+590.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18475 0 0 0 58773 103 0 0 25 0 1 0 1855720593 80990208 18278 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 19773 18278 145 145 0 19628 0 [pid=21623] vsize: 79092 Current children cumulated CPU time (s) 588.77 Current children cumulated vsize (Kb) 81216 [startup+600.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18715 0 0 0 59769 105 0 0 25 0 1 0 1855720593 81956864 18518 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 20009 18518 145 145 0 19864 0 [pid=21623] vsize: 80036 Current children cumulated CPU time (s) 598.75 Current children cumulated vsize (Kb) 82160 [startup+610.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18859 0 0 0 60766 106 0 0 25 0 1 0 1855720593 82530304 18662 4294967295 134512640 135094434 3221224448 3221223104 134557829 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 20149 18662 145 145 0 20004 0 [pid=21623] vsize: 80596 Current children cumulated CPU time (s) 608.73 Current children cumulated vsize (Kb) 82720 [startup+620.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 19103 0 0 0 61762 107 0 0 25 0 1 0 1855720593 83488768 18906 4294967295 134512640 135094434 3221224448 3221223040 134552168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 20383 18906 145 145 0 20238 0 [pid=21623] vsize: 81532 Current children cumulated CPU time (s) 618.7 Current children cumulated vsize (Kb) 83656 [startup+630.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 19530 0 0 0 62754 111 0 0 25 0 1 0 1855720593 85229568 19333 4294967295 134512640 135094434 3221224448 3221223040 134557263 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 20808 19333 145 145 0 20663 0 [pid=21623] vsize: 83232 Current children cumulated CPU time (s) 628.66 Current children cumulated vsize (Kb) 85356 [startup+640.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 19855 0 0 0 63747 114 0 0 25 0 1 0 1855720593 86544384 19658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21623/statm): 21129 19658 145 145 0 20984 0 [pid=21623] vsize: 84516 Current children cumulated CPU time (s) 638.62 Current children cumulated vsize (Kb) 86640 [startup+650.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 20183 0 0 0 64740 117 0 0 25 0 1 0 1855720593 87859200 19986 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21623/statm): 21450 19986 145 145 0 21305 0 [pid=21623] vsize: 85800 Current children cumulated CPU time (s) 648.58 Current children cumulated vsize (Kb) 87924 [startup+660.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 20452 0 0 0 65734 119 0 0 25 0 1 0 1855720593 88932352 20255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 21712 20255 145 145 0 21567 0 [pid=21623] vsize: 86848 Current children cumulated CPU time (s) 658.54 Current children cumulated vsize (Kb) 88972 [startup+670.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 66731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 668.54 Current children cumulated vsize (Kb) 90708 [startup+680.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 67731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223072 134557660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 678.54 Current children cumulated vsize (Kb) 90708 [startup+690.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 68731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 688.54 Current children cumulated vsize (Kb) 90708 [startup+700.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 69731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 698.54 Current children cumulated vsize (Kb) 90708 [startup+710.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 70731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 708.54 Current children cumulated vsize (Kb) 90708 [startup+720.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 71732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 718.55 Current children cumulated vsize (Kb) 90708 [startup+730.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 72732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 728.55 Current children cumulated vsize (Kb) 90708 [startup+740.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 73732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 738.55 Current children cumulated vsize (Kb) 90708 [startup+750.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 74732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 748.55 Current children cumulated vsize (Kb) 90708 [startup+760.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 75732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 758.55 Current children cumulated vsize (Kb) 90708 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 76733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 768.56 Current children cumulated vsize (Kb) 90708 [startup+780.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 77733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 778.56 Current children cumulated vsize (Kb) 90708 [startup+790.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 78733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 788.56 Current children cumulated vsize (Kb) 90708 [startup+800.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 79733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 798.56 Current children cumulated vsize (Kb) 90708 [startup+810.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21038 0 0 0 80734 122 0 0 25 0 1 0 1855720593 90710016 20676 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20676 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 808.57 Current children cumulated vsize (Kb) 90708 [startup+820.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21038 0 0 0 81734 122 0 0 25 0 1 0 1855720593 90710016 20676 4294967295 134512640 135094434 3221224448 3221223072 134557728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20676 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 818.57 Current children cumulated vsize (Kb) 90708 [startup+830.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 82734 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 828.57 Current children cumulated vsize (Kb) 90708 [startup+840.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 83734 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 838.57 Current children cumulated vsize (Kb) 90708 [startup+850.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 84734 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 848.57 Current children cumulated vsize (Kb) 90708 [startup+860.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 85735 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 858.58 Current children cumulated vsize (Kb) 90708 [startup+870.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 86735 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 868.58 Current children cumulated vsize (Kb) 90708 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 87735 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 878.58 Current children cumulated vsize (Kb) 90708 [startup+890.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 88736 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 888.59 Current children cumulated vsize (Kb) 90708 [startup+900.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 89736 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 898.59 Current children cumulated vsize (Kb) 90708 [startup+910.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 90736 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 908.59 Current children cumulated vsize (Kb) 90708 [startup+920.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 91736 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 918.59 Current children cumulated vsize (Kb) 90708 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 92736 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 928.59 Current children cumulated vsize (Kb) 90708 [startup+940.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 93736 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 938.59 Current children cumulated vsize (Kb) 90708 [startup+950.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 94737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 948.6 Current children cumulated vsize (Kb) 90708 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 95737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 958.6 Current children cumulated vsize (Kb) 90708 [startup+970.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 96737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 968.6 Current children cumulated vsize (Kb) 90708 [startup+980.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 97737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 978.6 Current children cumulated vsize (Kb) 90708 [startup+990.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 98737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 988.6 Current children cumulated vsize (Kb) 90708 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 99738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 998.61 Current children cumulated vsize (Kb) 90708 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 100738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1008.61 Current children cumulated vsize (Kb) 90708 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 101738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1018.61 Current children cumulated vsize (Kb) 90708 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 102738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1028.61 Current children cumulated vsize (Kb) 90708 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 103739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1038.62 Current children cumulated vsize (Kb) 90708 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 104739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1048.62 Current children cumulated vsize (Kb) 90708 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 105739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1058.62 Current children cumulated vsize (Kb) 90708 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 106739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1068.62 Current children cumulated vsize (Kb) 90708 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 107740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1078.63 Current children cumulated vsize (Kb) 90708 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 108740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1088.63 Current children cumulated vsize (Kb) 90708 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 109740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1098.63 Current children cumulated vsize (Kb) 90708 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 110740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1108.63 Current children cumulated vsize (Kb) 90708 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 111740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1118.63 Current children cumulated vsize (Kb) 90708 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 112741 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1128.64 Current children cumulated vsize (Kb) 90708 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 113741 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1138.64 Current children cumulated vsize (Kb) 90708 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 114741 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134561744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1148.64 Current children cumulated vsize (Kb) 90708 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 115742 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1158.65 Current children cumulated vsize (Kb) 90708 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 116742 122 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1168.65 Current children cumulated vsize (Kb) 90708 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 117742 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1178.66 Current children cumulated vsize (Kb) 90708 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 118742 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223040 134557494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1188.66 Current children cumulated vsize (Kb) 90708 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 119742 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1198.66 Current children cumulated vsize (Kb) 90708 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 120743 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1208.67 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.91 2/57 21623 Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21619/statm): 531 226 485 147 0 384 0 [pid=21619] vsize: 2124 Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 120743 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0 [pid=21623] vsize: 88584 Current children cumulated CPU time (s) 1208.67 Current children cumulated vsize (Kb) 90708 Sending SIGTERM to -21619 Sleeping 2 seconds One traced child (pid=21619) ended because it received signal 15 (SIGTERM) One traced child (pid=21623) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1208.71 CPU user time (s): 1207.44 CPU system time (s): 1.27181 CPU usage (%): 99.8817 Max. virtual memory (cumulated for all children) (Kb): 90708
ERROR: no interpretation found !