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 wulflinc7 THE 2005-05-25 22:27:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22545 boxname=wulflinc7 idbench=1361 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: a3dd3cd7dd293e24bffaff8bb73da54c /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-misc07.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-misc07.opb IDLAUNCH: 22545 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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: 916184 kB Buffers: 31228 kB Cached: 67580 kB SwapCached: 676 kB Active: 17872 kB Inactive: 82992 kB HighTotal: 131008 kB HighFree: 102480 kB LowTotal: 903652 kB LowFree: 813704 kB SwapTotal: 2097136 kB SwapFree: 2095524 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5068 kB Slab: 11980 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 22:48:00 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 22545 7 1229.84 152 #### 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 ---[ 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 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 14980 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.91 0.97 0.91 2/54 14976 Raw data (stat): 14976 (runsolver) R 14975 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784262234 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0005 s] Raw data (loadavg): 0.93 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0012 s] Raw data (loadavg): 0.94 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0021 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0023 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0024 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.003 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0032 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0043 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0049 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.107 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.113 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.113 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.113 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.113 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.114 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.114 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.115 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.115 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.114 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.114 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.114 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.115 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.115 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.115 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.116 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.117 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.118 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.117 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.118 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.73 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 14980 Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.73 CPU time (s): 1229.84 CPU user time (s): 1229.5 CPU system time (s): 0.347947 CPU usage (%): 100.009 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####