Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0201.opb |
MD5SUM | ffa3a55eb53181880328dd1b84f91e66 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1523 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 201 |
Biggest coefficient in the objective function | 1920 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 19980 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 1920 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 19980 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02184 |
Number of variables | 201 |
Total number of constraints | 334 |
Number of constraints which are clauses | 20 |
Number of constraints which are cardinality constraints (but not clauses) | 227 |
Number of constraints which are nor clauses,nor cardinality constraints | 87 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 67 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-21 17:40:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17121 boxname=wulflinc22 idbench=1317 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ffa3a55eb53181880328dd1b84f91e66 /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0201.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0201.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0201.opb IDLAUNCH: 17121 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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 : 3 cpu MHz : 451.031 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: 347744 kB Buffers: 30488 kB Cached: 627800 kB SwapCached: 20 kB Active: 118420 kB Inactive: 542556 kB HighTotal: 131008 kB HighFree: 7756 kB LowTotal: 903652 kB LowFree: 339988 kB SwapTotal: 2097892 kB SwapFree: 2097664 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6640 kB Slab: 20252 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 18:00:55 (client local time) WITH STATUS 10 IN 1200.2 SECONDS stats: 17121 7 1200.2 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 133 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): sssss c ---[ 137]---> BDD-cost: 3 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 15 c ---[ 131]---> BDD-cost: 15 c ---[ 129]---> BDD-cost: 15 c ---[ 127]---> BDD-cost: 15 c ---[ 125]---> BDD-cost: 15 c ---[ 123]---> BDD-cost: 15 c ---[ 121]---> BDD-cost: 15 c ---[ 119]---> BDD-cost: 15 c ---[ 117]---> BDD-cost: 15 c ---[ 115]---> BDD-cost: 15 c ---[ 113]---> BDD-cost: 15 c ---[ 111]---> BDD-cost: 15 c ---[ 109]---> BDD-cost: 15 c ---[ 107]---> BDD-cost: 15 c ---[ 105]---> BDD-cost: 15 c ---[ 103]---> BDD-cost: 15 c ---[ 101]---> BDD-cost: 15 c ---[ 99]---> BDD-cost: 15 c ---[ 97]---> BDD-cost: 15 c ---[ 95]---> BDD-cost: 15 c ---[ 89]---> BDD-cost: 39 c ---[ 88]---> BDD-cost: 42 c ---[ 87]---> BDD-cost: 42 c ---[ 86]---> BDD-cost: 54 c ---[ 85]---> BDD-cost: 73 c ---[ 84]---> BDD-cost: 73 c ---[ 83]---> BDD-cost: 98 c ---[ 82]---> BDD-cost: 85 c ---[ 81]---> BDD-cost: 85 c ---[ 80]---> BDD-cost: 160 c ---[ 79]---> BDD-cost: 107 c ---[ 78]---> BDD-cost: 107 c ---[ 77]---> BDD-cost: 201 c ---[ 76]---> BDD-cost: 128 c ---[ 75]---> BDD-cost: 128 c ---[ 74]---> BDD-cost: 241 c ---[ 73]---> BDD-cost: 150 c ---[ 72]---> BDD-cost: 150 c ---[ 71]---> BDD-cost: 281 c ---[ 70]---> BDD-cost: 172 c ---[ 69]---> BDD-cost: 172 c ---[ 68]---> BDD-cost: 321 c ---[ 67]---> BDD-cost: 194 c ---[ 66]---> BDD-cost: 194 c ---[ 65]---> BDD-cost: 361 c ---[ 64]---> BDD-cost: 3 c ---[ 63]---> BDD-cost: 3 c ---[ 62]---> BDD-cost: 3 c ---[ 61]---> BDD-cost: 3 c ---[ 60]---> BDD-cost: 3 c ---[ 59]---> BDD-cost: 3 c ---[ 58]---> BDD-cost: 9 c ---[ 57]---> BDD-cost: 11 c ---[ 56]---> BDD-cost: 11 c ---[ 55]---> BDD-cost: 9 c ---[ 54]---> BDD-cost: 11 c ---[ 53]---> BDD-cost: 11 c ---[ 52]---> BDD-cost: 9 c ---[ 51]---> BDD-cost: 11 c ---[ 50]---> BDD-cost: 11 c ---[ 49]---> BDD-cost: 9 c ---[ 48]---> BDD-cost: 11 c ---[ 47]---> BDD-cost: 11 c ---[ 46]---> BDD-cost: 9 c ---[ 45]---> BDD-cost: 11 c ---[ 44]---> BDD-cost: 11 c ---[ 43]---> BDD-cost: 9 c ---[ 42]---> BDD-cost: 11 c ---[ 41]---> BDD-cost: 11 c ---[ 40]---> BDD-cost: 9 c ---[ 39]---> BDD-cost: 11 c ---[ 38]---> BDD-cost: 11 c ---[ 37]---> BDD-cost: 9 c ---[ 36]---> BDD-cost: 11 c ---[ 35]---> BDD-cost: 11 c ---[ 34]---> BDD-cost: 9 c ---[ 33]---> BDD-cost: 11 c ---[ 32]---> BDD-cost: 11 c ---[ 31]---> BDD-cost: 9 c ---[ 30]---> BDD-cost: 11 c ---[ 29]---> BDD-cost: 11 c ---[ 28]---> BDD-cost: 9 c ---[ 27]---> BDD-cost: 11 c ---[ 26]---> BDD-cost: 11 c ---[ 25]---> BDD-cost: 9 c ---[ 24]---> BDD-cost: 11 c ---[ 23]---> BDD-cost: 11 c ---[ 22]---> BDD-cost: 9 c ---[ 21]---> BDD-cost: 11 c ---[ 20]---> BDD-cost: 11 c ---[ 19]---> BDD-cost: 9 c ---[ 18]---> BDD-cost: 11 c ---[ 17]---> BDD-cost: 11 c ---[ 16]---> BDD-cost: 9 c ---[ 15]---> BDD-cost: 11 c ---[ 14]---> BDD-cost: 11 c ---[ 13]---> BDD-cost: 9 c ---[ 12]---> BDD-cost: 11 c ---[ 11]---> BDD-cost: 11 c ---[ 10]---> BDD-cost: 9 c ---[ 9]---> BDD-cost: 11 c ---[ 8]---> BDD-cost: 11 c ---[ 7]---> BDD-cost: 9 c ---[ 6]---> BDD-cost: 11 c ---[ 5]---> BDD-cost: 11 c ---[ 4]---> BDD-cost: 1 c ---[ 3]---> BDD-cost: 1 c ---[ 2]---> BDD-cost: 1 c ---[ 1]---> BDD-cost: 1 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 23540 68455 | 7846 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 2734[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:21097 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7 | 78351 196805 | 26117 3 60 20.0 | 0.000 % | c ============================================================================== c [1mFound solution: 2329[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106 | 77002 193861 | 25667 84 1079 12.8 | 0.000 % | c ============================================================================== c [1mFound solution: 2304[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118 | 77013 193888 | 25671 96 1193 12.4 | 0.000 % | c | 218 | 76399 192474 | 28238 185 3409 18.4 | 4.161 % | c | 368 | 75394 190171 | 31061 323 4790 14.8 | 5.253 % | c | 594 | 71969 182251 | 34168 514 8965 17.4 | 9.788 % | c ============================================================================== c [1mFound solution: 2283[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 822 | 71047 180141 | 23682 720 13788 19.1 | 9.788 % | c | 922 | 70655 179234 | 26050 817 14502 17.8 | 11.766 % | c | 1072 | 70585 179073 | 28655 965 17039 17.7 | 11.866 % | c | 1300 | 70578 179052 | 31520 1190 21713 18.2 | 11.871 % | c ============================================================================== c [1mFound solution: 2225[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1454 | 70707 179370 | 23569 1344 24163 18.0 | 11.871 % | c ============================================================================== c [1mFound solution: 2191[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1457 | 70723 179410 | 23574 1347 24215 18.0 | 11.871 % | c | 1557 | 70723 179410 | 25931 1447 26069 18.0 | 11.918 % | c | 1707 | 70609 179152 | 28524 1574 27094 17.2 | 12.052 % | c | 1932 | 70609 179152 | 31376 1799 30446 16.9 | 12.053 % | c | 2270 | 70196 178201 | 34514 2121 32259 15.2 | 12.597 % | c ============================================================================== c [1mFound solution: 2179[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2277 | 70204 178221 | 23401 2128 32301 15.2 | 12.597 % | c | 2377 | 69756 177173 | 25741 2223 34819 15.7 | 13.223 % | c | 2527 | 68491 174206 | 28315 2347 38087 16.2 | 14.893 % | c ============================================================================== c [1mFound solution: 2173[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2595 | 67333 171523 | 22444 2401 38686 16.1 | 14.893 % | c | 2697 | 66571 169748 | 24688 2488 39496 15.9 | 17.501 % | c ============================================================================== c [1mFound solution: 2028[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2811 | 66573 169763 | 22191 2601 41964 16.1 | 17.501 % | c | 2912 | 66338 169218 | 24410 2687 43291 16.1 | 18.031 % | c ============================================================================== c [1mFound solution: 1924[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2988 | 65410 167073 | 21803 2746 43707 15.9 | 18.031 % | c | 3089 | 63386 162376 | 23983 2799 47959 17.1 | 21.953 % | c | 3239 | 63386 162376 | 26381 2949 62040 21.0 | 21.953 % | c | 3464 | 63386 162376 | 29019 3174 74050 23.3 | 21.953 % | c | 3803 | 61775 158616 | 31921 3446 76816 22.3 | 24.199 % | c | 4309 | 61422 157788 | 35113 3935 116814 29.7 | 24.657 % | c ============================================================================== c [1mFound solution: 1921[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4647 | 61453 157868 | 20484 4273 137525 32.2 | 24.657 % | c | 4750 | 61453 157868 | 22532 4376 140697 32.2 | 24.650 % | c | 4901 | 61453 157868 | 24785 4527 145200 32.1 | 24.650 % | c | 5127 | 61453 157868 | 27264 4753 151738 31.9 | 24.650 % | c | 5465 | 61349 157629 | 29990 5053 154257 30.5 | 24.780 % | c | 5971 | 61349 157629 | 32989 5559 167280 30.1 | 24.780 % | c ============================================================================== c [1mFound solution: 1907[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6178 | 61445 157865 | 20481 5766 175207 30.4 | 24.780 % | c | 6278 | 61232 157240 | 22529 5852 177409 30.3 | 24.977 % | c ============================================================================== c [1mFound solution: 1891[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6404 | 61201 157162 | 20400 5976 181572 30.4 | 24.977 % | c | 6506 | 61194 157141 | 22440 6076 186499 30.7 | 25.023 % | c | 6656 | 61174 157085 | 24684 6223 189898 30.5 | 25.040 % | c | 6881 | 60935 156508 | 27152 6427 193656 30.1 | 25.385 % | c | 7220 | 60725 156017 | 29867 6650 200513 30.2 | 25.635 % | c ============================================================================== c [1mFound solution: 1889[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7349 | 60733 156037 | 20244 6779 203446 30.0 | 25.635 % | c | 7450 | 60733 156037 | 22268 6880 205758 29.9 | 25.635 % | c | 7601 | 60728 156022 | 24495 7030 208603 29.7 | 25.640 % | c | 7827 | 60728 156022 | 26944 7256 213972 29.5 | 25.640 % | c | 8165 | 60551 155604 | 29639 7565 221473 29.3 | 25.877 % | c | 8671 | 60156 154619 | 32603 8053 252963 31.4 | 26.338 % | c | 9430 | 60004 154263 | 35863 8790 286402 32.6 | 26.540 % | c | 10571 | 59190 152376 | 39449 9881 315307 31.9 | 27.643 % | c | 12280 | 59107 152160 | 43394 11583 357293 30.8 | 27.729 % | c ============================================================================== c [1mFound solution: 1882[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12915 | 58997 151868 | 19665 12200 370350 30.4 | 27.729 % | c | 13015 | 58997 151868 | 21631 12300 372395 30.3 | 27.856 % | c | 13167 | 58958 151778 | 23794 12440 374194 30.1 | 27.912 % | c | 13392 | 58831 151484 | 26174 12656 375759 29.7 | 28.076 % | c ============================================================================== c [1mFound solution: 1879[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13486 | 58087 149754 | 19362 12598 375795 29.8 | 28.076 % | c | 13588 | 58087 149754 | 21298 12700 377802 29.7 | 29.115 % | c | 13741 | 58087 149754 | 23428 12853 387259 30.1 | 29.115 % | c | 13966 | 58087 149754 | 25770 13078 393630 30.1 | 29.115 % | c | 14306 | 58087 149754 | 28347 13418 400516 29.8 | 29.115 % | c | 14812 | 58087 149754 | 31182 13924 439892 31.6 | 29.115 % | c | 15571 | 57870 149241 | 34300 14673 454378 31.0 | 29.399 % | c | 16710 | 57870 149241 | 37731 15812 474459 30.0 | 29.399 % | c | 18418 | 57134 147529 | 41504 17423 574127 33.0 | 30.441 % | c | 20981 | 57134 147529 | 45654 19986 723332 36.2 | 30.441 % | c ============================================================================== c [1mFound solution: 1857[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21095 | 57151 147572 | 19050 20100 728049 36.2 | 30.441 % | c | 21195 | 57130 147525 | 20955 20195 730320 36.2 | 30.465 % | c | 21346 | 57130 147525 | 23050 20346 734030 36.1 | 30.465 % | c ============================================================================== c [1mFound solution: 1851[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21570 | 57125 147513 | 19041 20563 743827 36.2 | 30.465 % | c ============================================================================== c [1mFound solution: 1847[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21634 | 57128 147520 | 19042 20627 745630 36.1 | 30.465 % | c | 21737 | 57128 147520 | 20946 20730 751945 36.3 | 30.471 % | c | 21888 | 57045 147328 | 23040 20877 755676 36.2 | 30.574 % | c | 22114 | 57045 147328 | 25344 21103 766990 36.3 | 30.574 % | c | 22453 | 57020 147272 | 27879 21438 786878 36.7 | 30.604 % | c | 22959 | 57020 147272 | 30667 21944 826660 37.7 | 30.604 % | c ============================================================================== c [1mFound solution: 1845[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23563 | 56971 147158 | 18990 22547 891231 39.5 | 30.604 % | c | 23666 | 56971 147158 | 20889 22650 893152 39.4 | 30.675 % | c | 23817 | 56971 147158 | 22977 22801 895145 39.3 | 30.675 % | c | 24042 | 56971 147158 | 25275 23026 906809 39.4 | 30.675 % | c | 24379 | 56971 147158 | 27803 23363 937813 40.1 | 30.675 % | c | 24887 | 56669 146466 | 30583 23864 973509 40.8 | 31.071 % | c ============================================================================== c [1mFound solution: 1827[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25018 | 56676 146483 | 18892 23995 978086 40.8 | 31.071 % | c | 25118 | 56676 146483 | 20781 24095 981131 40.7 | 31.071 % | c | 25269 | 56676 146483 | 22859 24246 989880 40.8 | 31.071 % | c | 25495 | 56676 146483 | 25145 24472 1001050 40.9 | 31.071 % | c | 25832 | 56313 145647 | 27659 24774 1023643 41.3 | 31.575 % | c ============================================================================== c [1mFound solution: 1819[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25914 | 56316 145654 | 18772 24856 1031106 41.5 | 31.575 % | c | 26016 | 56316 145654 | 20649 24958 1032870 41.4 | 31.576 % | c | 26169 | 56316 145654 | 22714 25111 1046447 41.7 | 31.576 % | c | 26394 | 56316 145654 | 24985 25336 1064844 42.0 | 31.576 % | c | 26731 | 56292 145598 | 27484 25672 1075820 41.9 | 31.602 % | c | 27238 | 56233 145459 | 30232 26178 1098939 42.0 | 31.680 % | c | 27999 | 56159 145237 | 33255 26934 1182332 43.9 | 31.736 % | c | 29141 | 56159 145237 | 36581 28076 1252716 44.6 | 31.736 % | c | 30849 | 56150 145214 | 40239 29782 1351975 45.4 | 31.744 % | c ============================================================================== c [1mFound solution: 1789[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33214 | 56187 145307 | 18729 32147 1526468 47.5 | 31.744 % | c | 33314 | 56187 145307 | 20601 16174 791453 48.9 | 31.735 % | c | 33465 | 56187 145307 | 22662 16325 795339 48.7 | 31.735 % | c | 33690 | 56187 145307 | 24928 16550 811934 49.1 | 31.735 % | c | 34027 | 56187 145307 | 27421 16887 823519 48.8 | 31.735 % | c ============================================================================== c [1mFound solution: 1779[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34130 | 56203 145347 | 18734 16990 827111 48.7 | 31.735 % | c | 34232 | 56203 145347 | 20607 17092 838120 49.0 | 31.733 % | c | 34383 | 56203 145347 | 22668 17243 842134 48.8 | 31.733 % | c ============================================================================== c [1mFound solution: 1778[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34597 | 56213 145371 | 18737 17457 872147 50.0 | 31.733 % | c | 34697 | 56205 145353 | 20610 17555 873761 49.8 | 31.740 % | c | 34847 | 56163 145256 | 22671 17697 875346 49.5 | 31.796 % | c | 35074 | 55614 143980 | 24938 17713 880296 49.7 | 32.527 % | c | 35411 | 55614 143980 | 27432 18050 891405 49.4 | 32.527 % | c | 35920 | 55614 143980 | 30176 18559 929733 50.1 | 32.527 % | c | 36681 | 55614 143980 | 33193 19320 983705 50.9 | 32.527 % | c | 37820 | 55614 143980 | 36513 20459 1065761 52.1 | 32.527 % | c ============================================================================== c [1mFound solution: 1771[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39153 | 55618 143990 | 18539 21792 1168350 53.6 | 32.527 % | c | 39254 | 55618 143990 | 20392 21893 1171941 53.5 | 32.528 % | c | 39409 | 55618 143990 | 22432 22048 1182758 53.6 | 32.528 % | c | 39634 | 55618 143990 | 24675 22273 1190256 53.4 | 32.528 % | c | 39971 | 55618 143990 | 27142 22610 1198970 53.0 | 32.528 % | c | 40478 | 55618 143990 | 29857 23117 1241336 53.7 | 32.528 % | c | 41238 | 55443 143587 | 32842 23871 1300327 54.5 | 32.760 % | c | 42377 | 55436 143566 | 36127 25007 1332385 53.3 | 32.765 % | c | 44085 | 55436 143566 | 39739 26715 1385367 51.9 | 32.765 % | c | 46647 | 55427 143543 | 43713 29276 1512944 51.7 | 32.773 % | c ============================================================================== c [1mFound solution: 1761[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48332 | 55435 143563 | 18478 30961 1620159 52.3 | 32.773 % | c | 48432 | 55435 143563 | 20325 15581 569217 36.5 | 32.773 % | c | 48583 | 55435 143563 | 22358 15732 576354 36.6 | 32.773 % | c | 48809 | 55435 143563 | 24594 15958 586916 36.8 | 32.773 % | c ============================================================================== c [1mFound solution: 1751[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49011 | 55440 143576 | 18480 16160 598362 37.0 | 32.773 % | c | 49113 | 55440 143576 | 20328 16262 600587 36.9 | 32.775 % | c | 49263 | 55440 143576 | 22360 16412 615724 37.5 | 32.775 % | c | 49489 | 55433 143555 | 24596 16636 623173 37.5 | 32.779 % | c | 49828 | 55433 143555 | 27056 16975 630918 37.2 | 32.779 % | c | 50335 | 55433 143555 | 29762 17482 641582 36.7 | 32.779 % | c | 51094 | 55424 143532 | 32738 18238 662543 36.3 | 32.788 % | c | 52233 | 55290 143205 | 36012 19369 727221 37.5 | 32.951 % | c | 53942 | 55283 143184 | 39613 21074 777289 36.9 | 32.955 % | c ============================================================================== c [1mFound solution: 1730[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 55465 | 55305 143238 | 18435 22597 906318 40.1 | 32.955 % | c | 55565 | 55073 142698 | 20278 22684 907310 40.0 | 33.250 % | c | 55716 | 54831 142145 | 22306 22812 916789 40.2 | 33.556 % | c | 55941 | 54831 142145 | 24536 23037 931838 40.4 | 33.555 % | c | 56279 | 54686 141799 | 26990 23355 940703 40.3 | 33.749 % | c | 56786 | 54679 141778 | 29689 23860 965722 40.5 | 33.753 % | c | 57547 | 54679 141778 | 32658 24621 993342 40.3 | 33.753 % | c | 58686 | 54584 141534 | 35924 25756 1053248 40.9 | 33.869 % | c | 60394 | 54584 141534 | 39517 27464 1209356 44.0 | 33.869 % | c | 62956 | 54579 141519 | 43468 30024 1362239 45.4 | 33.873 % | c ============================================================================== c [1mFound solution: 1709[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 63218 | 54585 141533 | 18195 30286 1374583 45.4 | 33.873 % | c | 63318 | 54585 141533 | 20014 15243 636385 41.7 | 33.873 % | c | 63468 | 54585 141533 | 22015 15393 643684 41.8 | 33.873 % | c | 63693 | 54585 141533 | 24217 15618 663543 42.5 | 33.873 % | c | 64033 | 54585 141533 | 26639 15958 689700 43.2 | 33.873 % | c | 64540 | 54569 141485 | 29303 16462 710848 43.2 | 33.886 % | c | 65299 | 54556 141448 | 32233 17219 746818 43.4 | 33.899 % | c | 66438 | 54556 141448 | 35456 18358 860808 46.9 | 33.899 % | c | 68149 | 54556 141448 | 39002 20069 969043 48.3 | 33.899 % | c ============================================================================== c [1mFound solution: 1708[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69591 | 54563 141465 | 18187 21511 1057309 49.2 | 33.899 % | c | 69692 | 54483 141280 | 20005 21601 1058935 49.0 | 34.011 % | c | 69842 | 54483 141280 | 22006 21751 1067573 49.1 | 34.010 % | c | 70069 | 54483 141280 | 24206 21978 1078942 49.1 | 34.010 % | c | 70407 | 54483 141280 | 26627 22316 1102923 49.4 | 34.010 % | c | 70914 | 54474 141257 | 29290 22820 1129045 49.5 | 34.019 % | c | 71677 | 54192 140581 | 32219 23569 1181684 50.1 | 34.380 % | c | 72817 | 54170 140523 | 35441 24706 1248961 50.6 | 34.401 % | c ============================================================================== c [1mFound solution: 1704[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 73953 | 54176 140537 | 18058 25842 1331297 51.5 | 34.401 % | c | 74054 | 54176 140537 | 19863 25943 1334005 51.4 | 34.401 % | c | 74205 | 54168 140515 | 21850 26093 1343025 51.5 | 34.410 % | c | 74431 | 54168 140515 | 24035 26319 1348240 51.2 | 34.410 % | c | 74769 | 54168 140515 | 26438 26657 1359724 51.0 | 34.410 % | c | 75275 | 53782 139616 | 29082 27138 1367750 50.4 | 34.929 % | c | 76034 | 53666 139350 | 31990 27883 1422181 51.0 | 35.080 % | c | 77175 | 53666 139350 | 35189 29024 1499346 51.7 | 35.080 % | c | 78883 | 53661 139335 | 38708 30729 1570989 51.1 | 35.084 % | c ============================================================================== c [1mFound solution: 1701[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 79115 | 53667 139349 | 17889 30961 1595829 51.5 | 35.084 % | c | 79216 | 53667 139349 | 19677 15582 557033 35.7 | 35.084 % | c | 79372 | 53667 139349 | 21645 15738 564117 35.8 | 35.084 % | c | 79597 | 53667 139349 | 23810 15963 575906 36.1 | 35.084 % | c | 79934 | 53667 139349 | 26191 16300 596618 36.6 | 35.084 % | c | 80440 | 53667 139349 | 28810 16806 637980 38.0 | 35.084 % | c ============================================================================== c [1mFound solution: 1681[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 80786 | 53694 139418 | 17898 17152 669439 39.0 | 35.084 % | c | 80886 | 53694 139418 | 19687 17252 674169 39.1 | 35.074 % | c | 81036 | 53694 139418 | 21656 17402 682240 39.2 | 35.074 % | c | 81261 | 53694 139418 | 23822 17627 692778 39.3 | 35.074 % | c | 81598 | 53694 139418 | 26204 17964 707014 39.4 | 35.074 % | c | 82105 | 53694 139418 | 28824 18471 734735 39.8 | 35.074 % | c | 82864 | 53694 139418 | 31707 19230 761208 39.6 | 35.074 % | c | 84004 | 53694 139418 | 34878 20370 807262 39.6 | 35.074 % | c | 85713 | 53636 139247 | 38365 22064 869533 39.4 | 35.122 % | c | 88275 | 53636 139247 | 42202 24626 1028052 41.7 | 35.122 % | c | 92123 | 53636 139247 | 46422 28474 1285993 45.2 | 35.122 % | c | 97889 | 53636 139247 | 51065 34240 1645858 48.1 | 35.122 % | c ============================================================================== c [1mFound solution: 1679[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 101348 | 53649 139280 | 17883 37699 1869282 49.6 | 35.122 % | c | 101449 | 53649 139280 | 19671 17648 788473 44.7 | 35.120 % | c | 101599 | 53649 139280 | 21638 17798 798338 44.9 | 35.120 % | c | 101824 | 53464 138850 | 23802 18006 806059 44.8 | 35.373 % | c | 102161 | 53464 138850 | 26182 18343 820610 44.7 | 35.373 % | c | 102669 | 53464 138850 | 28800 18851 828169 43.9 | 35.373 % | c | 103428 | 53433 138779 | 31680 19608 854709 43.6 | 35.416 % | c | 104567 | 53433 138779 | 34848 20747 909381 43.8 | 35.416 % | c | 106275 | 53433 138779 | 38333 22455 981995 43.7 | 35.416 % | c | 108839 | 53409 138709 | 42167 25013 1091899 43.7 | 35.438 % | c ============================================================================== c [1mFound solution: 1675[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 111459 | 53417 138729 | 17805 27633 1215412 44.0 | 35.438 % | c | 111560 | 53417 138729 | 19585 13918 416627 29.9 | 35.437 % | c | 111710 | 53417 138729 | 21544 14068 423829 30.1 | 35.437 % | c | 111936 | 53417 138729 | 23698 14294 431416 30.2 | 35.437 % | c | 112275 | 53417 138729 | 26068 14633 450898 30.8 | 35.437 % | c | 112781 | 53417 138729 | 28675 15139 481538 31.8 | 35.437 % | c | 113541 | 53417 138729 | 31542 15899 529961 33.3 | 35.437 % | c | 114680 | 53417 138729 | 34696 17038 592837 34.8 | 35.437 % | c | 116388 | 53291 138436 | 38166 18722 655572 35.0 | 35.617 % | c | 118952 | 53142 138090 | 41983 21251 834890 39.3 | 35.819 % | c | 122797 | 53142 138090 | 46181 25096 1015052 40.4 | 35.819 % | c | 128563 | 53142 138090 | 50799 30862 1260163 40.8 | 35.819 % | c | 137214 | 53132 138063 | 55879 39507 1747123 44.2 | 35.828 % | c ============================================================================== c [1mFound solution: 1674[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 144513 | 53076 137933 | 17692 46804 2162886 46.2 | 35.828 % | c | 144614 | 53076 137933 | 19461 19538 755239 38.7 | 35.913 % | c | 144765 | 53076 137933 | 21407 19689 759014 38.6 | 35.913 % | c | 144990 | 53076 137933 | 23548 19914 771862 38.8 | 35.913 % | c | 145329 | 53076 137933 | 25902 20253 790174 39.0 | 35.913 % | c | 145837 | 53076 137933 | 28493 20761 816689 39.3 | 35.913 % | c | 146597 | 53076 137933 | 31342 21521 854194 39.7 | 35.913 % | c | 147736 | 53076 137933 | 34476 22660 909307 40.1 | 35.913 % | c | 149444 | 53076 137933 | 37924 24368 977408 40.1 | 35.913 % | c ============================================================================== c [1mFound solution: 1673[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 150144 | 53079 137938 | 17693 25067 1018697 40.6 | 35.913 % | c | 150244 | 53079 137938 | 19462 25167 1023272 40.7 | 35.917 % | c | 150394 | 53079 137938 | 21408 25317 1027428 40.6 | 35.917 % | c | 150619 | 52948 137633 | 23549 25530 1035370 40.6 | 36.102 % | c | 150956 | 52811 137306 | 25904 25842 1047899 40.6 | 36.269 % | c | 151464 | 52811 137306 | 28494 26350 1070170 40.6 | 36.269 % | c | 152224 | 52811 137306 | 31344 27110 1094861 40.4 | 36.269 % | c | 153363 | 52811 137306 | 34478 28249 1140635 40.4 | 36.269 % | c | 155071 | 52811 137306 | 37926 29957 1211321 40.4 | 36.269 % | c | 157633 | 52742 137146 | 41719 32516 1353392 41.6 | 36.368 % | c | 161477 | 52691 137025 | 45891 36347 1573604 43.3 | 36.432 % | c ============================================================================== c [1mFound solution: 1671[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 165192 | 52695 137035 | 17565 40062 1768654 44.1 | 36.432 % | c | 165292 | 52695 137035 | 19321 19125 689106 36.0 | 36.433 % | c | 165442 | 52695 137035 | 21253 19275 695771 36.1 | 36.433 % | c | 165670 | 52695 137035 | 23379 19503 711946 36.5 | 36.433 % | c | 166008 | 52695 137035 | 25716 19841 725279 36.6 | 36.433 % | c | 166514 | 52695 137035 | 28288 20347 746787 36.7 | 36.433 % | c ============================================================================== c [1mFound solution: 1668[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 166994 | 52699 137045 | 17566 20827 770393 37.0 | 36.433 % | c | 167095 | 52699 137045 | 19322 20928 777479 37.2 | 36.434 % | c | 167247 | 52699 137045 | 21254 21080 791718 37.6 | 36.434 % | c | 167474 | 52699 137045 | 23380 21307 799949 37.5 | 36.434 % | c | 167811 | 52699 137045 | 25718 21644 815385 37.7 | 36.434 % | c | 168317 | 52699 137045 | 28290 22150 847982 38.3 | 36.434 % | c | 169078 | 52699 137045 | 31119 22911 877800 38.3 | 36.434 % | c | 170218 | 52699 137045 | 34231 24051 927360 38.6 | 36.434 % | c | 171926 | 52699 137045 | 37654 25759 1026430 39.8 | 36.434 % | c | 174491 | 52699 137045 | 41419 28324 1168146 41.2 | 36.434 % | c ============================================================================== c [1mFound solution: 1659[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 175110 | 52703 137055 | 17567 28943 1215179 42.0 | 36.434 % | c | 175212 | 52652 136935 | 19323 14572 480982 33.0 | 36.517 % | c | 175362 | 52652 136935 | 21256 14722 490944 33.3 | 36.517 % | c | 175588 | 52649 136929 | 23381 14946 505311 33.8 | 36.521 % | c | 175928 | 52649 136929 | 25719 15286 524060 34.3 | 36.521 % | c | 176435 | 52649 136929 | 28291 15793 549075 34.8 | 36.521 % | c | 177194 | 52649 136929 | 31121 16552 587540 35.5 | 36.521 % | c | 178334 | 52649 136929 | 34233 17692 646778 36.6 | 36.521 % | c ============================================================================== c [1mFound solution: 1651[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 179859 | 52653 136939 | 17551 19217 741511 38.6 | 36.521 % | c | 179959 | 52653 136939 | 19306 19317 746063 38.6 | 36.522 % | c | 180109 | 52653 136939 | 21236 19467 753313 38.7 | 36.522 % | c | 180334 | 52653 136939 | 23360 19692 762998 38.7 | 36.522 % | c | 180672 | 52653 136939 | 25696 20030 780628 39.0 | 36.522 % | c | 181179 | 52653 136939 | 28266 20537 810883 39.5 | 36.522 % | c | 181938 | 52653 136939 | 31092 21296 849267 39.9 | 36.522 % | c | 183077 | 52653 136939 | 34201 22435 899688 40.1 | 36.522 % | c | 184786 | 52643 136916 | 37622 24139 992629 41.1 | 36.535 % | c | 187348 | 52639 136906 | 41384 26700 1120688 42.0 | 36.539 % | c ============================================================================== c [1mFound solution: 1648[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 188862 | 52646 136923 | 17548 28214 1228249 43.5 | 36.539 % | c | 188962 | 52646 136923 | 19302 14207 469546 33.1 | 36.539 % | c | 189112 | 52646 136923 | 21233 14357 474223 33.0 | 36.539 % | c | 189339 | 52646 136923 | 23356 14584 483674 33.2 | 36.539 % | c | 189676 | 52646 136923 | 25692 14921 500108 33.5 | 36.539 % | c | 190182 | 52646 136923 | 28261 15427 522460 33.9 | 36.539 % | c | 190943 | 52646 136923 | 31087 16188 557553 34.4 | 36.539 % | c | 192082 | 52646 136923 | 34196 17327 599942 34.6 | 36.539 % | c | 193792 | 52646 136923 | 37615 19037 717191 37.7 | 36.539 % | c | 196354 | 52632 136885 | 41377 21594 806921 37.4 | 36.552 % | c | 200198 | 52080 135597 | 45514 25416 1020646 40.2 | 37.324 % | c | 205964 | 52080 135597 | 50066 31182 1315835 42.2 | 37.324 % | c | 214613 | 52067 135564 | 55073 39828 1789558 44.9 | 37.337 % | c | 227587 | 52067 135564 | 60580 52802 2635487 49.9 | 37.337 % | c ============================================================================== c [1mFound solution: 1639[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 239337 | 52047 135506 | 17349 64547 3435785 53.2 | 37.337 % | c | 239438 | 52047 135506 | 19083 21363 926240 43.4 | 37.359 % | c | 239590 | 52047 135506 | 20992 21515 932551 43.3 | 37.359 % | c | 239815 | 52047 135506 | 23091 21740 941576 43.3 | 37.359 % | c | 240154 | 52047 135506 | 25400 22079 952174 43.1 | 37.359 % | c | 240661 | 52047 135506 | 27940 22586 977468 43.3 | 37.359 % | c | 241421 | 52047 135506 | 30734 23346 1027014 44.0 | 37.359 % | c | 242565 | 52047 135506 | 33808 24490 1076721 44.0 | 37.359 % | c | 244273 | 52047 135506 | 37189 26198 1169764 44.7 | 37.359 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.93 0.98 0.93 2/54 5339 Raw data (stat): 5339 (runsolver) R 5338 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546954394 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.94 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2436 0 0 0 993 5 0 0 25 0 1 0 546954394 12017664 2362 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2934 2362 603 41 0 2893 0 vsize: 11736 [startup+20.0012 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2539 0 0 0 1992 6 0 0 25 0 1 0 546954394 12447744 2465 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3039 2465 603 41 0 2998 0 vsize: 12156 [startup+30.0015 s] Raw data (loadavg): 0.95 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2620 0 0 0 2992 7 0 0 25 0 1 0 546954394 12877824 2546 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3144 2546 603 41 0 3103 0 vsize: 12576 [startup+40.0022 s] Raw data (loadavg): 0.96 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2733 0 0 0 3991 7 0 0 25 0 1 0 546954394 13312000 2659 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3250 2659 603 41 0 3209 0 vsize: 13000 [startup+50.0033 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2831 0 0 0 4991 8 0 0 25 0 1 0 546954394 13647872 2757 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3332 2757 603 41 0 3291 0 vsize: 13328 [startup+60.0026 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 2920 0 0 0 5990 9 0 0 25 0 1 0 546954394 14049280 2846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3430 2846 603 41 0 3389 0 vsize: 13720 [startup+70.0034 s] Raw data (loadavg): 0.97 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3060 0 0 0 6990 9 0 0 25 0 1 0 546954394 14729216 2986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3596 2986 603 41 0 3555 0 vsize: 14384 [startup+80.0045 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3217 0 0 0 7989 10 0 0 25 0 1 0 546954394 15261696 3143 4294967295 134512640 134672761 3221224544 3221223636 1075346528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3726 3143 603 41 0 3685 0 vsize: 14904 [startup+90.0048 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3390 0 0 0 8987 11 0 0 25 0 1 0 546954394 16027648 3316 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3913 3316 603 41 0 3872 0 vsize: 15652 [startup+100.004 s] Raw data (loadavg): 0.98 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3548 0 0 0 9987 12 0 0 25 0 1 0 546954394 16687104 3474 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4074 3474 603 41 0 4033 0 vsize: 16296 [startup+110.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3704 0 0 0 10986 13 0 0 25 0 1 0 546954394 17219584 3630 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4204 3630 603 41 0 4163 0 vsize: 16816 [startup+120.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3840 0 0 0 11985 14 0 0 25 0 1 0 546954394 17879040 3766 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4365 3766 603 41 0 4324 0 vsize: 17460 [startup+130.004 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 3956 0 0 0 12985 14 0 0 25 0 1 0 546954394 18272256 3882 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4461 3882 603 41 0 4420 0 vsize: 17844 [startup+140.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4119 0 0 0 13984 15 0 0 25 0 1 0 546954394 18939904 4045 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4624 4045 603 41 0 4583 0 vsize: 18496 [startup+150.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 14984 15 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+160.005 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 15984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+170.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 16984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+180.006 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 17984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+190.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 18984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+200.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4158 0 0 0 19984 16 0 0 25 0 1 0 546954394 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+210.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4266 0 0 0 20984 16 0 0 25 0 1 0 546954394 19595264 4192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4784 4192 603 41 0 4743 0 vsize: 19136 [startup+220.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 21984 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+230.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 22984 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+240.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 23985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+250.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 24985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+260.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 25985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+270.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 26985 16 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+280.007 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 27985 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+290.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 28985 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+300.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 29985 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+310.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 30986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+320.008 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 31986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+330.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 32986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+340.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 33986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+350.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4321 0 0 0 34986 17 0 0 25 0 1 0 546954394 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+360.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 35986 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+370.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 36986 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+380.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 37986 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+390.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 38987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+400.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 39987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+410.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 40987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+420.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 41987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+430.011 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4396 0 0 0 42987 17 0 0 25 0 1 0 546954394 20062208 4322 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+440.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4429 0 0 0 43987 17 0 0 25 0 1 0 546954394 20324352 4355 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4962 4355 603 41 0 4921 0 vsize: 19848 [startup+450.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4521 0 0 0 44987 18 0 0 25 0 1 0 546954394 20717568 4447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5058 4447 603 41 0 5017 0 vsize: 20232 [startup+460.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4650 0 0 0 45987 18 0 0 25 0 1 0 546954394 21250048 4576 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5188 4576 603 41 0 5147 0 vsize: 20752 [startup+470.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 46987 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+480.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 47987 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+490.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 48987 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+500.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 49988 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+510.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 50988 18 0 0 25 0 1 0 546954394 21635072 4679 4294967295 134512640 134672761 3221224544 3221223844 134556682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+520.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 51988 18 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+530.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 52988 18 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+540.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 53988 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+550.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 54988 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+560.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 55988 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+570.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 56989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+580.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 57989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+590.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 58989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+600.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 59989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+610.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 60989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+620.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4753 0 0 0 61989 19 0 0 25 0 1 0 546954394 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+630.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4754 0 0 0 62989 19 0 0 25 0 1 0 546954394 21630976 4680 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4680 603 41 0 5240 0 vsize: 21124 [startup+640.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4756 0 0 0 63989 19 0 0 25 0 1 0 546954394 21630976 4682 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5281 4682 603 41 0 5240 0 vsize: 21124 [startup+650.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4819 0 0 0 64989 19 0 0 25 0 1 0 546954394 21901312 4745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5347 4745 603 41 0 5306 0 vsize: 21388 [startup+660.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 4930 0 0 0 65989 19 0 0 25 0 1 0 546954394 22429696 4856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5476 4856 603 41 0 5435 0 vsize: 21904 [startup+670.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5049 0 0 0 66989 20 0 0 25 0 1 0 546954394 22822912 4975 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5572 4975 603 41 0 5531 0 vsize: 22288 [startup+680.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5166 0 0 0 67989 20 0 0 25 0 1 0 546954394 23351296 5092 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5701 5092 603 41 0 5660 0 vsize: 22804 [startup+690.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 68989 20 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+700.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 69989 20 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+710.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 70989 20 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+720.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 71989 20 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+730.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 72989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+740.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 73989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+750.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 74989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+760.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 75989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+770.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 76989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+780.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5196 0 0 0 77989 21 0 0 25 0 1 0 546954394 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+790.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 78989 21 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+800.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 79989 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+810.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 80990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+820.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 81990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+830.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 82990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+840.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 83990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+850.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 84990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+860.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 85990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+870.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 86990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+880.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 87990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+890.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 88991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+900.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 89990 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+910.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 90991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+920.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 91991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+930.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 92991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+940.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 93991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+950.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 94991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+960.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 95991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+970.014 s] Raw data (loadavg): 1.07 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 96991 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+980.015 s] Raw data (loadavg): 1.06 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 97992 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+990.014 s] Raw data (loadavg): 1.05 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 98992 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1000.01 s] Raw data (loadavg): 1.04 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 99992 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1010.01 s] Raw data (loadavg): 1.03 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 100992 22 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1020.01 s] Raw data (loadavg): 1.03 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 101992 23 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1030.01 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 102992 23 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1040.01 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5212 0 0 0 103992 23 0 0 25 0 1 0 546954394 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1050.01 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5265 0 0 0 104992 23 0 0 25 0 1 0 546954394 23785472 5191 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5807 5191 603 41 0 5766 0 vsize: 23228 [startup+1060.01 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5391 0 0 0 105992 23 0 0 25 0 1 0 546954394 24313856 5317 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5936 5317 603 41 0 5895 0 vsize: 23744 [startup+1070.02 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5507 0 0 0 106992 24 0 0 25 0 1 0 546954394 24752128 5433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6043 5433 603 41 0 6002 0 vsize: 24172 [startup+1080.02 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5621 0 0 0 107992 24 0 0 25 0 1 0 546954394 25276416 5547 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6171 5547 603 41 0 6130 0 vsize: 24684 [startup+1090.02 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5734 0 0 0 108991 25 0 0 25 0 1 0 546954394 25669632 5660 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6267 5660 603 41 0 6226 0 vsize: 25068 [startup+1100.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5880 0 0 0 109991 25 0 0 25 0 1 0 546954394 26365952 5806 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6437 5806 603 41 0 6396 0 vsize: 25748 [startup+1110.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 5996 0 0 0 110991 25 0 0 25 0 1 0 546954394 26763264 5922 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6534 5922 603 41 0 6493 0 vsize: 26136 [startup+1120.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6108 0 0 0 111991 26 0 0 25 0 1 0 546954394 27299840 6034 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6665 6034 603 41 0 6624 0 vsize: 26660 [startup+1130.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6236 0 0 0 112991 26 0 0 25 0 1 0 546954394 27832320 6162 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6795 6162 603 41 0 6754 0 vsize: 27180 [startup+1140.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 5339 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6360 0 0 0 113990 27 0 0 25 0 1 0 546954394 28233728 6286 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6893 6286 603 41 0 6852 0 vsize: 27572 [startup+1150.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 5340 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6499 0 0 0 114990 27 0 0 25 0 1 0 546954394 28774400 6425 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7025 6425 603 41 0 6984 0 vsize: 28100 [startup+1160.02 s] Raw data (loadavg): 1.07 1.02 0.94 2/54 5392 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6613 0 0 0 115982 35 0 0 25 0 1 0 546954394 29306880 6539 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7155 6539 603 41 0 7114 0 vsize: 28620 [startup+1170.02 s] Raw data (loadavg): 1.06 1.02 0.94 2/54 5392 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 116982 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7246 6644 603 41 0 7205 0 vsize: 28984 [startup+1180.02 s] Raw data (loadavg): 1.05 1.01 0.94 2/54 5392 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 117982 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7246 6644 603 41 0 7205 0 vsize: 28984 [startup+1190.02 s] Raw data (loadavg): 1.04 1.01 0.94 2/54 5392 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 118982 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7246 6644 603 41 0 7205 0 vsize: 28984 [startup+1200.02 s] Raw data (loadavg): 1.04 1.01 0.94 2/54 5392 Raw data (stat): 5339 (minisat+) R 5338 26298 26297 0 -1 0 6718 0 0 0 119983 35 0 0 25 0 1 0 546954394 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7246 6644 603 41 0 7205 0 vsize: 28984 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.03 s] Raw data (loadavg): 1.04 1.01 0.94 1/54 5392 Raw data (stat): 5339 (minisat+) Z 5338 26298 26297 0 -1 12 6721 0 0 0 119983 37 0 0 25 0 1 0 546954394 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.03 CPU time (s): 1200.2 CPU user time (s): 1199.83 CPU system time (s): 0.372943 CPU usage (%): 100.014 Max. virtual memory (Kb): 28984 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####