Name | normalized-opb/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 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-04-21 15:58:35 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17685 boxname=wulflinc29 idbench=1361 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: a3dd3cd7dd293e24bffaff8bb73da54c /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-misc07.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-misc07.opb IDLAUNCH: 17685 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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.020 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: 915856 kB Buffers: 11932 kB Cached: 80936 kB SwapCached: 4304 kB Active: 16460 kB Inactive: 82172 kB HighTotal: 131008 kB HighFree: 52584 kB LowTotal: 903652 kB LowFree: 863272 kB SwapTotal: 2097892 kB SwapFree: 2092680 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5100 kB Slab: 14440 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 16:18:37 (client local time) WITH STATUS 10 IN 1200.19 SECONDS stats: 17685 7 1200.19 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) 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 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.93 0.97 0.92 2/54 1156 Raw data (stat): 1156 (runsolver) R 1155 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546339079 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0013 s] Raw data (loadavg): 0.94 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 1926 0 0 0 994 5 0 0 25 0 1 0 546339079 9252864 1856 4294967295 134512640 134672761 3221224624 3221223808 134559045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2259 1856 603 41 0 2218 0 vsize: 9036 [startup+20.0016 s] Raw data (loadavg): 0.95 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 2440 0 0 0 1992 6 0 0 25 0 1 0 546339079 11407360 2370 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2785 2370 603 41 0 2744 0 vsize: 11140 [startup+30.0014 s] Raw data (loadavg): 0.95 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 2969 0 0 0 2990 9 0 0 25 0 1 0 546339079 13561856 2899 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3311 2899 603 41 0 3270 0 vsize: 13244 [startup+40.0016 s] Raw data (loadavg): 0.96 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3343 0 0 0 3988 10 0 0 25 0 1 0 546339079 15151104 3273 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3699 3273 603 41 0 3658 0 vsize: 14796 [startup+50.002 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3343 0 0 0 4988 11 0 0 25 0 1 0 546339079 15151104 3273 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3699 3273 603 41 0 3658 0 vsize: 14796 [startup+60.0032 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3343 0 0 0 5988 11 0 0 25 0 1 0 546339079 15151104 3273 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3699 3273 603 41 0 3658 0 vsize: 14796 [startup+70.004 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 6987 12 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+80.0043 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 1156 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 7987 12 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+90.0049 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 1168 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 8984 14 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+100.005 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 1209 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 9982 16 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+110.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1209 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 10981 17 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223728 134560180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+120.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1209 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 11981 18 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1209 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 12981 18 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+140.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1209 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 13981 18 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3829 3412 603 41 0 3788 0 vsize: 15316 [startup+150.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1209 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3694 0 0 0 14980 19 0 0 25 0 1 0 546339079 16613376 3624 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4056 3624 603 41 0 4015 0 vsize: 16224 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1209 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3902 0 0 0 15979 20 0 0 25 0 1 0 546339079 17412096 3832 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4251 3832 603 41 0 4210 0 vsize: 17004 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3902 0 0 0 16979 21 0 0 25 0 1 0 546339079 17412096 3832 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4251 3832 603 41 0 4210 0 vsize: 17004 [startup+180.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3910 0 0 0 17978 22 0 0 25 0 1 0 546339079 17412096 3840 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4251 3840 603 41 0 4210 0 vsize: 17004 [startup+190.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3924 0 0 0 18978 22 0 0 25 0 1 0 546339079 17555456 3854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4286 3854 603 41 0 4245 0 vsize: 17144 [startup+200.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4277 0 0 0 19976 24 0 0 25 0 1 0 546339079 18894848 4207 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4613 4207 603 41 0 4572 0 vsize: 18452 [startup+210.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4389 0 0 0 20976 24 0 0 25 0 1 0 546339079 19423232 4319 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4742 4319 603 41 0 4701 0 vsize: 18968 [startup+220.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4389 0 0 0 21976 25 0 0 25 0 1 0 546339079 19423232 4319 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4742 4319 603 41 0 4701 0 vsize: 18968 [startup+230.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4408 0 0 0 22975 25 0 0 25 0 1 0 546339079 19423232 4338 4294967295 134512640 134672761 3221224624 3221223760 134565137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4742 4338 603 41 0 4701 0 vsize: 18968 [startup+240.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4449 0 0 0 23975 26 0 0 25 0 1 0 546339079 19718144 4379 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4814 4379 603 41 0 4773 0 vsize: 19256 [startup+250.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4513 0 0 0 24975 26 0 0 25 0 1 0 546339079 20029440 4443 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4443 603 41 0 4849 0 vsize: 19560 [startup+260.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 25975 26 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4454 603 41 0 4849 0 vsize: 19560 [startup+270.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 26974 27 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223760 134565101 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4454 603 41 0 4849 0 vsize: 19560 [startup+280.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 27974 27 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4454 603 41 0 4849 0 vsize: 19560 [startup+290.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 28974 28 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4454 603 41 0 4849 0 vsize: 19560 [startup+300.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 29973 28 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4454 603 41 0 4849 0 vsize: 19560 [startup+310.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 30973 29 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4454 603 41 0 4849 0 vsize: 19560 [startup+320.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 31973 29 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+330.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 32973 30 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+340.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 33972 30 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+350.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 34972 31 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223808 134559038 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 35971 31 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+370.013 s] Raw data (loadavg): 0.99 0.97 0.92 3/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 36971 32 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+380.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 37971 32 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+390.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 38970 33 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+400.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 39970 33 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+410.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 40970 33 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4456 603 41 0 4849 0 vsize: 19560 [startup+420.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4527 0 0 0 41970 34 0 0 25 0 1 0 546339079 20029440 4457 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4457 603 41 0 4849 0 vsize: 19560 [startup+430.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1211 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4528 0 0 0 42969 34 0 0 25 0 1 0 546339079 20029440 4458 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4890 4458 603 41 0 4849 0 vsize: 19560 [startup+440.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4566 0 0 0 43968 35 0 0 25 0 1 0 546339079 20193280 4496 4294967295 134512640 134672761 3221224624 3221223808 134559512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4930 4496 603 41 0 4889 0 vsize: 19720 [startup+450.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4610 0 0 0 44968 36 0 0 25 0 1 0 546339079 20357120 4540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4970 4540 603 41 0 4929 0 vsize: 19880 [startup+460.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4641 0 0 0 45968 36 0 0 25 0 1 0 546339079 20553728 4571 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5018 4571 603 41 0 4977 0 vsize: 20072 [startup+470.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4685 0 0 0 46967 37 0 0 25 0 1 0 546339079 20881408 4615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5098 4615 603 41 0 5057 0 vsize: 20392 [startup+480.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4685 0 0 0 47967 37 0 0 25 0 1 0 546339079 20881408 4615 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5098 4615 603 41 0 5057 0 vsize: 20392 [startup+490.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4711 0 0 0 48967 37 0 0 25 0 1 0 546339079 21045248 4641 4294967295 134512640 134672761 3221224624 3221223760 134560613 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5138 4641 603 41 0 5097 0 vsize: 20552 [startup+500.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4713 0 0 0 49967 38 0 0 25 0 1 0 546339079 21045248 4643 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5138 4643 603 41 0 5097 0 vsize: 20552 [startup+510.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4742 0 0 0 50967 38 0 0 25 0 1 0 546339079 21209088 4672 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5178 4672 603 41 0 5137 0 vsize: 20712 [startup+520.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4784 0 0 0 51967 38 0 0 25 0 1 0 546339079 21405696 4714 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5226 4714 603 41 0 5185 0 vsize: 20904 [startup+530.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4834 0 0 0 52966 39 0 0 25 0 1 0 546339079 21798912 4764 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5322 4764 603 41 0 5281 0 vsize: 21288 [startup+540.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4835 0 0 0 53966 39 0 0 25 0 1 0 546339079 21798912 4765 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5322 4765 603 41 0 5281 0 vsize: 21288 [startup+550.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4835 0 0 0 54965 40 0 0 25 0 1 0 546339079 21798912 4765 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5322 4765 603 41 0 5281 0 vsize: 21288 [startup+560.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4835 0 0 0 55965 41 0 0 25 0 1 0 546339079 21798912 4765 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5322 4765 603 41 0 5281 0 vsize: 21288 [startup+570.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4837 0 0 0 56965 41 0 0 25 0 1 0 546339079 21798912 4767 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5322 4767 603 41 0 5281 0 vsize: 21288 [startup+580.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4838 0 0 0 57964 42 0 0 25 0 1 0 546339079 21798912 4768 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5322 4768 603 41 0 5281 0 vsize: 21288 [startup+590.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4838 0 0 0 58964 42 0 0 25 0 1 0 546339079 21798912 4768 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5322 4768 603 41 0 5281 0 vsize: 21288 [startup+600.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5037 0 0 0 59963 43 0 0 25 0 1 0 546339079 22601728 4967 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5518 4967 603 41 0 5477 0 vsize: 22072 [startup+610.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5249 0 0 0 60962 44 0 0 25 0 1 0 546339079 23408640 5179 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5715 5179 603 41 0 5674 0 vsize: 22860 [startup+620.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5257 0 0 0 61962 45 0 0 25 0 1 0 546339079 23408640 5187 4294967295 134512640 134672761 3221224624 3221223808 134559332 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5715 5187 603 41 0 5674 0 vsize: 22860 [startup+630.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5257 0 0 0 62962 45 0 0 25 0 1 0 546339079 23408640 5187 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5715 5187 603 41 0 5674 0 vsize: 22860 [startup+640.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5257 0 0 0 63962 45 0 0 25 0 1 0 546339079 23408640 5187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5715 5187 603 41 0 5674 0 vsize: 22860 [startup+650.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5453 0 0 0 64961 46 0 0 25 0 1 0 546339079 24203264 5383 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5909 5383 603 41 0 5868 0 vsize: 23636 [startup+660.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5898 0 0 0 65960 48 0 0 25 0 1 0 546339079 26206208 5828 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6398 5828 603 41 0 6357 0 vsize: 25592 [startup+670.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 66960 48 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6430 5858 603 41 0 6389 0 vsize: 25720 [startup+680.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 67960 48 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6430 5858 603 41 0 6389 0 vsize: 25720 [startup+690.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 68960 49 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6430 5858 603 41 0 6389 0 vsize: 25720 [startup+700.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 69959 49 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6430 5858 603 41 0 6389 0 vsize: 25720 [startup+710.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6299 0 0 0 70958 51 0 0 25 0 1 0 546339079 27815936 6229 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6791 6229 603 41 0 6750 0 vsize: 27164 [startup+720.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 71957 51 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+730.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 72957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+740.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 73957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+750.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 74957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+760.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 75957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+770.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 76957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+780.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 77957 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+790.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 78957 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+800.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 79958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+810.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 80958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+820.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 81958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134565110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+830.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 82958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+840.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 83958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+850.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 84958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6336 603 41 0 6847 0 vsize: 27552 [startup+860.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 85959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6337 603 41 0 6847 0 vsize: 27552 [startup+870.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 86959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6337 603 41 0 6847 0 vsize: 27552 [startup+880.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 87959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223808 134558629 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6337 603 41 0 6847 0 vsize: 27552 [startup+890.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 88959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6337 603 41 0 6847 0 vsize: 27552 [startup+900.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 89959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6337 603 41 0 6847 0 vsize: 27552 [startup+910.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 90960 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223808 134558638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6337 603 41 0 6847 0 vsize: 27552 [startup+920.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 91960 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6337 603 41 0 6847 0 vsize: 27552 [startup+930.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 92960 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6338 603 41 0 6847 0 vsize: 27552 [startup+940.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 93960 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6338 603 41 0 6847 0 vsize: 27552 [startup+950.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 94960 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6338 603 41 0 6847 0 vsize: 27552 [startup+960.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 95961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6338 603 41 0 6847 0 vsize: 27552 [startup+970.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 96961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6338 603 41 0 6847 0 vsize: 27552 [startup+980.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 97961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6338 603 41 0 6847 0 vsize: 27552 [startup+990.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 98961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6338 603 41 0 6847 0 vsize: 27552 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 99961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 100961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 101960 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 102960 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 103960 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 104961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 105961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134561127 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 106961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 107961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 108961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 109961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 110962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 111962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223824 134557897 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 112962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 113962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 114962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 115963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 116963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 117963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 118963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 [startup+1200.03 s] Raw data (loadavg): 1.07 0.99 0.93 2/54 1213 Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 119963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6888 6340 603 41 0 6847 0 vsize: 27552 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 1.07 0.99 0.93 1/54 1213 Raw data (stat): 1156 (minisat+) Z 1155 27222 27221 0 -1 12 6413 0 0 0 119963 54 0 0 25 0 1 0 546339079 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.05 CPU time (s): 1200.19 CPU user time (s): 1199.64 CPU system time (s): 0.546916 CPU usage (%): 100.012 Max. virtual memory (Kb): 27552 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####