Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-misc07.opb |
MD5SUM | a3dd3cd7dd293e24bffaff8bb73da54c |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1408128 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 21 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 2097151 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 1048576 |
Number of bits of the biggest number in a constraint | 21 |
Biggest sum of numbers in a constraint | 11486079 |
Number of bits of the biggest sum of numbers | 24 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 280 |
Total number of constraints | 471 |
Number of constraints which are clauses | 127 |
Number of constraints which are cardinality constraints (but not clauses) | 272 |
Number of constraints which are nor clauses,nor cardinality constraints | 72 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 253 |
LAUNCH ON wulflinc17 THE 2005-09-20 03:46:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3304 boxname=wulflinc17 idbench=960 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a3dd3cd7dd293e24bffaff8bb73da54c /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-misc07.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-misc07.opb IDLAUNCH: 3304 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 911408 kB Buffers: 14472 kB Cached: 81164 kB SwapCached: 516 kB Active: 26208 kB Inactive: 71848 kB HighTotal: 131008 kB HighFree: 50204 kB LowTotal: 903652 kB LowFree: 861204 kB SwapTotal: 2097892 kB SwapFree: 2096676 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5664 kB Slab: 19604 kB Committed_AS: 64316 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:06:37 (client local time) WITH STATUS 10 IN 1210.01 SECONDS stats: 3304 7 1210.01 10
c Parsing PB file... c Converting 247 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################### c -- Clauses(.)/Splits(s): ............................................................................................................................... c ---[ 245]---> Adder-cost: 1695 maxlim: 1048703 bits: 22/21 c ---[ 244]---> BDD-cost: 239 c ---[ 233]---> BDD-cost: 239 c ---[ 200]---> Sorter-cost: 127 Base: c ---[ 197]---> Sorter-cost: 127 Base: c ---[ 195]---> Sorter-cost: 127 Base: c ---[ 193]---> Sorter-cost: 127 Base: c ---[ 191]---> Sorter-cost: 127 Base: c ---[ 189]---> Sorter-cost: 127 Base: c ---[ 187]---> Sorter-cost: 127 Base: c ---[ 185]---> Sorter-cost: 127 Base: c ---[ 183]---> Sorter-cost: 127 Base: c ---[ 181]---> Sorter-cost: 127 Base: c ---[ 179]---> Sorter-cost: 127 Base: c ---[ 176]---> Sorter-cost: 127 Base: c ---[ 174]---> Sorter-cost: 127 Base: c ---[ 172]---> Sorter-cost: 127 Base: c ---[ 170]---> Sorter-cost: 127 Base: c ---[ 168]---> Sorter-cost: 127 Base: c ---[ 166]---> Sorter-cost: 127 Base: c ---[ 164]---> Sorter-cost: 127 Base: c ---[ 162]---> Sorter-cost: 127 Base: c ---[ 160]---> Sorter-cost: 127 Base: c ---[ 158]---> Sorter-cost: 127 Base: c ---[ 155]---> Sorter-cost: 127 Base: c ---[ 153]---> Sorter-cost: 127 Base: c ---[ 151]---> Sorter-cost: 127 Base: c ---[ 149]---> Sorter-cost: 127 Base: c ---[ 147]---> Sorter-cost: 127 Base: c ---[ 145]---> Sorter-cost: 127 Base: c ---[ 144]---> BDD-cost: 23 c ---[ 143]---> BDD-cost: 23 c ---[ 142]---> BDD-cost: 23 c ---[ 141]---> BDD-cost: 7 c ---[ 139]---> BDD-cost: 7 c ---[ 138]---> BDD-cost: 50 c ---[ 137]---> BDD-cost: 27 c ---[ 136]---> BDD-cost: 27 c ---[ 135]---> BDD-cost: 27 c ---[ 134]---> BDD-cost: 27 c ---[ 133]---> BDD-cost: 27 c ---[ 132]---> BDD-cost: 50 c ---[ 131]---> BDD-cost: 50 c ---[ 130]---> BDD-cost: 50 c ---[ 128]---> BDD-cost: 27 c ---[ 127]---> BDD-cost: 27 c ---[ 126]---> BDD-cost: 27 c ---[ 125]---> BDD-cost: 48 c ---[ 124]---> BDD-cost: 48 c ---[ 123]---> BDD-cost: 48 c ---[ 122]---> BDD-cost: 27 c ---[ 121]---> BDD-cost: 27 c ---[ 120]---> BDD-cost: 27 c ---[ 119]---> BDD-cost: 50 c ---[ 117]---> BDD-cost: 50 c ---[ 116]---> BDD-cost: 50 c ---[ 115]---> BDD-cost: 27 c ---[ 114]---> BDD-cost: 27 c ---[ 113]---> BDD-cost: 27 c ---[ 112]---> BDD-cost: 48 c ---[ 111]---> BDD-cost: 48 c ---[ 110]---> BDD-cost: 48 c ---[ 109]---> BDD-cost: 27 c ---[ 108]---> BDD-cost: 27 c ---[ 106]---> BDD-cost: 51 c ---[ 104]---> BDD-cost: 27 c ---[ 103]---> BDD-cost: 50 c ---[ 102]---> BDD-cost: 50 c ---[ 101]---> BDD-cost: 50 c ---[ 100]---> BDD-cost: 27 c ---[ 99]---> BDD-cost: 27 c ---[ 98]---> BDD-cost: 27 c ---[ 97]---> BDD-cost: 48 c ---[ 96]---> BDD-cost: 48 c ---[ 95]---> BDD-cost: 48 c ---[ 93]---> BDD-cost: 27 c ---[ 92]---> BDD-cost: 27 c ---[ 91]---> BDD-cost: 27 c ---[ 81]---> BDD-cost: 51 c ---[ 69]---> BDD-cost: 51 c ---[ 57]---> BDD-cost: 51 c ---[ 45]---> BDD-cost: 51 c ---[ 33]---> BDD-cost: 51 c ---[ 21]---> BDD-cost: 51 c ---[ 10]---> BDD-cost: 216 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 25782 84321 | 8594 0 0 nan | 0.000 % | c | 100 | 25752 84253 | 9453 98 6192 63.2 | 2.792 % | c ============================================================================== c [1mFound solution: 1583488[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 220 | 25767 84288 | 8589 218 12443 57.1 | 2.792 % | c ============================================================================== c [1mFound solution: 1580928[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 268 | 25776 84312 | 8592 266 20437 76.8 | 2.792 % | c | 368 | 25776 84312 | 9451 366 22162 60.6 | 2.817 % | c | 518 | 25776 84312 | 10396 516 29655 57.5 | 2.817 % | c | 744 | 25776 84312 | 11435 742 42680 57.5 | 2.817 % | c ============================================================================== c [1mFound solution: 1508608[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 870 | 25789 84343 | 8596 868 48024 55.3 | 2.817 % | c | 970 | 25789 84343 | 9455 968 60363 62.4 | 2.829 % | c | 1120 | 25778 84319 | 10401 1117 68505 61.3 | 2.872 % | c | 1347 | 25778 84319 | 11441 1344 77932 58.0 | 2.872 % | c | 1684 | 25778 84319 | 12585 1681 103593 61.6 | 2.872 % | c | 2190 | 25778 84319 | 13843 2187 126927 58.0 | 2.872 % | c | 2950 | 25767 84295 | 15228 2946 212260 72.1 | 2.916 % | c | 4090 | 25767 84295 | 16751 4086 295763 72.4 | 2.916 % | c | 5798 | 25731 84167 | 18426 5787 492222 85.1 | 2.945 % | c ============================================================================== c [1mFound solution: 1477248[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7454 | 25683 83993 | 8561 7434 643106 86.5 | 2.945 % | c | 7556 | 25683 83993 | 9417 7536 659060 87.5 | 3.056 % | c | 7706 | 25683 83993 | 10358 7686 665481 86.6 | 3.056 % | c | 7931 | 25683 83993 | 11394 7911 690952 87.3 | 3.056 % | c | 8270 | 25672 83969 | 12534 8249 707791 85.8 | 3.099 % | c | 8776 | 25672 83969 | 13787 8755 792296 90.5 | 3.099 % | c | 9537 | 25618 83822 | 15166 9509 863713 90.8 | 3.243 % | c | 10678 | 25536 83532 | 16682 10641 946280 88.9 | 3.358 % | c | 12386 | 25503 83415 | 18351 12346 1087746 88.1 | 3.387 % | c | 14949 | 25449 83245 | 20186 14900 1399535 93.9 | 3.488 % | c | 18793 | 25395 83098 | 22205 18736 1754727 93.7 | 3.632 % | c ============================================================================== c [1mFound solution: 1475328[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20218 | 25398 83107 | 8466 20160 1881199 93.3 | 3.632 % | c | 20322 | 25398 83107 | 9312 5144 289617 56.3 | 3.686 % | c | 20472 | 25398 83107 | 10243 5294 299464 56.6 | 3.686 % | c | 20697 | 25398 83107 | 11268 5519 320431 58.1 | 3.686 % | c | 21034 | 25387 83083 | 12395 5854 334549 57.1 | 3.729 % | c | 21540 | 25387 83083 | 13634 6360 407264 64.0 | 3.729 % | c | 22300 | 25354 82966 | 14998 7118 497542 69.9 | 3.758 % | c | 23439 | 25343 82942 | 16497 8256 599062 72.6 | 3.801 % | c | 25148 | 25316 82847 | 18147 9957 832837 83.6 | 3.830 % | c | 27712 | 25316 82847 | 19962 12521 1060640 84.7 | 3.830 % | c | 31557 | 25316 82847 | 21958 16366 1691483 103.4 | 3.830 % | c ============================================================================== c [1mFound solution: 1460608[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34542 | 25294 82772 | 8431 19345 1961844 101.4 | 3.830 % | c | 34643 | 25294 82772 | 9274 4938 275109 55.7 | 3.899 % | c | 34793 | 25294 82772 | 10201 5088 277980 54.6 | 3.899 % | c | 35019 | 25294 82772 | 11221 5314 292878 55.1 | 3.899 % | c | 35357 | 25294 82772 | 12343 5652 319785 56.6 | 3.899 % | c | 35863 | 25294 82772 | 13578 6158 364356 59.2 | 3.899 % | c | 36623 | 25294 82772 | 14936 6918 441267 63.8 | 3.899 % | c | 37763 | 25294 82772 | 16429 8058 574366 71.3 | 3.899 % | c ============================================================================== c [1mFound solution: 1458688[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38579 | 25307 82802 | 8435 8874 681730 76.8 | 3.899 % | c | 38679 | 25307 82802 | 9278 4537 324758 71.6 | 3.910 % | c | 38830 | 25296 82778 | 10206 4686 329928 70.4 | 3.953 % | c | 39055 | 25280 82743 | 11226 4907 340655 69.4 | 4.025 % | c | 39392 | 25204 82492 | 12349 5238 355692 67.9 | 4.168 % | c ============================================================================== c [1mFound solution: 1438848[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39556 | 25216 82524 | 8405 5402 383073 70.9 | 4.168 % | c | 39656 | 25173 82401 | 9245 5496 384861 70.0 | 4.279 % | c | 39806 | 25173 82401 | 10170 5646 400312 70.9 | 4.279 % | c | 40032 | 25151 82353 | 11187 5868 408033 69.5 | 4.365 % | c | 40369 | 25106 82252 | 12305 6197 430376 69.4 | 4.566 % | c | 40875 | 25106 82252 | 13536 6703 493435 73.6 | 4.566 % | c | 41634 | 25106 82252 | 14889 7462 569328 76.3 | 4.566 % | c | 42773 | 25106 82252 | 16378 8601 707090 82.2 | 4.566 % | c | 44481 | 25032 82007 | 18016 10298 853239 82.9 | 4.709 % | c | 47043 | 25021 81983 | 19818 12858 1115212 86.7 | 4.752 % | c | 50892 | 24980 81840 | 21800 16699 1507898 90.3 | 4.824 % | c ============================================================================== c [1mFound solution: 1431808[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 53691 | 24988 81862 | 8329 19495 1771927 90.9 | 4.824 % | c | 53791 | 24988 81862 | 9161 4974 265913 53.5 | 4.847 % | c | 53941 | 24988 81862 | 10078 5124 269820 52.7 | 4.847 % | c | 54167 | 24988 81862 | 11085 5350 286961 53.6 | 4.847 % | c | 54504 | 24958 81794 | 12194 5679 304170 53.6 | 4.962 % | c | 55010 | 24958 81794 | 13413 6185 351539 56.8 | 4.962 % | c | 55769 | 24958 81794 | 14755 6944 416677 60.0 | 4.962 % | c | 56909 | 24958 81794 | 16230 8084 562839 69.6 | 4.962 % | c | 58619 | 24947 81770 | 17853 9793 735565 75.1 | 5.005 % | c | 61182 | 24920 81700 | 19639 12351 959102 77.7 | 5.091 % | c | 65026 | 24907 81671 | 21603 16193 1315910 81.3 | 5.148 % | c | 70795 | 24907 81671 | 23763 21962 1922551 87.5 | 5.148 % | c | 79447 | 24865 81540 | 26139 18016 1482239 82.3 | 5.234 % | c | 92423 | 24801 81385 | 28753 16615 1259492 75.8 | 5.464 % | c ============================================================================== c [1mFound solution: 1427968[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 107128 | 24723 81184 | 8241 16283 1157306 71.1 | 5.464 % | c | 107230 | 24723 81184 | 9065 8244 476372 57.8 | 5.758 % | c | 107382 | 24723 81184 | 9971 8396 489220 58.3 | 5.759 % | c | 107608 | 24723 81184 | 10968 8622 522291 60.6 | 5.759 % | c | 107945 | 24723 81184 | 12065 8959 555312 62.0 | 5.758 % | c | 108452 | 24723 81184 | 13272 9466 618197 65.3 | 5.759 % | c | 109212 | 24678 81023 | 14599 10221 672039 65.8 | 5.787 % | c | 110351 | 24678 81023 | 16059 11360 765864 67.4 | 5.787 % | c | 112060 | 24678 81023 | 17665 13069 1024443 78.4 | 5.787 % | c | 114622 | 24620 80894 | 19431 15623 1365937 87.4 | 6.031 % | c | 118467 | 24590 80816 | 21375 19460 1763317 90.6 | 6.131 % | c | 124235 | 24590 80816 | 23512 14161 1019179 72.0 | 6.131 % | c | 132891 | 24551 80683 | 25863 22813 1779717 78.0 | 6.203 % | c | 145865 | 24551 80683 | 28450 22536 2054772 91.2 | 6.203 % | c ============================================================================== c [1mFound solution: 1423488[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 146568 | 24563 80714 | 8187 23239 2124527 91.4 | 6.203 % | c | 146668 | 24563 80714 | 9005 5910 256320 43.4 | 6.210 % | c | 146819 | 24563 80714 | 9906 6061 262458 43.3 | 6.210 % | c | 147044 | 24463 80383 | 10896 6275 285602 45.5 | 6.410 % | c | 147381 | 24423 80256 | 11986 6604 292865 44.3 | 6.496 % | c | 147887 | 24423 80256 | 13185 7110 338836 47.7 | 6.496 % | c | 148646 | 24423 80256 | 14503 7869 435930 55.4 | 6.496 % | c | 149788 | 24423 80256 | 15954 9011 542343 60.2 | 6.496 % | c | 151497 | 24406 80218 | 17549 10719 752216 70.2 | 6.567 % | c | 154060 | 24386 80171 | 19304 13280 990365 74.6 | 6.639 % | c | 157906 | 24386 80171 | 21234 17126 1287121 75.2 | 6.639 % | c | 163672 | 24340 80044 | 23358 11559 700256 60.6 | 6.796 % | c | 172321 | 24340 80044 | 25694 20208 1333788 66.0 | 6.796 % | c | 185296 | 24314 79967 | 28263 19623 1161767 59.2 | 6.854 % | c | 204758 | 24314 79967 | 31090 23903 1595766 66.8 | 6.854 % | c | 233951 | 24224 79722 | 34199 21100 1491804 70.7 | 7.154 % | c ============================================================================== c [1mFound solution: 1420288[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 269048 | 24088 79244 | 8029 16815 1491486 88.7 | 7.154 % | c | 269148 | 24088 79244 | 8831 8508 640879 75.3 | 7.459 % | c | 269298 | 24088 79244 | 9715 8658 661275 76.4 | 7.459 % | c | 269523 | 24088 79244 | 10686 8883 678039 76.3 | 7.459 % | c | 269860 | 24088 79244 | 11755 9220 719171 78.0 | 7.460 % | c | 270367 | 24088 79244 | 12930 9727 729922 75.0 | 7.459 % | c | 271127 | 24088 79244 | 14223 10487 840546 80.2 | 7.459 % | c | 272266 | 24073 79211 | 15646 11624 968142 83.3 | 7.516 % | c | 273975 | 24073 79211 | 17210 13333 1152071 86.4 | 7.516 % | c | 276537 | 24045 79149 | 18931 15889 1433911 90.2 | 7.631 % | c | 280383 | 23865 78603 | 20825 19704 1796107 91.2 | 8.117 % | c | 286151 | 23865 78603 | 22907 14391 1054594 73.3 | 8.117 % | c | 294801 | 23865 78603 | 25198 23041 1954414 84.8 | 8.117 % | c | 307776 | 23854 78579 | 27718 22285 2001861 89.8 | 8.159 % | c | 327237 | 23847 78564 | 30490 27154 2268727 83.6 | 8.188 % | c | 356429 | 23803 78464 | 33539 24241 1688878 69.7 | 8.402 % | c ============================================================================== c [1mFound solution: 1416448[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 384550 | 23765 78382 | 7921 32917 2863259 87.0 | 8.402 % | c | 384650 | 23754 78358 | 8713 7690 702581 91.4 | 8.665 % | c | 384801 | 23754 78358 | 9584 7841 714078 91.1 | 8.665 % | c | 385027 | 23754 78358 | 10542 8067 743664 92.2 | 8.665 % | c | 385364 | 23754 78358 | 11597 8404 790915 94.1 | 8.665 % | c | 385870 | 23678 78088 | 12756 8901 805477 90.5 | 8.822 % | c | 386631 | 23678 78088 | 14032 9662 860772 89.1 | 8.822 % | c | 387773 | 23678 78088 | 15435 10804 1046707 96.9 | 8.822 % | c | 389481 | 23678 78088 | 16979 12512 1164690 93.1 | 8.822 % | c | 392043 | 23678 78088 | 18677 15074 1561117 103.6 | 8.822 % | c | 395887 | 23678 78088 | 20545 18918 1996674 105.5 | 8.822 % | c | 401654 | 23678 78088 | 22599 13746 1222434 88.9 | 8.822 % | c | 410306 | 23665 78059 | 24859 22395 2137343 95.4 | 8.879 % | c | 423280 | 23647 77997 | 27345 21922 2153316 98.2 | 8.908 % |
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/6746/stat): 6746 (minisat+_script) R 6745 6746 19316 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855431038 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/6746/statm): 174 3 169 147 0 27 0 [pid=6746] 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=6747 New process pid=6748 New process pid=6749 execve syscall for /bin/sed executable One traced child (pid=6748) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=6749) exited with status: 0 One traced child (pid=6747) exited with status: 0 New process pid=6750 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-misc07.opb [startup+10.0037 s] Raw data (loadavg): 1.11 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 1624 0 0 0 979 6 0 0 25 0 1 0 1855431043 6725632 1526 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 1642 1526 145 145 0 1497 0 [pid=6750] vsize: 6568 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 8692 [startup+20.0053 s] Raw data (loadavg): 1.10 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 2189 0 0 0 1969 10 0 0 25 0 1 0 1855431043 9052160 2091 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 2210 2091 145 145 0 2065 0 [pid=6750] vsize: 8840 Current children cumulated CPU time (s) 19.8 Current children cumulated vsize (Kb) 10964 [startup+30.0059 s] Raw data (loadavg): 1.08 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 2692 0 0 0 2959 14 0 0 25 0 1 0 1855431043 11096064 2594 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 2709 2594 145 145 0 2564 0 [pid=6750] vsize: 10836 Current children cumulated CPU time (s) 29.74 Current children cumulated vsize (Kb) 12960 [startup+40.0065 s] Raw data (loadavg): 1.07 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3153 0 0 0 3950 19 0 0 25 0 1 0 1855431043 13033472 3055 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3182 3055 145 145 0 3037 0 [pid=6750] vsize: 12728 Current children cumulated CPU time (s) 39.7 Current children cumulated vsize (Kb) 14852 [startup+50.0071 s] Raw data (loadavg): 1.06 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3195 0 0 0 4949 19 0 0 25 0 1 0 1855431043 13201408 3097 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3223 3097 145 145 0 3078 0 [pid=6750] vsize: 12892 Current children cumulated CPU time (s) 49.69 Current children cumulated vsize (Kb) 15016 [startup+60.0087 s] Raw data (loadavg): 1.05 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3195 0 0 0 5948 20 0 0 25 0 1 0 1855431043 13201408 3097 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3223 3097 145 145 0 3078 0 [pid=6750] vsize: 12892 Current children cumulated CPU time (s) 59.69 Current children cumulated vsize (Kb) 15016 [startup+70.0093 s] Raw data (loadavg): 1.04 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 6946 21 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 69.68 Current children cumulated vsize (Kb) 15572 [startup+80.0099 s] Raw data (loadavg): 1.03 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 7945 22 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223056 134562152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 79.68 Current children cumulated vsize (Kb) 15572 [startup+90.0115 s] Raw data (loadavg): 1.03 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 8945 22 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 89.68 Current children cumulated vsize (Kb) 15572 [startup+100.012 s] Raw data (loadavg): 1.02 1.01 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 9945 22 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 99.68 Current children cumulated vsize (Kb) 15572 [startup+110.014 s] Raw data (loadavg): 1.02 1.00 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 10944 23 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 109.68 Current children cumulated vsize (Kb) 15572 [startup+120.015 s] Raw data (loadavg): 1.10 1.02 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 11944 23 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 119.68 Current children cumulated vsize (Kb) 15572 [startup+130.016 s] Raw data (loadavg): 1.08 1.02 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 12944 23 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 129.68 Current children cumulated vsize (Kb) 15572 [startup+140.017 s] Raw data (loadavg): 1.07 1.02 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 13943 24 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0 [pid=6750] vsize: 13448 Current children cumulated CPU time (s) 139.68 Current children cumulated vsize (Kb) 15572 [startup+150.017 s] Raw data (loadavg): 1.06 1.02 0.98 2/57 6750 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3434 0 0 0 14942 25 0 0 25 0 1 0 1855431043 14172160 3336 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3460 3336 145 145 0 3315 0 [pid=6750] vsize: 13840 Current children cumulated CPU time (s) 149.68 Current children cumulated vsize (Kb) 15964 [startup+160.018 s] Raw data (loadavg): 1.20 1.05 0.99 3/60 6791 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3754 0 0 0 15926 36 0 0 19 0 1 0 1855431043 15482880 3656 4294967295 134512640 135094434 3221224432 3221222160 134562860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 3780 3656 145 145 0 3635 0 [pid=6750] vsize: 15120 Current children cumulated CPU time (s) 159.63 Current children cumulated vsize (Kb) 17244 [startup+170.018 s] Raw data (loadavg): 1.17 1.05 0.99 2/57 6801 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3754 0 0 0 16925 38 0 0 25 0 1 0 1855431043 15482880 3656 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3780 3656 145 145 0 3635 0 [pid=6750] vsize: 15120 Current children cumulated CPU time (s) 169.64 Current children cumulated vsize (Kb) 17244 [startup+180.019 s] Raw data (loadavg): 1.14 1.05 0.99 2/57 6801 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3761 0 0 0 17925 38 0 0 25 0 1 0 1855431043 15515648 3663 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3788 3663 145 145 0 3643 0 [pid=6750] vsize: 15152 Current children cumulated CPU time (s) 179.64 Current children cumulated vsize (Kb) 17276 [startup+190.019 s] Raw data (loadavg): 1.12 1.04 0.99 2/57 6801 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3768 0 0 0 18925 38 0 0 25 0 1 0 1855431043 15548416 3670 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3796 3670 145 145 0 3651 0 [pid=6750] vsize: 15184 Current children cumulated CPU time (s) 189.64 Current children cumulated vsize (Kb) 17308 [startup+200.02 s] Raw data (loadavg): 1.10 1.04 0.99 2/57 6801 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3924 0 0 0 19923 39 0 0 25 0 1 0 1855431043 16195584 3826 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 3954 3826 145 145 0 3809 0 [pid=6750] vsize: 15816 Current children cumulated CPU time (s) 199.63 Current children cumulated vsize (Kb) 17940 [startup+210.022 s] Raw data (loadavg): 1.09 1.04 0.99 2/57 6801 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4240 0 0 0 20916 42 0 0 25 0 1 0 1855431043 17477632 4142 4294967295 134512640 135094434 3221224432 3221223104 134555606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4267 4142 145 145 0 4122 0 [pid=6750] vsize: 17068 Current children cumulated CPU time (s) 209.59 Current children cumulated vsize (Kb) 19192 [startup+220.022 s] Raw data (loadavg): 1.07 1.04 0.99 2/57 6801 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4240 0 0 0 21916 42 0 0 25 0 1 0 1855431043 17477632 4142 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4267 4142 145 145 0 4122 0 [pid=6750] vsize: 17068 Current children cumulated CPU time (s) 219.59 Current children cumulated vsize (Kb) 19192 [startup+230.023 s] Raw data (loadavg): 1.06 1.04 0.99 2/57 6803 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4240 0 0 0 22916 42 0 0 25 0 1 0 1855431043 17477632 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4267 4142 145 145 0 4122 0 [pid=6750] vsize: 17068 Current children cumulated CPU time (s) 229.59 Current children cumulated vsize (Kb) 19192 [startup+240.024 s] Raw data (loadavg): 1.05 1.03 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4287 0 0 0 23916 42 0 0 25 0 1 0 1855431043 17686528 4189 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4318 4189 145 145 0 4173 0 [pid=6750] vsize: 17272 Current children cumulated CPU time (s) 239.59 Current children cumulated vsize (Kb) 19396 [startup+250.024 s] Raw data (loadavg): 1.04 1.03 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4323 0 0 0 24916 43 0 0 25 0 1 0 1855431043 17866752 4225 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4362 4225 145 145 0 4217 0 [pid=6750] vsize: 17448 Current children cumulated CPU time (s) 249.6 Current children cumulated vsize (Kb) 19572 [startup+260.026 s] Raw data (loadavg): 1.04 1.03 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 25916 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223088 134556605 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 259.6 Current children cumulated vsize (Kb) 19860 [startup+270.026 s] Raw data (loadavg): 1.03 1.03 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 26916 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223104 134556279 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 269.6 Current children cumulated vsize (Kb) 19860 [startup+280.026 s] Raw data (loadavg): 1.02 1.03 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 27916 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 279.6 Current children cumulated vsize (Kb) 19860 [startup+290.026 s] Raw data (loadavg): 1.02 1.03 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 28917 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 289.61 Current children cumulated vsize (Kb) 19860 [startup+300.027 s] Raw data (loadavg): 1.02 1.03 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 29917 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 299.61 Current children cumulated vsize (Kb) 19860 [startup+310.028 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4380 0 0 0 30916 43 0 0 25 0 1 0 1855431043 18161664 4282 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4282 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 309.6 Current children cumulated vsize (Kb) 19860 [startup+320.028 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 31916 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 319.6 Current children cumulated vsize (Kb) 19860 [startup+330.029 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 32916 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 329.6 Current children cumulated vsize (Kb) 19860 [startup+340.029 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 33916 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 339.6 Current children cumulated vsize (Kb) 19860 [startup+350.029 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 34917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 349.61 Current children cumulated vsize (Kb) 19860 [startup+360.03 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 35917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 359.61 Current children cumulated vsize (Kb) 19860 [startup+370.03 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 36917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 369.61 Current children cumulated vsize (Kb) 19860 [startup+380.031 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 37917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 379.61 Current children cumulated vsize (Kb) 19860 [startup+390.031 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 38917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 389.61 Current children cumulated vsize (Kb) 19860 [startup+400.032 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 39917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 399.61 Current children cumulated vsize (Kb) 19860 [startup+410.033 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 40918 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 409.62 Current children cumulated vsize (Kb) 19860 [startup+420.033 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 41918 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 419.62 Current children cumulated vsize (Kb) 19860 [startup+430.034 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 42918 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 429.62 Current children cumulated vsize (Kb) 19860 [startup+440.034 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4383 0 0 0 43918 43 0 0 25 0 1 0 1855431043 18161664 4285 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4434 4285 145 145 0 4289 0 [pid=6750] vsize: 17736 Current children cumulated CPU time (s) 439.62 Current children cumulated vsize (Kb) 19860 [startup+450.035 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4426 0 0 0 44918 43 0 0 25 0 1 0 1855431043 18374656 4328 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4486 4328 145 145 0 4341 0 [pid=6750] vsize: 17944 Current children cumulated CPU time (s) 449.62 Current children cumulated vsize (Kb) 20068 [startup+460.036 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4476 0 0 0 45918 43 0 0 25 0 1 0 1855431043 18636800 4378 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4550 4378 145 145 0 4405 0 [pid=6750] vsize: 18200 Current children cumulated CPU time (s) 459.62 Current children cumulated vsize (Kb) 20324 [startup+470.036 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4502 0 0 0 46919 43 0 0 25 0 1 0 1855431043 18767872 4404 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4582 4404 145 145 0 4437 0 [pid=6750] vsize: 18328 Current children cumulated CPU time (s) 469.63 Current children cumulated vsize (Kb) 20452 [startup+480.036 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6805 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4551 0 0 0 47919 43 0 0 25 0 1 0 1855431043 19025920 4453 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4645 4453 145 145 0 4500 0 [pid=6750] vsize: 18580 Current children cumulated CPU time (s) 479.63 Current children cumulated vsize (Kb) 20704 [startup+490.036 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4551 0 0 0 48918 44 0 0 25 0 1 0 1855431043 19025920 4453 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4645 4453 145 145 0 4500 0 [pid=6750] vsize: 18580 Current children cumulated CPU time (s) 489.63 Current children cumulated vsize (Kb) 20704 [startup+500.037 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4564 0 0 0 49917 45 0 0 25 0 1 0 1855431043 19091456 4466 4294967295 134512640 135094434 3221224432 3221223120 134554736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4661 4466 145 145 0 4516 0 [pid=6750] vsize: 18644 Current children cumulated CPU time (s) 499.63 Current children cumulated vsize (Kb) 20768 [startup+510.038 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4575 0 0 0 50917 45 0 0 25 0 1 0 1855431043 19156992 4477 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4677 4477 145 145 0 4532 0 [pid=6750] vsize: 18708 Current children cumulated CPU time (s) 509.63 Current children cumulated vsize (Kb) 20832 [startup+520.038 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4596 0 0 0 51917 46 0 0 25 0 1 0 1855431043 19288064 4498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4709 4498 145 145 0 4564 0 [pid=6750] vsize: 18836 Current children cumulated CPU time (s) 519.64 Current children cumulated vsize (Kb) 20960 [startup+530.039 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4666 0 0 0 52916 46 0 0 25 0 1 0 1855431043 19681280 4568 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4805 4568 145 145 0 4660 0 [pid=6750] vsize: 19220 Current children cumulated CPU time (s) 529.63 Current children cumulated vsize (Kb) 21344 [startup+540.039 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 53916 47 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0 [pid=6750] vsize: 19348 Current children cumulated CPU time (s) 539.64 Current children cumulated vsize (Kb) 21472 [startup+550.04 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 54915 47 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0 [pid=6750] vsize: 19348 Current children cumulated CPU time (s) 549.63 Current children cumulated vsize (Kb) 21472 [startup+560.041 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 55914 49 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0 [pid=6750] vsize: 19348 Current children cumulated CPU time (s) 559.64 Current children cumulated vsize (Kb) 21472 [startup+570.041 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 56914 49 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0 [pid=6750] vsize: 19348 Current children cumulated CPU time (s) 569.64 Current children cumulated vsize (Kb) 21472 [startup+580.041 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4698 0 0 0 57915 49 0 0 25 0 1 0 1855431043 19812352 4600 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4837 4600 145 145 0 4692 0 [pid=6750] vsize: 19348 Current children cumulated CPU time (s) 579.65 Current children cumulated vsize (Kb) 21472 [startup+590.042 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4699 0 0 0 58915 49 0 0 25 0 1 0 1855431043 19812352 4601 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4837 4601 145 145 0 4692 0 [pid=6750] vsize: 19348 Current children cumulated CPU time (s) 589.65 Current children cumulated vsize (Kb) 21472 [startup+600.042 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4699 0 0 0 59915 49 0 0 25 0 1 0 1855431043 19812352 4601 4294967295 134512640 135094434 3221224432 3221223104 134556210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 4837 4601 145 145 0 4692 0 [pid=6750] vsize: 19348 Current children cumulated CPU time (s) 599.65 Current children cumulated vsize (Kb) 21472 [startup+610.043 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4966 0 0 0 60911 50 0 0 25 0 1 0 1855431043 20905984 4868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5104 4868 145 145 0 4959 0 [pid=6750] vsize: 20416 Current children cumulated CPU time (s) 609.62 Current children cumulated vsize (Kb) 22540 [startup+620.043 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 61907 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221222896 134781535 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0 [pid=6750] vsize: 21004 Current children cumulated CPU time (s) 619.59 Current children cumulated vsize (Kb) 23128 [startup+630.043 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 62908 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0 [pid=6750] vsize: 21004 Current children cumulated CPU time (s) 629.6 Current children cumulated vsize (Kb) 23128 [startup+640.044 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 63908 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0 [pid=6750] vsize: 21004 Current children cumulated CPU time (s) 639.6 Current children cumulated vsize (Kb) 23128 [startup+650.044 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 64908 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0 [pid=6750] vsize: 21004 Current children cumulated CPU time (s) 649.6 Current children cumulated vsize (Kb) 23128 [startup+660.045 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5355 0 0 0 65904 53 0 0 25 0 1 0 1855431043 22626304 5257 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5524 5257 145 145 0 5379 0 [pid=6750] vsize: 22096 Current children cumulated CPU time (s) 659.58 Current children cumulated vsize (Kb) 24220 [startup+670.045 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 66897 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0 [pid=6750] vsize: 23804 Current children cumulated CPU time (s) 669.54 Current children cumulated vsize (Kb) 25928 [startup+680.046 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 67897 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0 [pid=6750] vsize: 23804 Current children cumulated CPU time (s) 679.54 Current children cumulated vsize (Kb) 25928 [startup+690.047 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 68897 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0 [pid=6750] vsize: 23804 Current children cumulated CPU time (s) 689.54 Current children cumulated vsize (Kb) 25928 [startup+700.047 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 69898 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0 [pid=6750] vsize: 23804 Current children cumulated CPU time (s) 699.55 Current children cumulated vsize (Kb) 25928 [startup+710.049 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 70898 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0 [pid=6750] vsize: 23804 Current children cumulated CPU time (s) 709.55 Current children cumulated vsize (Kb) 25928 [startup+720.049 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6184 0 0 0 71890 59 0 0 25 0 1 0 1855431043 26009600 6086 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6350 6086 145 145 0 6205 0 [pid=6750] vsize: 25400 Current children cumulated CPU time (s) 719.5 Current children cumulated vsize (Kb) 27524 [startup+730.05 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 72888 60 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 729.49 Current children cumulated vsize (Kb) 27832 [startup+740.052 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 73889 60 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223024 134556727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 739.5 Current children cumulated vsize (Kb) 27832 [startup+750.052 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 74889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 749.51 Current children cumulated vsize (Kb) 27832 [startup+760.053 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 75888 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 759.5 Current children cumulated vsize (Kb) 27832 [startup+770.053 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 76888 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 769.5 Current children cumulated vsize (Kb) 27832 [startup+780.054 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 77888 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 779.5 Current children cumulated vsize (Kb) 27832 [startup+790.054 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 78889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 789.51 Current children cumulated vsize (Kb) 27832 [startup+800.055 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 79889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 799.51 Current children cumulated vsize (Kb) 27832 [startup+810.057 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 80889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 809.51 Current children cumulated vsize (Kb) 27832 [startup+820.057 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 81889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 819.51 Current children cumulated vsize (Kb) 27832 [startup+830.057 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 82889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 829.51 Current children cumulated vsize (Kb) 27832 [startup+840.058 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 83890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 839.52 Current children cumulated vsize (Kb) 27832 [startup+850.058 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 84890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 849.52 Current children cumulated vsize (Kb) 27832 [startup+860.059 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 85890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221222896 134781514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 859.52 Current children cumulated vsize (Kb) 27832 [startup+870.059 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 86890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 869.52 Current children cumulated vsize (Kb) 27832 [startup+880.06 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 87891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 879.53 Current children cumulated vsize (Kb) 27832 [startup+890.061 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 88891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 889.53 Current children cumulated vsize (Kb) 27832 [startup+900.061 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 89891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 899.53 Current children cumulated vsize (Kb) 27832 [startup+910.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 90891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 909.53 Current children cumulated vsize (Kb) 27832 [startup+920.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 91892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 919.54 Current children cumulated vsize (Kb) 27832 [startup+930.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 92892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 929.54 Current children cumulated vsize (Kb) 27832 [startup+940.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 93892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 939.54 Current children cumulated vsize (Kb) 27832 [startup+950.063 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 94892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 949.54 Current children cumulated vsize (Kb) 27832 [startup+960.064 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 95893 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 959.55 Current children cumulated vsize (Kb) 27832 [startup+970.064 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 96893 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 969.55 Current children cumulated vsize (Kb) 27832 [startup+980.065 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6265 0 0 0 97932 61 0 0 25 0 1 0 1855431043 26324992 6167 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6167 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 979.94 Current children cumulated vsize (Kb) 27832 [startup+990.455 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6265 0 0 0 98932 61 0 0 25 0 1 0 1855431043 26324992 6167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6167 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 989.94 Current children cumulated vsize (Kb) 27832 [startup+1000.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6265 0 0 0 99932 61 0 0 25 0 1 0 1855431043 26324992 6167 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6167 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 999.94 Current children cumulated vsize (Kb) 27832 [startup+1010.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 100932 61 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1009.94 Current children cumulated vsize (Kb) 27832 [startup+1020.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 101933 61 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1019.95 Current children cumulated vsize (Kb) 27832 [startup+1030.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 102933 61 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1029.95 Current children cumulated vsize (Kb) 27832 [startup+1040.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 103933 62 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1039.96 Current children cumulated vsize (Kb) 27832 [startup+1050.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 104933 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1049.96 Current children cumulated vsize (Kb) 27832 [startup+1060.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 105933 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1059.96 Current children cumulated vsize (Kb) 27832 [startup+1070.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 106933 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1069.96 Current children cumulated vsize (Kb) 27832 [startup+1080.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 107934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1079.97 Current children cumulated vsize (Kb) 27832 [startup+1090.46 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 108934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1089.97 Current children cumulated vsize (Kb) 27832 [startup+1100.46 s] Raw data (loadavg): 1.07 1.02 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 109934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1099.97 Current children cumulated vsize (Kb) 27832 [startup+1110.46 s] Raw data (loadavg): 1.06 1.02 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 110934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1109.97 Current children cumulated vsize (Kb) 27832 [startup+1120.46 s] Raw data (loadavg): 1.05 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 111934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1119.97 Current children cumulated vsize (Kb) 27832 [startup+1130.46 s] Raw data (loadavg): 1.04 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 112934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1129.97 Current children cumulated vsize (Kb) 27832 [startup+1140.46 s] Raw data (loadavg): 1.04 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 113935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1139.98 Current children cumulated vsize (Kb) 27832 [startup+1150.46 s] Raw data (loadavg): 1.03 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 114935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1149.98 Current children cumulated vsize (Kb) 27832 [startup+1160.46 s] Raw data (loadavg): 1.02 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 115935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1159.98 Current children cumulated vsize (Kb) 27832 [startup+1170.46 s] Raw data (loadavg): 1.02 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 116935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1169.98 Current children cumulated vsize (Kb) 27832 [startup+1180.46 s] Raw data (loadavg): 1.02 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 117935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1179.98 Current children cumulated vsize (Kb) 27832 [startup+1190.46 s] Raw data (loadavg): 1.01 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 118936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1189.99 Current children cumulated vsize (Kb) 27832 [startup+1200.46 s] Raw data (loadavg): 1.01 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 119936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1199.99 Current children cumulated vsize (Kb) 27832 [startup+1210.46 s] Raw data (loadavg): 1.01 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 120936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1209.99 Current children cumulated vsize (Kb) 27832 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.47 s] Raw data (loadavg): 1.01 1.01 1.00 2/57 6807 Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6746/statm): 531 226 485 147 0 384 0 [pid=6746] vsize: 2124 Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 120936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0 [pid=6750] vsize: 25708 Current children cumulated CPU time (s) 1209.99 Current children cumulated vsize (Kb) 27832 Sending SIGTERM to -6746 Sleeping 2 seconds One traced child (pid=6746) ended because it received signal 15 (SIGTERM) One traced child (pid=6750) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.48 CPU time (s): 1210.01 CPU user time (s): 1209.37 CPU system time (s): 0.638902 CPU usage (%): 99.9607 Max. virtual memory (cumulated for all children) (Kb): 27832
ERROR: no interpretation found !