Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.02284 |
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 wulflinc15 THE 2005-04-22 02:03:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12129 boxname=wulflinc15 idbench=933 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ffa3a55eb53181880328dd1b84f91e66 /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-p0201.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-p0201.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-p0201.opb IDLAUNCH: 12129 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 638624 kB Buffers: 27584 kB Cached: 347004 kB SwapCached: 432 kB Active: 40884 kB Inactive: 335912 kB HighTotal: 131008 kB HighFree: 60564 kB LowTotal: 903652 kB LowFree: 578060 kB SwapTotal: 2097136 kB SwapFree: 2095984 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5364 kB Slab: 13528 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 02:23:34 (client local time) WITH STATUS 10 IN 1200.22 SECONDS stats: 12129 7 1200.22 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 % | #### 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.78 0.95 0.94 2/54 22181 Raw data (stat): 22181 (runsolver) R 22180 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491747314 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10 s] Raw data (loadavg): 0.81 0.95 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2436 0 0 0 991 7 0 0 25 0 1 0 491747314 12017664 2362 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2934 2362 603 41 0 2893 0 vsize: 11736 [startup+19.9997 s] Raw data (loadavg): 0.84 0.95 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2539 0 0 0 1991 7 0 0 25 0 1 0 491747314 12447744 2465 4294967295 134512640 134672761 3221224544 3221223712 134561215 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.0008 s] Raw data (loadavg): 0.86 0.95 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2622 0 0 0 2990 7 0 0 25 0 1 0 491747314 12877824 2548 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3144 2548 603 41 0 3103 0 vsize: 12576 [startup+40.0004 s] Raw data (loadavg): 0.89 0.95 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2734 0 0 0 3990 7 0 0 25 0 1 0 491747314 13312000 2660 4294967295 134512640 134672761 3221224544 3221223728 134559313 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3250 2660 603 41 0 3209 0 vsize: 13000 [startup+50.0012 s] Raw data (loadavg): 0.90 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2831 0 0 0 4990 8 0 0 25 0 1 0 491747314 13647872 2757 4294967295 134512640 134672761 3221224544 3221223696 134561035 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.0016 s] Raw data (loadavg): 0.92 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 2923 0 0 0 5990 8 0 0 25 0 1 0 491747314 14049280 2849 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3430 2849 603 41 0 3389 0 vsize: 13720 [startup+70.0018 s] Raw data (loadavg): 0.93 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3063 0 0 0 6989 8 0 0 25 0 1 0 491747314 14729216 2989 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3596 2989 603 41 0 3555 0 vsize: 14384 [startup+80.0027 s] Raw data (loadavg): 0.94 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3236 0 0 0 7988 10 0 0 25 0 1 0 491747314 15392768 3162 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3758 3162 603 41 0 3717 0 vsize: 15032 [startup+90.0028 s] Raw data (loadavg): 0.95 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3407 0 0 0 8988 10 0 0 25 0 1 0 491747314 16027648 3333 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3913 3333 603 41 0 3872 0 vsize: 15652 [startup+100.003 s] Raw data (loadavg): 0.96 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3558 0 0 0 9988 10 0 0 25 0 1 0 491747314 16687104 3484 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4074 3484 603 41 0 4033 0 vsize: 16296 [startup+110.004 s] Raw data (loadavg): 0.96 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3717 0 0 0 10987 11 0 0 25 0 1 0 491747314 17350656 3643 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4236 3643 603 41 0 4195 0 vsize: 16944 [startup+120.004 s] Raw data (loadavg): 0.97 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3845 0 0 0 11987 11 0 0 25 0 1 0 491747314 17879040 3771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4365 3771 603 41 0 4324 0 vsize: 17460 [startup+130.005 s] Raw data (loadavg): 0.97 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 3968 0 0 0 12987 12 0 0 25 0 1 0 491747314 18407424 3894 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4494 3894 603 41 0 4453 0 vsize: 17976 [startup+140.005 s] Raw data (loadavg): 0.98 0.96 0.94 2/54 22181 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4124 0 0 0 13986 12 0 0 25 0 1 0 491747314 18939904 4050 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4624 4050 603 41 0 4583 0 vsize: 18496 [startup+150.006 s] Raw data (loadavg): 0.98 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 14986 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+160.006 s] Raw data (loadavg): 0.98 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 15986 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+170.006 s] Raw data (loadavg): 0.98 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 16987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 17987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+190.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 18987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+200.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4158 0 0 0 19987 13 0 0 25 0 1 0 491747314 19070976 4084 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4656 4084 603 41 0 4615 0 vsize: 18624 [startup+210.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4266 0 0 0 20987 14 0 0 25 0 1 0 491747314 19595264 4192 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4784 4192 603 41 0 4743 0 vsize: 19136 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 21986 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 22987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 23987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+250.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 24987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223648 134559922 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 25987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 26987 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+280.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 27988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+290.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 28988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+300.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 29988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+310.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 30988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+320.009 s] Raw data (loadavg): 1.07 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 31988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+330.011 s] Raw data (loadavg): 1.06 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 32988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+340.01 s] Raw data (loadavg): 1.05 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 33988 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+350.011 s] Raw data (loadavg): 1.04 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4321 0 0 0 34989 14 0 0 25 0 1 0 491747314 19755008 4247 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4247 603 41 0 4782 0 vsize: 19292 [startup+360.012 s] Raw data (loadavg): 1.03 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 35989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+370.012 s] Raw data (loadavg): 1.03 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 36989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+380.011 s] Raw data (loadavg): 1.02 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 37989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+390.012 s] Raw data (loadavg): 1.02 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 38989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+400.012 s] Raw data (loadavg): 1.02 0.99 0.94 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 39989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+410.012 s] Raw data (loadavg): 1.17 1.02 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 40989 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+420.012 s] Raw data (loadavg): 1.14 1.02 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 41990 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+430.013 s] Raw data (loadavg): 1.12 1.02 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 42990 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+440.012 s] Raw data (loadavg): 1.10 1.02 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4396 0 0 0 43990 14 0 0 25 0 1 0 491747314 20062208 4322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4898 4322 603 41 0 4857 0 vsize: 19592 [startup+450.014 s] Raw data (loadavg): 1.08 1.02 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4491 0 0 0 44990 15 0 0 25 0 1 0 491747314 20586496 4417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5026 4417 603 41 0 4985 0 vsize: 20104 [startup+460.013 s] Raw data (loadavg): 1.07 1.02 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4625 0 0 0 45990 15 0 0 25 0 1 0 491747314 21118976 4551 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5156 4551 603 41 0 5115 0 vsize: 20624 [startup+470.014 s] Raw data (loadavg): 1.06 1.01 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 46990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+480.014 s] Raw data (loadavg): 1.05 1.01 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 47990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+490.014 s] Raw data (loadavg): 1.04 1.01 0.95 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 48990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+500.014 s] Raw data (loadavg): 1.12 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 49990 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+510.014 s] Raw data (loadavg): 1.17 1.04 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 50991 15 0 0 25 0 1 0 491747314 21635072 4679 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5282 4679 603 41 0 5241 0 vsize: 21128 [startup+520.015 s] Raw data (loadavg): 1.14 1.04 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 51991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+530.015 s] Raw data (loadavg): 1.12 1.04 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 52991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+540.015 s] Raw data (loadavg): 1.10 1.04 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 53991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+550.016 s] Raw data (loadavg): 1.09 1.04 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 54991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+560.015 s] Raw data (loadavg): 1.07 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 55991 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+570.015 s] Raw data (loadavg): 1.06 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 56992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+580.017 s] Raw data (loadavg): 1.05 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 57992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+590.017 s] Raw data (loadavg): 1.04 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 58992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+600.018 s] Raw data (loadavg): 1.04 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 59992 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+610.019 s] Raw data (loadavg): 1.03 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 60993 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+620.018 s] Raw data (loadavg): 1.02 1.03 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 61993 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+630.018 s] Raw data (loadavg): 1.02 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4753 0 0 0 62993 15 0 0 25 0 1 0 491747314 21630976 4679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4679 603 41 0 5240 0 vsize: 21124 [startup+640.02 s] Raw data (loadavg): 1.02 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4755 0 0 0 63993 15 0 0 25 0 1 0 491747314 21630976 4681 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5281 4681 603 41 0 5240 0 vsize: 21124 [startup+650.02 s] Raw data (loadavg): 1.01 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4791 0 0 0 64993 15 0 0 25 0 1 0 491747314 21766144 4717 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5314 4717 603 41 0 5273 0 vsize: 21256 [startup+660.02 s] Raw data (loadavg): 1.01 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4874 0 0 0 65993 15 0 0 25 0 1 0 491747314 22167552 4800 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5412 4800 603 41 0 5371 0 vsize: 21648 [startup+670.02 s] Raw data (loadavg): 1.01 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 4993 0 0 0 66993 16 0 0 25 0 1 0 491747314 22691840 4919 4294967295 134512640 134672761 3221224544 3221223728 134559351 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5540 4919 603 41 0 5499 0 vsize: 22160 [startup+680.02 s] Raw data (loadavg): 1.01 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5114 0 0 0 67993 16 0 0 25 0 1 0 491747314 23085056 5040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5636 5040 603 41 0 5595 0 vsize: 22544 [startup+690.02 s] Raw data (loadavg): 1.01 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 68993 16 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+700.021 s] Raw data (loadavg): 1.00 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 69993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+710.022 s] Raw data (loadavg): 1.00 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 70993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+720.022 s] Raw data (loadavg): 1.00 1.02 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 71993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+730.023 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 72993 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+740.023 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 73994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+750.024 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 74994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+760.025 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 75994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+770.026 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 76994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+780.026 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5196 0 0 0 77994 17 0 0 25 0 1 0 491747314 23425024 5122 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5719 5122 603 41 0 5678 0 vsize: 22876 [startup+790.026 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 78994 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+800.026 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 79995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+810.026 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 80995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+820.026 s] Raw data (loadavg): 1.00 1.01 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 81995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+830.027 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 82995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+840.027 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 83995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+850.028 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 84995 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+860.028 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 85996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+870.028 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 86996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+880.029 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 87996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223628 1075346528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+890.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 88996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+900.031 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 89996 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+910.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 90997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+920.031 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 91997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+930.031 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 92997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+940.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 93997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+950.033 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 94997 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+960.033 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 95998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+970.034 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 96998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+980.034 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 97998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+990.034 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 98998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1000.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 99998 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1010.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 100999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1020.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 101999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1030.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 102999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1040.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 103999 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1050.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5212 0 0 0 105000 17 0 0 25 0 1 0 491747314 23523328 5138 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5743 5138 603 41 0 5702 0 vsize: 22972 [startup+1060.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5279 0 0 0 105999 17 0 0 25 0 1 0 491747314 23785472 5205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5807 5205 603 41 0 5766 0 vsize: 23228 [startup+1070.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5403 0 0 0 106999 18 0 0 25 0 1 0 491747314 24313856 5329 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5936 5329 603 41 0 5895 0 vsize: 23744 [startup+1080.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5514 0 0 0 107999 18 0 0 25 0 1 0 491747314 24752128 5440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6043 5440 603 41 0 6002 0 vsize: 24172 [startup+1090.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5625 0 0 0 108998 19 0 0 25 0 1 0 491747314 25276416 5551 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6171 5551 603 41 0 6130 0 vsize: 24684 [startup+1100.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5739 0 0 0 109998 19 0 0 25 0 1 0 491747314 25669632 5665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6267 5665 603 41 0 6226 0 vsize: 25068 [startup+1110.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5881 0 0 0 110999 19 0 0 25 0 1 0 491747314 26365952 5807 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6437 5807 603 41 0 6396 0 vsize: 25748 [startup+1120.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 5996 0 0 0 111998 20 0 0 25 0 1 0 491747314 26763264 5922 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6534 5922 603 41 0 6493 0 vsize: 26136 [startup+1130.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6108 0 0 0 112999 20 0 0 25 0 1 0 491747314 27299840 6034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6665 6034 603 41 0 6624 0 vsize: 26660 [startup+1140.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6233 0 0 0 113998 20 0 0 25 0 1 0 491747314 27697152 6159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6762 6159 603 41 0 6721 0 vsize: 27048 [startup+1150.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6355 0 0 0 114998 21 0 0 25 0 1 0 491747314 28233728 6281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6893 6281 603 41 0 6852 0 vsize: 27572 [startup+1160.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6494 0 0 0 115998 21 0 0 25 0 1 0 491747314 28774400 6420 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7025 6420 603 41 0 6984 0 vsize: 28100 [startup+1170.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6611 0 0 0 116998 21 0 0 25 0 1 0 491747314 29306880 6537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7155 6537 603 41 0 7114 0 vsize: 28620 [startup+1180.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6718 0 0 0 117997 22 0 0 25 0 1 0 491747314 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7246 6644 603 41 0 7205 0 vsize: 28984 [startup+1190.05 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6718 0 0 0 118998 22 0 0 25 0 1 0 491747314 29679616 6644 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7246 6644 603 41 0 7205 0 vsize: 28984 [startup+1200.05 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 22183 Raw data (stat): 22181 (minisat+) R 22180 29151 29150 0 -1 0 6718 0 0 0 119998 22 0 0 25 0 1 0 491747314 29679616 6644 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7246 6644 603 41 0 7205 0 vsize: 28984 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.06 s] Raw data (loadavg): 1.00 1.00 0.96 1/54 22183 Raw data (stat): 22181 (minisat+) Z 22180 29151 29150 0 -1 12 6721 0 0 0 119998 23 0 0 25 0 1 0 491747314 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.06 CPU time (s): 1200.22 CPU user time (s): 1199.99 CPU system time (s): 0.236963 CPU usage (%): 100.013 Max. virtual memory (Kb): 28984 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####