Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-flugpl.opb |
MD5SUM | 1b5898327a7b85a882e36ea549878fdf |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1843200 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 195 |
Biggest coefficient in the objective function | 47185920 |
Number of bits for the biggest coefficient in the objective function | 26 |
Sum of the numbers in the objective function | 103639200 |
Number of bits of the sum of numbers in the objective function | 27 |
Biggest number in a constraint | 78643200 |
Number of bits of the biggest number in a constraint | 27 |
Biggest sum of numbers in a constraint | 159755625 |
Number of bits of the biggest sum of numbers | 28 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.181972 |
Number of variables | 195 |
Total number of constraints | 29 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 29 |
Minimum length of a constraint | 5 |
Maximum length of a constraint | 45 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-04-21 03:11:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18369 boxname=wulflinc21 idbench=1413 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1b5898327a7b85a882e36ea549878fdf /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-flugpl.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-flugpl.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-flugpl.opb IDLAUNCH: 18369 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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.161 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: 787120 kB Buffers: 6736 kB Cached: 217188 kB SwapCached: 0 kB Active: 63316 kB Inactive: 163488 kB HighTotal: 131008 kB HighFree: 65660 kB LowTotal: 903652 kB LowFree: 721460 kB SwapTotal: 2097892 kB SwapFree: 2097804 kB Dirty: 8 kB Writeback: 0 kB Mapped: 6948 kB Slab: 15012 kB Committed_AS: 63796 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 03:12:15 (client local time) WITH STATUS 30 IN 23.3454 SECONDS stats: 18369 0 23.3454 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 35 PB-constraints to clauses... c -- Unit propagations: pp c -- Detecting intervals from adjacent constraints: ##### c -- Clauses(.)/Splits(s): (none) c ---[ 34]---> BDD-cost: 4 c ---[ 33]---> BDD-cost: 4 c ---[ 32]---> BDD-cost: 4 c ---[ 31]---> BDD-cost: 4 c ---[ 30]---> BDD-cost: 4 c ---[ 29]---> BDD-cost: 4 c ---[ 28]---> BDD-cost: 4 c ---[ 27]---> BDD-cost: 4 c ---[ 26]---> BDD-cost: 4 c ---[ 25]---> BDD-cost: 4 c ---[ 24]---> BDD-cost: 4 c ---[ 20]---> BDD-cost: 20 c ---[ 18]---> BDD-cost: 63 c ---[ 16]---> BDD-cost: 63 c ---[ 14]---> BDD-cost: 63 c ---[ 12]---> BDD-cost: 63 c ---[ 11]---> BDD-cost: 107 c ---[ 10]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 9]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 8]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 7]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 6]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 5]---> BDD-cost: 17 c ---[ 4]---> BDD-cost: 86 c ---[ 3]---> BDD-cost: 86 c ---[ 2]---> BDD-cost: 86 c ---[ 1]---> BDD-cost: 86 c ---[ 0]---> BDD-cost: 86 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 10491 25716 | 3497 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 2143616[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9040 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20 | 35519 84451 | 11839 20 176 8.8 | 0.000 % | c ============================================================================== c [1mFound solution: 2093317[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6159 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 93 | 51600 122279 | 17200 92 658 7.2 | 0.000 % | c ============================================================================== c [1mFound solution: 2091322[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 125 | 51796 122849 | 17265 123 975 7.9 | 0.000 % | c | 226 | 49470 117464 | 18991 208 1498 7.2 | 4.433 % | c ============================================================================== c [1mFound solution: 2060538[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6039 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 326 | 65361 154809 | 21787 301 2537 8.4 | 4.433 % | c | 426 | 57963 137640 | 23965 377 9327 24.7 | 13.020 % | c ============================================================================== c [1mFound solution: 2030842[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4707 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 474 | 66838 158637 | 22279 412 9765 23.7 | 13.020 % | c ============================================================================== c [1mFound solution: 1957678[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3590 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 545 | 74842 177522 | 24947 479 11139 23.3 | 13.020 % | c ============================================================================== c [1mFound solution: 1951918[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 609 | 74638 177088 | 24879 540 12576 23.3 | 13.020 % | c | 709 | 73853 175285 | 27366 638 13804 21.6 | 16.406 % | c ============================================================================== c [1mFound solution: 1949614[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3095 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 746 | 82079 194624 | 27359 673 14233 21.1 | 16.406 % | c ============================================================================== c [1mFound solution: 1946810[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 788 | 82181 194909 | 27393 714 14699 20.6 | 16.406 % | c ============================================================================== c [1mFound solution: 1920954[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 833 | 89061 211226 | 29687 753 16207 21.5 | 16.406 % | c ============================================================================== c [1mFound solution: 1913785[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3121 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 919 | 94618 224444 | 31539 821 16981 20.7 | 16.406 % | c ============================================================================== c [1mFound solution: 1904630[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 956 | 94698 224666 | 31566 858 17841 20.8 | 16.406 % | c ============================================================================== c [1mFound solution: 1904629[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1018 | 94470 224158 | 31490 919 19501 21.2 | 16.406 % | c ============================================================================== c [1mFound solution: 1904598[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1043 | 94497 224227 | 31499 944 19863 21.0 | 16.406 % | c ============================================================================== c [1mFound solution: 1894389[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1108 | 94410 224039 | 31470 1008 21833 21.7 | 16.406 % | c ============================================================================== c [1mFound solution: 1892342[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1131 | 94428 224085 | 31476 1031 22892 22.2 | 16.406 % | c | 1231 | 94428 224085 | 34623 1131 25469 22.5 | 17.410 % | c ============================================================================== c [1mFound solution: 1892334[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1269 | 94444 224129 | 31481 1169 26268 22.5 | 17.410 % | c ============================================================================== c [1mFound solution: 1884041[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1312 | 94472 224201 | 31490 1212 27107 22.4 | 17.410 % | c ============================================================================== c [1mFound solution: 1883930[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1333 | 94500 224273 | 31500 1233 27674 22.4 | 17.410 % | c ============================================================================== c [1mFound solution: 1883545[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2157 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1346 | 70217 168166 | 23405 1108 21333 19.3 | 17.410 % | c ============================================================================== c [1mFound solution: 1883537[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1351 | 70298 168381 | 23432 1113 21343 19.2 | 17.410 % | c ============================================================================== c [1mFound solution: 1883530[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1352 | 70330 168461 | 23443 1114 21345 19.2 | 17.410 % | c ============================================================================== c [1mFound solution: 1883529[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1353 | 70355 168522 | 23451 1115 21347 19.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1883528[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1353 | 70386 168599 | 23462 1115 21347 19.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1883527[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1356 | 70417 168676 | 23472 1118 21357 19.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1882506[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1359 | 70431 168712 | 23477 1121 21407 19.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1881994[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1376 | 70448 168755 | 23482 1138 21732 19.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1881930[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1409 | 70436 168733 | 23478 1169 22443 19.2 | 17.410 % | c ============================================================================== c [1mFound solution: 1880970[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1438 | 70457 168784 | 23485 1198 23312 19.5 | 17.410 % | c ============================================================================== c [1mFound solution: 1867802[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1470 | 70477 168841 | 23492 1229 24055 19.6 | 17.410 % | c ============================================================================== c [1mFound solution: 1867678[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1516 | 70469 168833 | 23489 1273 24359 19.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1867666[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1535 | 70501 168913 | 23500 1292 24545 19.0 | 17.410 % | c ============================================================================== c [1mFound solution: 1866742[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1561 | 70524 168972 | 23508 1318 24878 18.9 | 17.410 % | c ============================================================================== c [1mFound solution: 1863670[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1574 | 70540 169012 | 23513 1331 24964 18.8 | 17.410 % | c ============================================================================== c [1mFound solution: 1863662[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1575 | 70562 169068 | 23520 1332 24967 18.7 | 17.410 % | c ============================================================================== c [1mFound solution: 1863661[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1578 | 70587 169133 | 23529 1335 24977 18.7 | 17.410 % | c ============================================================================== c [1mFound solution: 1863645[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1589 | 70611 169195 | 23537 1346 25281 18.8 | 17.410 % | c ============================================================================== c [1mFound solution: 1862637[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1609 | 70633 169253 | 23544 1366 25557 18.7 | 17.410 % | c ============================================================================== c [1mFound solution: 1859629[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1626 | 70619 169230 | 23539 1381 25760 18.7 | 17.410 % | c ============================================================================== c [1mFound solution: 1859628[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1672 | 70649 169306 | 23549 1427 26335 18.5 | 17.410 % | c ============================================================================== c [1mFound solution: 1859625[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1684 | 70677 169376 | 23559 1439 26469 18.4 | 17.410 % | c ============================================================================== c [1mFound solution: 1859033[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1701 | 70708 169451 | 23569 1456 26896 18.5 | 17.410 % | c ============================================================================== c [1mFound solution: 1859029[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1722 | 70742 169533 | 23580 1477 27177 18.4 | 17.410 % | c ============================================================================== c [1mFound solution: 1851417[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1763 | 70763 169586 | 23587 1518 27871 18.4 | 17.410 % | c ============================================================================== c [1mFound solution: 1851409[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1770 | 70784 169639 | 23594 1525 27934 18.3 | 17.410 % | c ============================================================================== c [1mFound solution: 1851408[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1788 | 70813 169712 | 23604 1543 28198 18.3 | 17.410 % | c ============================================================================== c [1mFound solution: 1848556[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1804 | 70841 169780 | 23613 1559 28544 18.3 | 17.410 % | c ============================================================================== c [1mFound solution: 1848528[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1850 | 70872 169855 | 23624 1605 29129 18.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1848464[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1863 | 70902 169927 | 23634 1618 29370 18.2 | 17.410 % | c ============================================================================== c [1mFound solution: 1848400[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1868 | 70930 169995 | 23643 1623 29453 18.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1848336[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1888 | 70955 170056 | 23651 1643 29719 18.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1848332[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1898 | 70985 170130 | 23661 1653 29965 18.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1848324[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1913 | 71019 170214 | 23673 1668 30130 18.1 | 17.410 % | c ============================================================================== c [1mFound solution: 1847308[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1936 | 71041 170266 | 23680 1691 30491 18.0 | 17.410 % | c | 2036 | 71041 170266 | 26048 1791 33023 18.4 | 39.044 % | c ============================================================================== c [1mFound solution: 1847296[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2080 | 71066 170327 | 23688 1835 33595 18.3 | 39.044 % | c ============================================================================== c [1mFound solution: 1847292[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2091 | 71094 170397 | 23698 1846 33998 18.4 | 39.044 % | c ============================================================================== c [1mFound solution: 1846908[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2136 | 71126 170475 | 23708 1891 34858 18.4 | 39.044 % | c ============================================================================== c [1mFound solution: 1846876[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2151 | 71137 170506 | 23712 1903 35057 18.4 | 39.044 % | c ============================================================================== c [1mFound solution: 1846460[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2159 | 71168 170581 | 23722 1911 35174 18.4 | 39.044 % | c ============================================================================== c [1mFound solution: 1846459[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2177 | 71195 170646 | 23731 1929 35331 18.3 | 39.044 % | c ============================================================================== c [1mFound solution: 1846316[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2179 | 71221 170710 | 23740 1931 35339 18.3 | 39.044 % | c ============================================================================== c [1mFound solution: 1846124[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2181 | 71249 170778 | 23749 1933 35396 18.3 | 39.044 % | c ============================================================================== c [1mFound solution: 1845868[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2185 | 71273 170836 | 23757 1937 35632 18.4 | 39.044 % | c ============================================================================== c [1mFound solution: 1843564[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2245 | 71295 170890 | 23765 1997 37375 18.7 | 39.044 % | c | 2345 | 71016 170246 | 26141 2092 39683 19.0 | 39.207 % | c ============================================================================== c [1mFound solution: 1843563[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2443 | 71045 170317 | 23681 2190 41801 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843548[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2443 | 71070 170378 | 23690 2190 41801 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843547[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2443 | 71098 170446 | 23699 2190 41801 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843512[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2447 | 71128 170520 | 23709 2194 41815 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843511[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2452 | 71158 170594 | 23719 2199 41837 19.0 | 39.207 % | c ============================================================================== c [1mFound solution: 1843510[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2457 | 71187 170665 | 23729 2204 41850 19.0 | 39.207 % | c ============================================================================== c [1mFound solution: 1843507[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2458 | 71217 170739 | 23739 2205 41854 19.0 | 39.207 % | c ============================================================================== c [1mFound solution: 1843493[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2459 | 71249 170817 | 23749 2206 41856 19.0 | 39.207 % | c ============================================================================== c [1mFound solution: 1843489[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2460 | 71281 170895 | 23760 2207 41860 19.0 | 39.207 % | c ============================================================================== c [1mFound solution: 1843481[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2536 | 71182 170670 | 23727 2282 43861 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843465[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2538 | 71207 170731 | 23735 2284 43870 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843458[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2539 | 71235 170801 | 23745 2285 43873 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843457[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2539 | 71262 170868 | 23754 2285 43873 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843456[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2539 | 71287 170929 | 23762 2285 43873 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843353[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2541 | 71310 170986 | 23770 2287 43891 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843352[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2542 | 71340 171060 | 23780 2288 43895 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843337[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2543 | 71360 171110 | 23786 2289 43899 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843336[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2543 | 71383 171167 | 23794 2289 43899 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843288[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71410 171234 | 23803 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843272[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71438 171304 | 23812 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843264[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71466 171374 | 23822 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843260[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71490 171434 | 23830 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843256[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71510 171484 | 23836 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843240[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71538 171554 | 23846 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843232[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71566 171624 | 23855 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843228[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71591 171687 | 23863 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843224[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71612 171740 | 23870 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843220[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71638 171806 | 23879 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843216[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71653 171843 | 23884 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843212[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2544 | 71667 171877 | 23889 2290 43903 19.2 | 39.207 % | c ============================================================================== c [1mFound solution: 1843211[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2549 | 71690 171936 | 23896 2295 44203 19.3 | 39.207 % | c ============================================================================== c [1mFound solution: 1843209[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2619 | 71710 171986 | 23903 2365 45279 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843208[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2623 | 71731 172039 | 23910 2369 45311 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843207[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2623 | 71752 172092 | 23917 2369 45311 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843206[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2624 | 71779 172161 | 23926 2370 45313 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843205[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2624 | 71804 172224 | 23934 2370 45313 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843204[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2624 | 71822 172268 | 23940 2370 45313 19.1 | 39.207 % | c ============================================================================== c [1mFound solution: 1843200[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2625 | 71836 172302 | 23945 2371 45317 19.1 | 39.207 % | c ============================================================================== c [1mOptimal solution: 1843200[0m s OPTIMUM FOUND v -STM1_bit_7 -STM1_bit_6 -STM1_bit_5 -STM1_bit_4 -STM1_bit_3 -STM1_bit_2 -STM1_bit_1 -STM1_bit0 -STM1_bit1 STM1_bit2 STM1_bit3 STM1_bit4 STM1_bit5 -STM1_bit6 -STM1_bit7 -STM1_bit8 -STM1_bit9 -STM1_bit10 -STM1_bit11 -STM1_bit12 -ANM1_bit0 ANM1_bit1 ANM1_bit2 -ANM1_bit3 -ANM1_bit4 -UE1_bit_7 -UE1_bit_6 -UE1_bit_5 -UE1_bit_4 -UE1_bit_3 -UE1_bit_2 -UE1_bit_1 -UE1_bit0 -UE1_bit1 -UE1_bit2 -UE1_bit3 -UE1_bit4 -UE1_bit5 -UE1_bit6 -UE1_bit7 -UE1_bit8 -UE1_bit9 -UE1_bit10 -UE1_bit11 -UE1_bit12 STM2_bit0 STM2_bit1 -STM2_bit2 -STM2_bit3 -STM2_bit4 -ANM2_bit0 ANM2_bit1 ANM2_bit2 -ANM2_bit3 -ANM2_bit4 -UE2_bit_7 -UE2_bit_6 -UE2_bit_5 -UE2_bit_4 -UE2_bit_3 -UE2_bit_2 -UE2_bit_1 -UE2_bit0 -UE2_bit1 -UE2_bit2 UE2_bit3 UE2_bit4 -UE2_bit5 UE2_bit6 -UE2_bit7 -UE2_bit8 UE2_bit9 -UE2_bit10 -UE2_bit11 -UE2_bit12 STM3_bit0 STM3_bit1 -STM3_bit2 -STM3_bit3 -STM3_bit4 -ANM3_bit0 -ANM3_bit1 -ANM3_bit2 -ANM3_bit3 ANM3_bit4 -UE3_bit_7 -UE3_bit_6 -UE3_bit_5 -UE3_bit_4 -UE3_bit_3 -UE3_bit_2 -UE3_bit_1 -UE3_bit0 -UE3_bit1 -UE3_bit2 UE3_bit3 UE3_bit4 -UE3_bit5 UE3_bit6 -UE3_bit7 -UE3_bit8 UE3_bit9 -UE3_bit10 -UE3_bit11 -UE3_bit12 STM4_bit0 -STM4_bit1 STM4_bit2 STM4_bit3 -STM4_bit4 ANM4_bit0 ANM4_bit1 ANM4_bit2 -ANM4_bit3 -ANM4_bit4 -UE4_bit_7 -UE4_bit_6 -UE4_bit_5 -UE4_bit_4 -UE4_bit_3 -UE4_bit_2 -UE4_bit_1 -UE4_bit0 -UE4_bit1 -UE4_bit2 UE4_bit3 -UE4_bit4 -UE4_bit5 UE4_bit6 UE4_bit7 -UE4_bit8 -UE4_bit9 -UE4_bit10 -UE4_bit11 -UE4_bit12 STM5_bit0 -STM5_bit1 STM5_bit2 STM5_bit3 -STM5_bit4 -ANM5_bit0 -ANM5_bit1 ANM5_bit2 ANM5_bit3 -ANM5_bit4 -UE5_bit_7 -UE5_bit_6 -UE5_bit_5 -UE5_bit_4 -UE5_bit_3 -UE5_bit_2 -UE5_bit_1 -UE5_bit0 -UE5_bit1 -UE5_bit2 -UE5_bit3 -UE5_bit4 -UE5_bit5 -UE5_bit6 -UE5_bit7 -UE5_bit8 -UE5_bit9 -UE5_bit10 -UE5_bit11 -UE5_bit12 -STM6_bit0 STM6_bit1 -STM6_bit2 -STM6_bit3 STM6_bit4 -ANM6_bit0 -ANM6_bit1 -ANM6_bit2 -ANM6_bit3 -ANM6_bit4 -UE6_bit_7 -UE6_bit_6 -UE6_bit_5 -UE6_bit_4 -UE6_bit_3 -UE6_bit_2 -UE6_bit_1 -UE6_bit0 UE6_bit1 UE6_bit2 UE6_bit3 -UE6_bit4 UE6_bit5 UE6_bit6 UE6_bit7 -UE6_bit8 UE6_bit9 -UE6_bit10 -UE6_bit11 -UE6_bit12 c _______________________________________________________________________________ c c restarts : 109 c conflicts : 2691 (116 /sec) c decisions : 12375 (533 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 23.2215 s c _______________________________________________________________________________ #### 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.56 0.86 0.88 2/55 960 Raw data (stat): 960 (runsolver) R 959 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 419004767 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.0002 s] Raw data (loadavg): 0.63 0.87 0.88 2/55 960 Raw data (stat): 960 (minisat+) R 959 30927 30926 0 -1 0 3639 0 0 0 990 8 0 0 25 0 1 0 419004767 17719296 3483 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4326 3483 603 41 0 4285 0 vsize: 17304 [startup+19.9999 s] Raw data (loadavg): 0.68 0.87 0.88 2/55 960 Raw data (stat): 960 (minisat+) R 959 30927 30926 0 -1 0 3697 0 0 0 1989 9 0 0 25 0 1 0 419004767 17948672 3541 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4382 3541 603 41 0 4341 0 vsize: 17528 [startup+23.359 s] Raw data (loadavg): 0.71 0.87 0.88 1/54 960 Raw data (stat): 960 (minisat+) R 959 30927 30926 0 -1 0 3697 0 0 0 1989 9 0 0 25 0 1 0 419004767 17948672 3541 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4382 3541 603 41 0 4341 0 vsize: 0 Child status: 30 Real time (s): 23.3587 CPU time (s): 23.3454 CPU user time (s): 23.2375 CPU system time (s): 0.107983 CPU usage (%): 99.9434 Max. virtual memory (Kb): 17528 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1843200 #### END VERIFIER DATA ####