Name | normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-6.opb |
MD5SUM | 5d90b7cbb5bac2aa14257b9c5448f25d |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 304 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 173 |
Biggest coefficient in the objective function | 100 |
Number of bits for the biggest coefficient in the objective function | 7 |
Sum of the numbers in the objective function | 8448 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 100 |
Number of bits of the biggest number in a constraint | 7 |
Biggest sum of numbers in a constraint | 8448 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.05184 |
Number of variables | 257 |
Total number of constraints | 353 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 353 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 44 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-14 05:02:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4868 boxname=wulflinc22 idbench=356 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5d90b7cbb5bac2aa14257b9c5448f25d /oldhome/oroussel/tmp/wulflinc22/normalized-ss97-6.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-ss97-6.opb /oldhome/oroussel/tmp/wulflinc22/normalized-ss97-6.opb IDLAUNCH: 4868 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 827320 kB Buffers: 33480 kB Cached: 130624 kB SwapCached: 524 kB Active: 51928 kB Inactive: 115556 kB HighTotal: 131008 kB HighFree: 6552 kB LowTotal: 903652 kB LowFree: 820768 kB SwapTotal: 2097892 kB SwapFree: 2097368 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 34164 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 05:02:31 (client local time) WITH STATUS 30 IN 4.25735 SECONDS stats: 4868 0 4.25735 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 180 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################################################################################### c -- Clauses(.)/Splits(s): (none) c ---[ 179]---> Sorter-cost: 694 Base: c ---[ 178]---> Sorter-cost: 694 Base: c ---[ 177]---> Sorter-cost: 694 Base: c ---[ 176]---> Sorter-cost: 694 Base: c ---[ 175]---> Sorter-cost: 610 Base: c ---[ 174]---> Sorter-cost: 610 Base: c ---[ 173]---> Sorter-cost: 262 Base: c ---[ 172]---> Sorter-cost: 262 Base: c ---[ 171]---> Sorter-cost: 262 Base: c ---[ 170]---> Sorter-cost: 262 Base: c ---[ 169]---> Sorter-cost: 170 Base: c ---[ 168]---> Sorter-cost: 170 Base: c ---[ 166]---> BDD-cost: 5 c ---[ 164]---> BDD-cost: 1 c ---[ 162]---> BDD-cost: 5 c ---[ 160]---> BDD-cost: 1 c ---[ 158]---> BDD-cost: 5 c ---[ 156]---> BDD-cost: 1 c ---[ 154]---> BDD-cost: 5 c ---[ 152]---> BDD-cost: 1 c ---[ 150]---> BDD-cost: 5 c ---[ 148]---> BDD-cost: 1 c ---[ 146]---> BDD-cost: 5 c ---[ 144]---> BDD-cost: 1 c ---[ 142]---> BDD-cost: 5 c ---[ 140]---> BDD-cost: 1 c ---[ 138]---> BDD-cost: 5 c ---[ 136]---> BDD-cost: 1 c ---[ 134]---> BDD-cost: 5 c ---[ 132]---> BDD-cost: 1 c ---[ 130]---> BDD-cost: 5 c ---[ 128]---> BDD-cost: 1 c ---[ 126]---> BDD-cost: 5 c ---[ 124]---> BDD-cost: 1 c ---[ 122]---> BDD-cost: 5 c ---[ 120]---> BDD-cost: 1 c ---[ 118]---> BDD-cost: 5 c ---[ 116]---> BDD-cost: 5 c ---[ 114]---> BDD-cost: 5 c ---[ 112]---> BDD-cost: 5 c ---[ 110]---> BDD-cost: 1 c ---[ 108]---> BDD-cost: 5 c ---[ 106]---> BDD-cost: 5 c ---[ 104]---> BDD-cost: 5 c ---[ 102]---> BDD-cost: 5 c ---[ 100]---> BDD-cost: 5 c ---[ 98]---> BDD-cost: 5 c ---[ 96]---> BDD-cost: 5 c ---[ 94]---> BDD-cost: 5 c ---[ 92]---> BDD-cost: 1 c ---[ 90]---> BDD-cost: 5 c ---[ 88]---> BDD-cost: 1 c ---[ 86]---> BDD-cost: 5 c ---[ 84]---> BDD-cost: 1 c ---[ 82]---> BDD-cost: 1 c ---[ 80]---> BDD-cost: 5 c ---[ 78]---> BDD-cost: 1 c ---[ 76]---> BDD-cost: 5 c ---[ 74]---> BDD-cost: 1 c ---[ 72]---> BDD-cost: 1 c ---[ 70]---> BDD-cost: 5 c ---[ 68]---> BDD-cost: 1 c ---[ 66]---> BDD-cost: 1 c ---[ 64]---> BDD-cost: 5 c ---[ 62]---> BDD-cost: 1 c ---[ 60]---> BDD-cost: 5 c ---[ 58]---> BDD-cost: 1 c ---[ 56]---> BDD-cost: 5 c ---[ 54]---> BDD-cost: 1 c ---[ 52]---> BDD-cost: 1 c ---[ 50]---> BDD-cost: 5 c ---[ 48]---> BDD-cost: 1 c ---[ 46]---> BDD-cost: 5 c ---[ 44]---> BDD-cost: 1 c ---[ 42]---> BDD-cost: 5 c ---[ 40]---> BDD-cost: 1 c ---[ 38]---> BDD-cost: 5 c ---[ 36]---> BDD-cost: 1 c ---[ 34]---> BDD-cost: 5 c ---[ 32]---> BDD-cost: 1 c ---[ 30]---> BDD-cost: 5 c ---[ 28]---> BDD-cost: 1 c ---[ 26]---> BDD-cost: 5 c ---[ 24]---> BDD-cost: 1 c ---[ 22]---> BDD-cost: 5 c ---[ 20]---> BDD-cost: 1 c ---[ 18]---> BDD-cost: 1 c ---[ 16]---> BDD-cost: 1 c ---[ 14]---> BDD-cost: 5 c ---[ 12]---> BDD-cost: 1 c ---[ 10]---> BDD-cost: 5 c ---[ 8]---> BDD-cost: 1 c ---[ 6]---> BDD-cost: 5 c ---[ 4]---> BDD-cost: 1 c ---[ 2]---> BDD-cost: 5 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 10608 25406 | 3536 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1915[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4055 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69 | 20234 47976 | 6744 69 437 6.3 | 0.000 % | c | 170 | 18886 44896 | 7418 140 860 6.1 | 7.648 % | c ============================================================================== c [1mFound solution: 1828[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 252 | 18053 43026 | 6017 180 1049 5.8 | 7.648 % | c | 352 | 17712 42245 | 6618 240 1323 5.5 | 14.416 % | c ============================================================================== c [1mFound solution: 1819[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 407 | 17847 42570 | 5949 295 1715 5.8 | 14.416 % | c ============================================================================== c [1mFound solution: 1818[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 431 | 17863 42608 | 5954 319 1843 5.8 | 14.416 % | c ============================================================================== c [1mFound solution: 1817[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 451 | 18006 42953 | 6002 339 1959 5.8 | 14.416 % | c | 551 | 17923 42763 | 6602 410 2428 5.9 | 15.181 % | c | 702 | 17923 42763 | 7262 561 3504 6.2 | 15.181 % | c | 927 | 17837 42567 | 7988 783 4707 6.0 | 15.545 % | c ============================================================================== c [1mFound solution: 1816[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 945 | 17943 42823 | 5981 801 4795 6.0 | 15.545 % | c | 1046 | 17792 42481 | 6579 896 5336 6.0 | 16.352 % | c ============================================================================== c [1mFound solution: 1719[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1063 | 17804 42511 | 5934 913 5412 5.9 | 16.352 % | c ============================================================================== c [1mFound solution: 1621[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1092 | 17854 42633 | 5951 942 5625 6.0 | 16.352 % | c ============================================================================== c [1mFound solution: 1619[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1179 | 17864 42659 | 5954 1029 6649 6.5 | 16.352 % | c | 1281 | 17813 42542 | 6549 1130 7434 6.6 | 16.561 % | c ============================================================================== c [1mFound solution: 1618[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1369 | 17711 42309 | 5903 1213 7942 6.5 | 16.561 % | c | 1471 | 17711 42309 | 6493 1315 8604 6.5 | 17.027 % | c | 1621 | 17580 42005 | 7142 1463 9625 6.6 | 17.622 % | c ============================================================================== c [1mFound solution: 1520[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1681 | 17153 41017 | 5717 1505 9876 6.6 | 17.622 % | c ============================================================================== c [1mFound solution: 1519[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1719 | 17118 40937 | 5706 1540 10080 6.5 | 17.622 % | c ============================================================================== c [1mFound solution: 1518[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1749 | 17122 40947 | 5707 1570 10244 6.5 | 17.622 % | c ============================================================================== c [1mFound solution: 1516[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1780 | 17120 40943 | 5706 1599 10444 6.5 | 17.622 % | c ============================================================================== c [1mFound solution: 1514[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1835 | 17112 40928 | 5704 1653 10802 6.5 | 17.622 % | c | 1935 | 17112 40928 | 6274 1753 11409 6.5 | 19.873 % | c ============================================================================== c [1mFound solution: 1513[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1976 | 17123 40955 | 5707 1794 11692 6.5 | 19.873 % | c | 2076 | 17064 40817 | 6277 1893 12384 6.5 | 20.152 % | c ============================================================================== c [1mFound solution: 1313[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2102 | 17103 40910 | 5701 1919 12576 6.6 | 20.152 % | c ============================================================================== c [1mFound solution: 1312[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2178 | 17114 40937 | 5704 1995 13094 6.6 | 20.152 % | c | 2278 | 17108 40923 | 6274 2093 13766 6.6 | 20.160 % | c ============================================================================== c [1mFound solution: 1311[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2288 | 17085 40871 | 5695 2082 13503 6.5 | 20.160 % | c | 2389 | 17075 40848 | 6264 2181 14360 6.6 | 20.369 % | c ============================================================================== c [1mFound solution: 1309[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2437 | 17084 40871 | 5694 2229 14771 6.6 | 20.369 % | c ============================================================================== c [1mFound solution: 1213[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2454 | 17112 40940 | 5704 2246 14834 6.6 | 20.369 % | c ============================================================================== c [1mFound solution: 1113[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2477 | 17126 40974 | 5708 2269 14989 6.6 | 20.369 % | c ============================================================================== c [1mFound solution: 1111[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2536 | 17130 40984 | 5710 2328 15325 6.6 | 20.369 % | c ============================================================================== c [1mFound solution: 1110[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2612 | 17092 40895 | 5697 2401 16148 6.7 | 20.369 % | c ============================================================================== c [1mFound solution: 1010[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2681 | 17114 40950 | 5704 2470 16621 6.7 | 20.369 % | c ============================================================================== c [1mFound solution: 1009[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2737 | 17126 40980 | 5708 2526 16970 6.7 | 20.369 % | c | 2837 | 17126 40980 | 6278 2626 17692 6.7 | 20.548 % | c ============================================================================== c [1mFound solution: 917[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2860 | 17137 41007 | 5712 2649 17810 6.7 | 20.548 % | c ============================================================================== c [1mFound solution: 916[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2876 | 17141 41017 | 5713 2665 17896 6.7 | 20.548 % | c ============================================================================== c [1mFound solution: 915[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2886 | 17098 40920 | 5699 2673 17956 6.7 | 20.548 % | c ============================================================================== c [1mFound solution: 914[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2906 | 17102 40930 | 5700 2693 18071 6.7 | 20.548 % | c ============================================================================== c [1mFound solution: 816[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2938 | 17118 40970 | 5706 2725 18255 6.7 | 20.548 % | c ============================================================================== c [1mFound solution: 809[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2955 | 17126 40990 | 5708 2742 18362 6.7 | 20.548 % | c | 3055 | 17126 40990 | 6278 2842 19130 6.7 | 20.790 % | c ============================================================================== c [1mFound solution: 808[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3078 | 17121 40983 | 5707 2862 19266 6.7 | 20.790 % | c ============================================================================== c [1mFound solution: 807[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3123 | 17130 41006 | 5710 2907 19569 6.7 | 20.790 % | c ============================================================================== c [1mFound solution: 709[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3140 | 17140 41030 | 5713 2924 19702 6.7 | 20.790 % | c | 3240 | 17140 41030 | 6284 3024 21017 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 609[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3287 | 17155 41067 | 5718 3071 21414 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 608[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3303 | 17166 41094 | 5722 3087 21521 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 509[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3309 | 17176 41118 | 5725 3093 21579 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 508[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3321 | 17180 41128 | 5726 3105 21640 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 507[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3323 | 17187 41145 | 5729 3107 21656 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 506[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3328 | 17196 41168 | 5732 3112 21678 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 409[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3353 | 17205 41189 | 5735 3137 21954 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 309[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3367 | 8929 21655 | 2976 1286 9037 7.0 | 20.857 % | c ============================================================================== c [1mFound solution: 304[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1933 Base: 5 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3373 | 13078 31300 | 4359 1265 8706 6.9 | 20.857 % | c | 3473 | 12096 29092 | 4794 1330 9287 7.0 | 52.202 % | c | 3623 | 10867 26269 | 5274 1417 9877 7.0 | 56.595 % | c ============================================================================== c [1mOptimal solution: 304[0m s OPTIMUM FOUND v v133 -v177 v217 v3 v179 v7 v8 -v96 v184 -v224 -v185 v225 -v10 -v98 v142 v186 -v226 v99 v12 v13 -v14 v58 v103 -v60 -v104 v148 v229 v61 v19 -v107 -v108 v152 v21 -v109 -v153 -v110 v154 v111 v191 -v231 -v26 v70 v236 v117 v197 -v237 v198 -v238 v118 -v199 v239 v163 v120 -v201 v241 -v202 v242 -v121 v203 -v243 -v123 v167 -v205 v245 v124 v246 -v37 -v125 v169 -v207 v247 v126 v248 -v39 v171 v249 -v212 v252 v129 v213 -v253 v130 -v214 v254 v131 -v215 v255 v132 v256 -v1 -v45 -v89 -v90 -v178 -v47 -v219 -v221 -v223 -v52 -v140 -v11 -v55 -v143 -v227 -v56 -v144 -v228 -v57 -v145 -v102 -v146 -v15 -v147 -v17 -v149 v18 -v62 -v106 -v150 -v151 -v65 -v23 -v67 -v155 -v24 v68 -v112 -v156 -v190 v230 -v158 -v232 -v233 -v234 -v235 -v29 -v73 -v161 -v30 -v74 -v162 -v75 -v119 -v240 -v32 -v76 -v164 -v33 -v165 -v34 -v78 -v244 -v79 -v80 -v168 -v81 -v38 -v82 -v170 -v83 -v127 -v41 -v85 -v173 -v42 -v86 -v174 -v43 -v87 -v175 -v176 -v216 one -v2 -v4 -v5 -v6 -v9 -v16 -v20 -v22 -v25 -v27 v28 -v31 -v35 -v36 v40 -v44 v46 v48 v49 v50 -v51 v53 -v54 -v59 -v63 -v64 -v66 v69 v71 -v72 v77 -v84 -v88 -v91 -v92 -v93 -v94 -v95 -v97 -v100 -v101 -v105 -v113 -v114 -v115 -v116 -v122 -v128 -v134 -v135 -v136 -v137 -v138 -v139 -v141 -v157 -v159 -v160 v166 -v172 -v180 v181 -v182 v183 v187 v188 -v189 v192 v193 v194 v195 -v196 v200 v204 -v206 -v208 -v209 v210 v211 v218 v220 v222 -v250 -v251 c _______________________________________________________________________________ c c restarts : 63 c conflicts : 3643 (864 /sec) c decisions : 17680 (4192 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 4.21736 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.86 0.97 0.91 2/54 32366 Raw data (stat): 32366 (runsolver) R 32365 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481914642 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+4.26943 s] Raw data (loadavg): 0.87 0.97 0.91 1/53 32366 Raw data (stat): 32366 (runsolver) R 32365 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481914642 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 0 Child status: 30 Real time (s): 4.26886 CPU time (s): 4.25735 CPU user time (s): 4.22136 CPU system time (s): 0.035994 CPU usage (%): 99.7305 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 304 #### END VERIFIER DATA ####