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 wulflinc8 THE 2005-04-21 04:16:22 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17693 boxname=wulflinc8 idbench=1361 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a3dd3cd7dd293e24bffaff8bb73da54c /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-misc07.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-misc07.opb IDLAUNCH: 17693 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 581232 kB Buffers: 34476 kB Cached: 395488 kB SwapCached: 0 kB Active: 169888 kB Inactive: 262964 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 580980 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6948 kB Slab: 14816 kB Committed_AS: 63588 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 04:36:24 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 17693 7 1200.21 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 | 31883 102562 | 10627 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1613568[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 | 38 | 31883 102561 | 10627 33 1157 35.1 | 0.000 % | c | 143 | 31872 102537 | 11689 137 3564 26.0 | 2.790 % | c ============================================================================== c [1mFound solution: 1596928[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 | 193 | 31890 102584 | 10630 187 5865 31.4 | 2.790 % | c | 294 | 31869 102530 | 11693 280 9886 35.3 | 2.875 % | c ============================================================================== c [1mFound solution: 1587328[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 | 344 | 31887 102579 | 10629 330 12609 38.2 | 2.875 % | c | 444 | 31887 102579 | 11691 430 16407 38.2 | 2.888 % | c | 594 | 31846 102488 | 12861 546 27567 50.5 | 3.061 % | c | 820 | 31825 102413 | 14147 770 33768 43.9 | 3.075 % | c ============================================================================== c [1mFound solution: 1577728[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 | 963 | 31837 102448 | 10612 912 39997 43.9 | 3.075 % | c | 1064 | 31837 102448 | 11673 1013 46227 45.6 | 3.116 % | c | 1215 | 31837 102448 | 12840 1164 68529 58.9 | 3.116 % | c | 1441 | 31826 102424 | 14124 1389 79179 57.0 | 3.160 % | c | 1779 | 31793 102328 | 15537 1724 91340 53.0 | 3.232 % | c | 2287 | 31793 102328 | 17090 2232 127232 57.0 | 3.232 % | c ============================================================================== c [1mFound solution: 1574528[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 | 2565 | 31811 102377 | 10603 2510 151065 60.2 | 3.232 % | c | 2666 | 31800 102353 | 11663 2610 151960 58.2 | 3.288 % | c | 2819 | 31800 102353 | 12829 2763 168910 61.1 | 3.288 % | c ============================================================================== c [1mFound solution: 1534848[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 | 2950 | 31799 102357 | 10599 2889 174053 60.2 | 3.288 % | c | 3050 | 31799 102357 | 11658 2989 178071 59.6 | 3.427 % | c | 3203 | 31799 102357 | 12824 3142 190049 60.5 | 3.427 % | c | 3429 | 31764 102274 | 14107 3362 202069 60.1 | 3.557 % | c | 3766 | 31759 102259 | 15517 3696 212478 57.5 | 3.571 % | c | 4272 | 31759 102259 | 17069 4202 274876 65.4 | 3.571 % | c | 5035 | 31759 102259 | 18776 4965 370051 74.5 | 3.571 % | c ============================================================================== c [1mFound solution: 1515008[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6125 | 31772 102292 | 10590 6055 470975 77.8 | 3.571 % | c | 6226 | 31772 102292 | 11649 6156 472186 76.7 | 3.584 % | c | 6377 | 31772 102292 | 12813 6307 483543 76.7 | 3.584 % | c | 6603 | 31772 102292 | 14095 6533 519287 79.5 | 3.584 % | c | 6943 | 31772 102292 | 15504 6873 532785 77.5 | 3.584 % | c | 7449 | 31767 102277 | 17055 7363 582180 79.1 | 3.598 % | c | 8209 | 31741 102200 | 18760 8119 655126 80.7 | 3.656 % | c | 9349 | 31699 102087 | 20636 9246 701059 75.8 | 3.800 % | c | 11058 | 31617 101902 | 22700 10940 902558 82.5 | 4.116 % | c ============================================================================== c [1mFound solution: 1511168[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11870 | 31606 101884 | 10535 11748 953485 81.2 | 4.116 % | c | 11970 | 31606 101884 | 11588 5974 395177 66.1 | 4.257 % | c | 12121 | 31606 101884 | 12747 6125 409181 66.8 | 4.257 % | c | 12347 | 31606 101884 | 14022 6351 419537 66.1 | 4.257 % | c | 12690 | 31606 101884 | 15424 6694 439539 65.7 | 4.257 % | c ============================================================================== c [1mFound solution: 1502848[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 | 12759 | 31617 101914 | 10539 6762 445694 65.9 | 4.257 % | c | 12859 | 31617 101914 | 11592 6862 448320 65.3 | 4.310 % | c | 13011 | 31617 101914 | 12752 7014 452122 64.5 | 4.310 % | c | 13236 | 31617 101914 | 14027 7239 490788 67.8 | 4.310 % | c | 13575 | 31617 101914 | 15430 7578 511781 67.5 | 4.310 % | c | 14082 | 31617 101914 | 16973 8085 594746 73.6 | 4.310 % | c | 14841 | 31610 101899 | 18670 8843 659185 74.5 | 4.339 % | c | 15981 | 31610 101899 | 20537 9983 726620 72.8 | 4.339 % | c | 17691 | 31565 101771 | 22591 11682 1003706 85.9 | 4.454 % | c ============================================================================== c [1mFound solution: 1477248[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 | 19430 | 31567 101781 | 10522 13418 1113496 83.0 | 4.454 % | c | 19531 | 31567 101781 | 11574 6810 480934 70.6 | 4.577 % | c | 19681 | 31546 101706 | 12731 6958 485984 69.8 | 4.592 % | c ============================================================================== c [1mFound solution: 1469568[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 | 19825 | 31538 101681 | 10512 7085 488771 69.0 | 4.592 % | c | 19925 | 31538 101681 | 11563 7185 490601 68.3 | 4.701 % | c | 20075 | 31538 101681 | 12719 7335 499855 68.1 | 4.701 % | c | 20300 | 31538 101681 | 13991 7560 528557 69.9 | 4.701 % | c | 20637 | 31502 101555 | 15390 7891 543718 68.9 | 4.744 % | c | 21147 | 31473 101477 | 16929 8388 579542 69.1 | 4.845 % | c | 21907 | 31473 101477 | 18622 9148 684665 74.8 | 4.845 % | c ============================================================================== c [1mFound solution: 1465728[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 | 22356 | 31458 101407 | 10486 9590 732744 76.4 | 4.845 % | c | 22457 | 31458 101407 | 11534 9691 742463 76.6 | 4.924 % | c ============================================================================== c [1mFound solution: 1443328[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 | 22542 | 31477 101456 | 10492 9776 750323 76.8 | 4.924 % | c | 22642 | 31477 101456 | 11541 9876 754215 76.4 | 4.935 % | c | 22793 | 31477 101456 | 12695 10027 782224 78.0 | 4.935 % | c | 23019 | 31415 101253 | 13964 10223 786431 76.9 | 5.035 % | c | 23356 | 31404 101229 | 15361 10559 811781 76.9 | 5.078 % | c | 23863 | 31393 101205 | 16897 11065 860086 77.7 | 5.121 % | c | 24622 | 31378 101152 | 18587 11820 890979 75.4 | 5.135 % | c | 25761 | 31378 101152 | 20445 12959 1015303 78.3 | 5.135 % | c | 27471 | 31378 101152 | 22490 14669 1181298 80.5 | 5.135 % | c ============================================================================== c [1mFound solution: 1431808[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 | 29653 | 31399 101201 | 10466 16849 1477790 87.7 | 5.135 % | c | 29754 | 31399 101201 | 11512 8526 641225 75.2 | 5.158 % | c | 29905 | 31390 101178 | 12663 8675 650420 75.0 | 5.186 % | c | 30132 | 31390 101178 | 13930 8902 666664 74.9 | 5.186 % | c | 30469 | 31390 101178 | 15323 9239 672768 72.8 | 5.186 % | c | 30975 | 31390 101178 | 16855 9745 763783 78.4 | 5.186 % | c | 31735 | 31390 101178 | 18541 10505 813475 77.4 | 5.186 % | c | 32876 | 31290 100920 | 20395 11618 901317 77.6 | 5.544 % | c | 34585 | 31290 100920 | 22434 13327 1165183 87.4 | 5.544 % | c | 37148 | 31202 100646 | 24678 15878 1471696 92.7 | 5.715 % | c | 40992 | 31161 100555 | 27146 19717 1846602 93.7 | 5.887 % | c | 46760 | 31156 100540 | 29860 25484 2469226 96.9 | 5.901 % | c ============================================================================== c [1mFound solution: 1429248[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46777 | 31175 100587 | 10391 25501 2471279 96.9 | 5.901 % | c ============================================================================== c [1mFound solution: 1423488[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46843 | 31192 100628 | 10397 6442 363817 56.5 | 5.901 % | c ============================================================================== c [1mFound solution: 1422208[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 | 46852 | 31216 100686 | 10405 6451 364632 56.5 | 5.901 % | c | 46953 | 31216 100686 | 11445 6552 376820 57.5 | 5.927 % | c | 47106 | 31216 100686 | 12590 6705 389588 58.1 | 5.927 % | c | 47333 | 31216 100686 | 13849 6932 415149 59.9 | 5.927 % | c | 47672 | 31216 100686 | 15233 7271 456768 62.8 | 5.927 % | c ============================================================================== c [1mFound solution: 1408128[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47867 | 31224 100708 | 10408 7463 475739 63.7 | 5.927 % | c | 47967 | 31224 100708 | 11448 7563 486414 64.3 | 5.992 % | c | 48117 | 31224 100708 | 12593 7713 510129 66.1 | 5.992 % | c | 48342 | 31224 100708 | 13853 7938 531836 67.0 | 5.992 % | c | 48680 | 31224 100708 | 15238 8276 562132 67.9 | 5.992 % | c | 49187 | 31224 100708 | 16762 8783 610844 69.5 | 5.992 % | c | 49946 | 31224 100708 | 18438 9542 712585 74.7 | 5.992 % | c | 51085 | 31219 100693 | 20282 10615 798793 75.3 | 6.006 % | c | 52793 | 31219 100693 | 22310 12323 1070504 86.9 | 6.006 % | c | 55355 | 31160 100486 | 24541 14882 1294947 87.0 | 6.092 % | c | 59199 | 31131 100412 | 26995 18716 1657683 88.6 | 6.191 % | c | 64965 | 31101 100337 | 29695 24473 2285411 93.4 | 6.291 % | c | 73614 | 31045 100213 | 32664 17437 1489263 85.4 | 6.519 % | c | 86592 | 31036 100182 | 35931 30403 2843663 93.5 | 6.533 % | c | 106054 | 31027 100151 | 39524 30469 2741050 90.0 | 6.547 % | c | 135247 | 30994 100072 | 43476 32841 3542567 107.9 | 6.675 % | c | 179036 | 30965 99981 | 47824 27424 2498435 91.1 | 6.732 % | #### 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.86 0.98 0.92 1/54 22614 Raw data (stat): 22614 (runsolver) R 22613 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 470341922 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99998 s] Raw data (loadavg): 0.88 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 1843 0 0 0 993 5 0 0 25 0 1 0 470341922 8929280 1773 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2180 1773 603 41 0 2139 0 vsize: 8720 [startup+20.0002 s] Raw data (loadavg): 0.90 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2326 0 0 0 1990 7 0 0 25 0 1 0 470341922 10936320 2256 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2670 2256 603 41 0 2629 0 vsize: 10680 [startup+30.001 s] Raw data (loadavg): 0.91 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2458 0 0 0 2990 7 0 0 25 0 1 0 470341922 11468800 2388 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2800 2388 603 41 0 2759 0 vsize: 11200 [startup+40.0012 s] Raw data (loadavg): 0.93 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2526 0 0 0 3989 8 0 0 25 0 1 0 470341922 11735040 2456 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2865 2456 603 41 0 2824 0 vsize: 11460 [startup+50.0026 s] Raw data (loadavg): 0.94 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2811 0 0 0 4989 8 0 0 25 0 1 0 470341922 12931072 2741 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3157 2741 603 41 0 3116 0 vsize: 12628 [startup+60.0033 s] Raw data (loadavg): 0.95 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2953 0 0 0 5988 9 0 0 25 0 1 0 470341922 13516800 2883 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3300 2883 603 41 0 3259 0 vsize: 13200 [startup+70.0036 s] Raw data (loadavg): 0.95 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3084 0 0 0 6987 9 0 0 25 0 1 0 470341922 14053376 3014 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3431 3014 603 41 0 3390 0 vsize: 13724 [startup+80.0048 s] Raw data (loadavg): 0.96 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3417 0 0 0 7984 11 0 0 25 0 1 0 470341922 15396864 3347 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3759 3347 603 41 0 3718 0 vsize: 15036 [startup+90.0054 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3736 0 0 0 8983 12 0 0 25 0 1 0 470341922 16732160 3666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4085 3666 603 41 0 4044 0 vsize: 16340 [startup+100.006 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3996 0 0 0 9982 13 0 0 25 0 1 0 470341922 17797120 3926 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4345 3926 603 41 0 4304 0 vsize: 17380 [startup+110.007 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 10982 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4444 4031 603 41 0 4403 0 vsize: 17776 [startup+120.008 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 11982 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4444 4031 603 41 0 4403 0 vsize: 17776 [startup+130.008 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 12983 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4444 4031 603 41 0 4403 0 vsize: 17776 [startup+140.008 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 13983 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4444 4031 603 41 0 4403 0 vsize: 17776 [startup+150.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 14983 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4444 4031 603 41 0 4403 0 vsize: 17776 [startup+160.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4245 0 0 0 15982 14 0 0 25 0 1 0 470341922 18747392 4175 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4577 4175 603 41 0 4536 0 vsize: 18308 [startup+170.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4701 0 0 0 16981 16 0 0 25 0 1 0 470341922 20615168 4631 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5033 4631 603 41 0 4992 0 vsize: 20132 [startup+180.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 17981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5198 4793 603 41 0 5157 0 vsize: 20792 [startup+190.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 18981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5198 4793 603 41 0 5157 0 vsize: 20792 [startup+200.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 19981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5198 4793 603 41 0 5157 0 vsize: 20792 [startup+210.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 20981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5198 4793 603 41 0 5157 0 vsize: 20792 [startup+220.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4990 0 0 0 21981 17 0 0 25 0 1 0 470341922 21958656 4920 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5361 4920 603 41 0 5320 0 vsize: 21444 [startup+230.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5320 0 0 0 22980 18 0 0 25 0 1 0 470341922 23289856 5250 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5686 5250 603 41 0 5645 0 vsize: 22744 [startup+240.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 23980 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5784 5344 603 41 0 5743 0 vsize: 23136 [startup+250.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 24981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5784 5344 603 41 0 5743 0 vsize: 23136 [startup+260.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 25981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5784 5344 603 41 0 5743 0 vsize: 23136 [startup+270.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 26981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5784 5344 603 41 0 5743 0 vsize: 23136 [startup+280.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 27981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5784 5344 603 41 0 5743 0 vsize: 23136 [startup+290.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 28981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5784 5344 603 41 0 5743 0 vsize: 23136 [startup+300.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 29981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5784 5344 603 41 0 5743 0 vsize: 23136 [startup+310.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5751 0 0 0 30981 19 0 0 25 0 1 0 470341922 25030656 5681 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6111 5681 603 41 0 6070 0 vsize: 24444 [startup+320.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6279 0 0 0 31980 20 0 0 25 0 1 0 470341922 27160576 6209 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6631 6209 603 41 0 6590 0 vsize: 26524 [startup+330.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 32979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6925 6508 603 41 0 6884 0 vsize: 27700 [startup+340.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 33979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6925 6508 603 41 0 6884 0 vsize: 27700 [startup+350.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 34979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223728 134558690 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6925 6508 603 41 0 6884 0 vsize: 27700 [startup+360.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 35979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6925 6508 603 41 0 6884 0 vsize: 27700 [startup+370.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6599 0 0 0 36979 21 0 0 25 0 1 0 470341922 28504064 6529 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6959 6529 603 41 0 6918 0 vsize: 27836 [startup+380.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6614 0 0 0 37979 21 0 0 25 0 1 0 470341922 28651520 6544 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6995 6544 603 41 0 6954 0 vsize: 27980 [startup+390.011 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6631 0 0 0 38979 21 0 0 25 0 1 0 470341922 28651520 6561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6995 6561 603 41 0 6954 0 vsize: 27980 [startup+400.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6649 0 0 0 39980 21 0 0 25 0 1 0 470341922 28798976 6579 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7031 6579 603 41 0 6990 0 vsize: 28124 [startup+410.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6669 0 0 0 40980 21 0 0 25 0 1 0 470341922 28798976 6599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7031 6599 603 41 0 6990 0 vsize: 28124 [startup+420.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6702 0 0 0 41979 21 0 0 25 0 1 0 470341922 29110272 6632 4294967295 134512640 134672761 3221224544 3221223600 134565096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7107 6632 603 41 0 7066 0 vsize: 28428 [startup+430.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6709 0 0 0 42979 22 0 0 25 0 1 0 470341922 29110272 6639 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6639 603 41 0 7066 0 vsize: 28428 [startup+440.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6721 0 0 0 43979 22 0 0 25 0 1 0 470341922 29110272 6651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6651 603 41 0 7066 0 vsize: 28428 [startup+450.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6735 0 0 0 44979 22 0 0 25 0 1 0 470341922 29274112 6665 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7147 6665 603 41 0 7106 0 vsize: 28588 [startup+460.012 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6764 0 0 0 45979 22 0 0 25 0 1 0 470341922 29437952 6694 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7187 6694 603 41 0 7146 0 vsize: 28748 [startup+470.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6836 0 0 0 46979 22 0 0 25 0 1 0 470341922 29700096 6766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7251 6766 603 41 0 7210 0 vsize: 29004 [startup+480.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7031 0 0 0 47979 23 0 0 25 0 1 0 470341922 30556160 6961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7460 6961 603 41 0 7419 0 vsize: 29840 [startup+490.013 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7217 0 0 0 48978 23 0 0 25 0 1 0 470341922 31367168 7147 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7658 7147 603 41 0 7617 0 vsize: 30632 [startup+500.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7403 0 0 0 49978 24 0 0 25 0 1 0 470341922 32186368 7333 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7858 7333 603 41 0 7817 0 vsize: 31432 [startup+510.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7586 0 0 0 50978 25 0 0 25 0 1 0 470341922 32985088 7516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8053 7516 603 41 0 8012 0 vsize: 32212 [startup+520.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7752 0 0 0 51977 25 0 0 25 0 1 0 470341922 33656832 7682 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8217 7682 603 41 0 8176 0 vsize: 32868 [startup+530.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7752 0 0 0 52977 25 0 0 25 0 1 0 470341922 33656832 7682 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8217 7682 603 41 0 8176 0 vsize: 32868 [startup+540.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7753 0 0 0 53977 25 0 0 25 0 1 0 470341922 33656832 7683 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8217 7683 603 41 0 8176 0 vsize: 32868 [startup+550.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7760 0 0 0 54978 25 0 0 25 0 1 0 470341922 33800192 7690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8252 7690 603 41 0 8211 0 vsize: 33008 [startup+560.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7768 0 0 0 55978 25 0 0 25 0 1 0 470341922 33800192 7698 4294967295 134512640 134672761 3221224544 3221223500 1075350544 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8252 7698 603 41 0 8211 0 vsize: 33008 [startup+570.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7768 0 0 0 56978 25 0 0 25 0 1 0 470341922 33800192 7698 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8252 7698 603 41 0 8211 0 vsize: 33008 [startup+580.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7773 0 0 0 57978 25 0 0 25 0 1 0 470341922 33800192 7703 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8252 7703 603 41 0 8211 0 vsize: 33008 [startup+590.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7778 0 0 0 58978 25 0 0 25 0 1 0 470341922 33800192 7708 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8252 7708 603 41 0 8211 0 vsize: 33008 [startup+600.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7807 0 0 0 59978 25 0 0 25 0 1 0 470341922 33964032 7737 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8292 7737 603 41 0 8251 0 vsize: 33168 [startup+610.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7839 0 0 0 60978 26 0 0 25 0 1 0 470341922 34127872 7769 4294967295 134512640 134672761 3221224544 3221223728 134558700 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8332 7769 603 41 0 8291 0 vsize: 33328 [startup+620.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7859 0 0 0 61978 26 0 0 25 0 1 0 470341922 34324480 7789 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8380 7789 603 41 0 8339 0 vsize: 33520 [startup+630.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7872 0 0 0 62979 26 0 0 25 0 1 0 470341922 34324480 7802 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8380 7802 603 41 0 8339 0 vsize: 33520 [startup+640.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7874 0 0 0 63979 26 0 0 25 0 1 0 470341922 34324480 7804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8380 7804 603 41 0 8339 0 vsize: 33520 [startup+650.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7892 0 0 0 64979 26 0 0 25 0 1 0 470341922 34488320 7822 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8420 7822 603 41 0 8379 0 vsize: 33680 [startup+660.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7903 0 0 0 65979 26 0 0 25 0 1 0 470341922 34488320 7833 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8420 7833 603 41 0 8379 0 vsize: 33680 [startup+670.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7955 0 0 0 66979 26 0 0 25 0 1 0 470341922 34816000 7885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8500 7885 603 41 0 8459 0 vsize: 34000 [startup+680.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8003 0 0 0 67979 26 0 0 25 0 1 0 470341922 35012608 7933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8548 7933 603 41 0 8507 0 vsize: 34192 [startup+690.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8016 0 0 0 68979 26 0 0 25 0 1 0 470341922 35012608 7946 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8548 7946 603 41 0 8507 0 vsize: 34192 [startup+700.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8021 0 0 0 69979 26 0 0 25 0 1 0 470341922 35012608 7951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8548 7951 603 41 0 8507 0 vsize: 34192 [startup+710.056 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8033 0 0 0 70984 26 0 0 25 0 1 0 470341922 35209216 7963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8596 7963 603 41 0 8555 0 vsize: 34384 [startup+720.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8079 0 0 0 71984 26 0 0 25 0 1 0 470341922 35405824 8009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8644 8009 603 41 0 8603 0 vsize: 34576 [startup+730.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8092 0 0 0 72984 26 0 0 25 0 1 0 470341922 35405824 8022 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8644 8022 603 41 0 8603 0 vsize: 34576 [startup+740.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8092 0 0 0 73984 26 0 0 25 0 1 0 470341922 35405824 8022 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8644 8022 603 41 0 8603 0 vsize: 34576 [startup+750.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8094 0 0 0 74984 26 0 0 25 0 1 0 470341922 35405824 8024 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8644 8024 603 41 0 8603 0 vsize: 34576 [startup+760.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8094 0 0 0 75984 26 0 0 25 0 1 0 470341922 35405824 8024 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8644 8024 603 41 0 8603 0 vsize: 34576 [startup+770.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8095 0 0 0 76984 26 0 0 25 0 1 0 470341922 35405824 8025 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8644 8025 603 41 0 8603 0 vsize: 34576 [startup+780.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8104 0 0 0 77984 26 0 0 25 0 1 0 470341922 35602432 8034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8692 8034 603 41 0 8651 0 vsize: 34768 [startup+790.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8115 0 0 0 78984 26 0 0 25 0 1 0 470341922 35602432 8045 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8692 8045 603 41 0 8651 0 vsize: 34768 [startup+800.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8134 0 0 0 79985 26 0 0 25 0 1 0 470341922 35799040 8064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8740 8064 603 41 0 8699 0 vsize: 34960 [startup+810.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8153 0 0 0 80985 26 0 0 25 0 1 0 470341922 35799040 8083 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8740 8083 603 41 0 8699 0 vsize: 34960 [startup+820.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8155 0 0 0 81985 26 0 0 25 0 1 0 470341922 35799040 8085 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8740 8085 603 41 0 8699 0 vsize: 34960 [startup+830.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8167 0 0 0 82985 26 0 0 25 0 1 0 470341922 35995648 8097 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8788 8097 603 41 0 8747 0 vsize: 35152 [startup+840.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8168 0 0 0 83985 26 0 0 25 0 1 0 470341922 35995648 8098 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8788 8098 603 41 0 8747 0 vsize: 35152 [startup+850.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8182 0 0 0 84985 26 0 0 25 0 1 0 470341922 35995648 8112 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8788 8112 603 41 0 8747 0 vsize: 35152 [startup+860.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8183 0 0 0 85985 26 0 0 25 0 1 0 470341922 35995648 8113 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8788 8113 603 41 0 8747 0 vsize: 35152 [startup+870.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8183 0 0 0 86986 26 0 0 25 0 1 0 470341922 35995648 8113 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8788 8113 603 41 0 8747 0 vsize: 35152 [startup+880.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8205 0 0 0 87986 27 0 0 25 0 1 0 470341922 36192256 8135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8836 8135 603 41 0 8795 0 vsize: 35344 [startup+890.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8245 0 0 0 88986 27 0 0 25 0 1 0 470341922 36388864 8175 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8884 8175 603 41 0 8843 0 vsize: 35536 [startup+900.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8261 0 0 0 89986 27 0 0 25 0 1 0 470341922 36388864 8191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8884 8191 603 41 0 8843 0 vsize: 35536 [startup+910.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8265 0 0 0 90986 27 0 0 25 0 1 0 470341922 36388864 8195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8884 8195 603 41 0 8843 0 vsize: 35536 [startup+920.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8278 0 0 0 91986 27 0 0 25 0 1 0 470341922 36388864 8208 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8884 8208 603 41 0 8843 0 vsize: 35536 [startup+930.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8290 0 0 0 92987 27 0 0 25 0 1 0 470341922 36388864 8220 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8884 8220 603 41 0 8843 0 vsize: 35536 [startup+940.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8308 0 0 0 93987 27 0 0 25 0 1 0 470341922 36585472 8238 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8932 8238 603 41 0 8891 0 vsize: 35728 [startup+950.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8314 0 0 0 94987 27 0 0 25 0 1 0 470341922 36585472 8244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8932 8244 603 41 0 8891 0 vsize: 35728 [startup+960.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8321 0 0 0 95987 27 0 0 25 0 1 0 470341922 36585472 8251 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8932 8251 603 41 0 8891 0 vsize: 35728 [startup+970.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8321 0 0 0 96987 27 0 0 25 0 1 0 470341922 36585472 8251 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8932 8251 603 41 0 8891 0 vsize: 35728 [startup+980.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8329 0 0 0 97987 27 0 0 25 0 1 0 470341922 36585472 8259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8932 8259 603 41 0 8891 0 vsize: 35728 [startup+990.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8339 0 0 0 98988 27 0 0 25 0 1 0 470341922 36585472 8269 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8932 8269 603 41 0 8891 0 vsize: 35728 [startup+1000.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8350 0 0 0 99988 27 0 0 25 0 1 0 470341922 36773888 8280 4294967295 134512640 134672761 3221224544 3221223728 134558671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8978 8280 603 41 0 8937 0 vsize: 35912 [startup+1010.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8350 0 0 0 100988 27 0 0 25 0 1 0 470341922 36773888 8280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8978 8280 603 41 0 8937 0 vsize: 35912 [startup+1020.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8364 0 0 0 101988 27 0 0 25 0 1 0 470341922 36773888 8294 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8978 8294 603 41 0 8937 0 vsize: 35912 [startup+1030.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8366 0 0 0 102988 27 0 0 25 0 1 0 470341922 36773888 8296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8978 8296 603 41 0 8937 0 vsize: 35912 [startup+1040.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8380 0 0 0 103988 27 0 0 25 0 1 0 470341922 36773888 8310 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8978 8310 603 41 0 8937 0 vsize: 35912 [startup+1050.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8383 0 0 0 104988 27 0 0 25 0 1 0 470341922 36773888 8313 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8978 8313 603 41 0 8937 0 vsize: 35912 [startup+1060.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8395 0 0 0 105988 27 0 0 25 0 1 0 470341922 36970496 8325 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 8325 603 41 0 8985 0 vsize: 36104 [startup+1070.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8398 0 0 0 106988 27 0 0 25 0 1 0 470341922 36970496 8328 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 8328 603 41 0 8985 0 vsize: 36104 [startup+1080.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8404 0 0 0 107989 27 0 0 25 0 1 0 470341922 36970496 8334 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 8334 603 41 0 8985 0 vsize: 36104 [startup+1090.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8429 0 0 0 108989 27 0 0 25 0 1 0 470341922 36970496 8359 4294967295 134512640 134672761 3221224544 3221223648 134560390 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 8359 603 41 0 8985 0 vsize: 36104 [startup+1100.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8439 0 0 0 109989 27 0 0 25 0 1 0 470341922 36970496 8369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 8369 603 41 0 8985 0 vsize: 36104 [startup+1110.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8470 0 0 0 110989 28 0 0 25 0 1 0 470341922 37167104 8400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8400 603 41 0 9033 0 vsize: 36296 [startup+1120.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8499 0 0 0 111989 28 0 0 25 0 1 0 470341922 37167104 8429 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8429 603 41 0 9033 0 vsize: 36296 [startup+1130.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 112989 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8437 603 41 0 9033 0 vsize: 36296 [startup+1140.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 113989 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8437 603 41 0 9033 0 vsize: 36296 [startup+1150.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 114990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8437 603 41 0 9033 0 vsize: 36296 [startup+1160.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 115990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8437 603 41 0 9033 0 vsize: 36296 [startup+1170.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 116990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8437 603 41 0 9033 0 vsize: 36296 [startup+1180.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 117990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8437 603 41 0 9033 0 vsize: 36296 [startup+1190.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 118990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9074 8437 603 41 0 9033 0 vsize: 36296 [startup+1200.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 22614 Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8518 0 0 0 119990 28 0 0 25 0 1 0 470341922 37363712 8448 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9122 8448 603 41 0 9081 0 vsize: 36488 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.98 0.92 1/54 22614 Raw data (stat): 22614 (minisat+) Z 22613 26667 26666 0 -1 12 8521 0 0 0 119990 29 0 0 25 0 1 0 470341922 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.08 CPU time (s): 1200.21 CPU user time (s): 1199.91 CPU system time (s): 0.298954 CPU usage (%): 100.011 Max. virtual memory (Kb): 36488 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####