Name | normalized-opb/submitted/een/normalized-mod008.opb |
MD5SUM | 18b325bb9311c83b0604c703bacc9a29 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 87 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 319 |
Biggest coefficient in the objective function | 87 |
Number of bits for the biggest coefficient in the objective function | 7 |
Sum of the numbers in the objective function | 23554 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 7499 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 758444 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.283956 |
Number of variables | 319 |
Total number of constraints | 6 |
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 | 6 |
Minimum length of a constraint | 186 |
Maximum length of a constraint | 231 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc5 THE 2005-04-14 21:14:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=5146 boxname=wulflinc5 idbench=396 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 18b325bb9311c83b0604c703bacc9a29 /oldhome/oroussel/tmp/wulflinc5/normalized-mod008.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-mod008.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mod008.opb IDLAUNCH: 5146 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 882644 kB Buffers: 35672 kB Cached: 94520 kB SwapCached: 2272 kB Active: 60320 kB Inactive: 74968 kB HighTotal: 131008 kB HighFree: 32648 kB LowTotal: 903652 kB LowFree: 849996 kB SwapTotal: 2097136 kB SwapFree: 2094864 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6924 kB Slab: 11120 kB Committed_AS: 63472 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 21:17:26 (client local time) WITH STATUS 30 IN 172.335 SECONDS stats: 5146 0 172.335 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 6 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): sss.ss c ---[ 4]---> BDD-cost: 105 c ---[ 3]---> BDD-cost: 168 c ---[ 2]---> BDD-cost: 223 c ---[ 1]---> Sorter-cost: 663 Base: 3 c ---[ 0]---> Sorter-cost: 354 Base: 11 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 2343 7303 | 702 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/1342 c -- var.elim.: 1342/1342 c -- var.elim.: 786/786 c -- var.elim.: 361/361 c -- var.elim.: 239/239 c -- subsuming c -- var.elim.: 507/507 c -- var.elim.: 332/332 c -- var.elim.: 4/4 c -- var.elim.: 228/228 c | 0 | 1682 15611 | -- 0 -- -- | -- | -661/8313 c | 0 | 1682 15611 | 672 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.484926 s) c ============================================================================== c [1mFound solution: 3002[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:61666 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 152897 368710 | 45869 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/56152 c -- var.elim.: 2000/56152 c -- var.elim.: 3000/56152 c -- var.elim.: 4000/56152 c -- var.elim.: 5000/56152 c -- var.elim.: 6000/56152 c -- var.elim.: 7000/56152 c -- var.elim.: 8000/56152 c -- var.elim.: 9000/56152 c -- var.elim.: 10000/56152 c -- var.elim.: 11000/56152 c -- var.elim.: 12000/56152 c -- var.elim.: 13000/56152 c -- var.elim.: 14000/56152 c -- var.elim.: 15000/56152 c -- var.elim.: 16000/56152 c -- var.elim.: 17000/56152 c -- var.elim.: 18000/56152 c -- var.elim.: 19000/56152 c -- var.elim.: 20000/56152 c -- var.elim.: 21000/56152 c -- var.elim.: 22000/56152 c -- var.elim.: 23000/56152 c -- var.elim.: 24000/56152 c -- var.elim.: 25000/56152 c -- var.elim.: 26000/56152 c -- var.elim.: 27000/56152 c -- var.elim.: 28000/56152 c -- var.elim.: 29000/56152 c -- var.elim.: 30000/56152 c -- var.elim.: 31000/56152 c -- var.elim.: 32000/56152 c -- var.elim.: 33000/56152 c -- var.elim.: 34000/56152 c -- var.elim.: 35000/56152 c -- var.elim.: 36000/56152 c -- var.elim.: 37000/56152 c -- var.elim.: 38000/56152 c -- var.elim.: 39000/56152 c -- var.elim.: 40000/56152 c -- var.elim.: 41000/56152 c -- var.elim.: 42000/56152 c -- var.elim.: 43000/56152 c -- var.elim.: 44000/56152 c -- var.elim.: 45000/56152 c -- var.elim.: 46000/56152 c -- var.elim.: 47000/56152 c -- var.elim.: 48000/56152 c -- var.elim.: 49000/56152 c -- var.elim.: 50000/56152 c -- var.elim.: 51000/56152 c -- var.elim.: 52000/56152 c -- var.elim.: 53000/56152 c -- var.elim.: 54000/56152 c -- var.elim.: 55000/56152 c -- var.elim.: 56000/56152 c -- var.elim.: 56152/56152 c -- var.elim.: 1000/30101 c -- var.elim.: 2000/30101 c -- var.elim.: 3000/30101 c -- var.elim.: 4000/30101 c -- var.elim.: 5000/30101 c -- var.elim.: 6000/30101 c -- var.elim.: 7000/30101 c -- var.elim.: 8000/30101 c -- var.elim.: 9000/30101 c -- var.elim.: 10000/30101 c -- var.elim.: 11000/30101 c -- var.elim.: 12000/30101 c -- var.elim.: 13000/30101 c -- var.elim.: 14000/30101 c -- var.elim.: 15000/30101 c -- var.elim.: 16000/30101 c -- var.elim.: 17000/30101 c -- var.elim.: 18000/30101 c -- var.elim.: 19000/30101 c -- var.elim.: 20000/30101 c -- var.elim.: 21000/30101 c -- var.elim.: 22000/30101 c -- var.elim.: 23000/30101 c -- var.elim.: 24000/30101 c -- var.elim.: 25000/30101 c -- var.elim.: 26000/30101 c -- var.elim.: 27000/30101 c -- var.elim.: 28000/30101 c -- var.elim.: 29000/30101 c -- var.elim.: 30000/30101 c -- var.elim.: 30101/30101 c -- var.elim.: 564/564 c -- subsuming c -- var.elim.: 1000/5286 c -- var.elim.: 2000/5286 c -- var.elim.: 3000/5286 c -- var.elim.: 4000/5286 c -- var.elim.: 5000/5286 c -- var.elim.: 5286/5286 c -- var.elim.: 204/204 c -- subsuming c -- var.elim.: 79/79 c -- var.elim.: 7/7 c | 0 | 135835 458593 | -- 0 -- -- | -- | -17062/89884 c | 0 | 135835 458593 | 54334 0 0 nan | 0.000 % | c | 100 | 135835 458593 | 59767 100 1626 16.3 | 0.020 % | c | 250 | 135835 458593 | 65744 250 2927 11.7 | 0.020 % | c | 475 | 135835 458593 | 72318 475 4568 9.6 | 0.020 % | c | 814 | 135835 458593 | 79550 814 10797 13.3 | 0.020 % | c | 1322 | 135835 458593 | 87505 1322 131461 99.4 | 0.020 % | c | 2082 | 135835 458593 | 96255 2082 209718 100.7 | 0.020 % | c | 3223 | 135835 458593 | 105881 3223 276264 85.7 | 0.020 % | c | 4932 | 135835 458593 | 116469 4932 331702 67.3 | 0.020 % | c | 7494 | 135835 458593 | 128116 7494 374019 49.9 | 0.020 % | c | 11339 | 135835 458593 | 140928 11339 476841 42.1 | 0.020 % | c | 17105 | 135835 458593 | 155021 17105 707933 41.4 | 0.020 % | c ============================================================================== c (current CPU-time: 52.438 s) c ============================================================================== c [1mFound solution: 2698[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 17492 | 137791 463951 | 41337 17492 735744 42.1 | 0.020 % | c -- subsuming c -- var.elim.: 1000/3103 c -- var.elim.: 2000/3103 c -- var.elim.: 3000/3103 c -- var.elim.: 3103/3103 c -- var.elim.: 1000/1742 c -- var.elim.: 1742/1742 c -- subsuming c -- var.elim.: 117/117 c | 17492 | 136672 464529 | -- 17492 -- -- | -- | -1119/579 c | 17492 | 136672 464529 | 54668 17492 735744 42.1 | 0.020 % | c | 17592 | 136672 464529 | 60135 17592 736518 41.9 | 0.023 % | c | 17742 | 136672 464529 | 66149 17742 738562 41.6 | 0.023 % | c | 17967 | 136672 464529 | 72764 17967 741327 41.3 | 0.023 % | c | 18304 | 136672 464529 | 80040 18304 743519 40.6 | 0.023 % | c | 18810 | 136672 464529 | 88044 18810 790898 42.0 | 0.023 % | c | 19569 | 136672 464529 | 96849 19569 801850 41.0 | 0.023 % | c | 20708 | 136672 464529 | 106534 20708 814472 39.3 | 0.023 % | c | 22417 | 136672 464529 | 117187 22417 913646 40.8 | 0.023 % | c | 24980 | 136672 464529 | 128906 24980 967008 38.7 | 0.023 % | c | 28824 | 136672 464529 | 141796 28824 1088444 37.8 | 0.023 % | c ============================================================================== c (current CPU-time: 76.7673 s) c ============================================================================== c [1mFound solution: 2651[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 31430 | 138071 468400 | 41421 31430 1139487 36.3 | 0.023 % | c -- subsuming c -- var.elim.: 1000/2264 c -- var.elim.: 2000/2264 c -- var.elim.: 2264/2264 c -- var.elim.: 1000/1311 c -- var.elim.: 1311/1311 c -- subsuming c -- var.elim.: 95/95 c | 31430 | 137276 468638 | -- 31430 -- -- | -- | -795/239 c | 31430 | 137276 468638 | 54910 31430 1139487 36.3 | 0.023 % | c | 31530 | 137276 468638 | 60401 31530 1140241 36.2 | 0.026 % | c | 31680 | 137276 468638 | 66441 31680 1156169 36.5 | 0.026 % | c | 31905 | 137276 468638 | 73085 31905 1168770 36.6 | 0.026 % | c ============================================================================== c (current CPU-time: 80.7647 s) c ============================================================================== c [1mFound solution: 2640[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 31969 | 137220 468817 | 41165 31963 1170179 36.6 | 0.026 % | c -- subsuming c -- var.elim.: 505/505 c -- var.elim.: 782/782 c | 31969 | 137189 469404 | -- 31963 -- -- | -- | -31/588 c | 31969 | 137189 469404 | 54875 31963 1170179 36.6 | 0.026 % | c | 32069 | 137189 469404 | 60363 32063 1183569 36.9 | 0.071 % | c | 32221 | 137189 469404 | 66399 32215 1184697 36.8 | 0.071 % | c | 32447 | 137189 469404 | 73039 32441 1186609 36.6 | 0.071 % | c | 32784 | 137189 469404 | 80343 32778 1192205 36.4 | 0.071 % | c | 33290 | 137189 469404 | 88377 33284 1202462 36.1 | 0.071 % | c | 34049 | 137189 469404 | 97215 34043 1222962 35.9 | 0.071 % | c | 35190 | 137189 469404 | 106937 35184 1238927 35.2 | 0.071 % | c | 36899 | 137189 469404 | 117630 36893 1261287 34.2 | 0.071 % | c ============================================================================== c (current CPU-time: 95.1195 s) c ============================================================================== c [1mFound solution: 2603[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 37476 | 137352 470263 | 41205 37470 1278740 34.1 | 0.071 % | c -- subsuming c -- var.elim.: 780/780 c -- var.elim.: 569/569 c -- var.elim.: 11/11 c -- var.elim.: 242/242 c | 37476 | 137231 470894 | -- 37470 -- -- | -- | -121/632 c | 37476 | 137231 470894 | 54892 36832 1149670 31.2 | 0.071 % | c | 37577 | 137231 470894 | 60381 36933 1155361 31.3 | 0.074 % | c | 37727 | 137231 470894 | 66419 37083 1156353 31.2 | 0.074 % | c ============================================================================== c (current CPU-time: 96.9663 s) c ============================================================================== c [1mFound solution: 1186[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 37816 | 137692 472517 | 41307 37172 1156853 31.1 | 0.074 % | c -- subsuming c -- var.elim.: 1000/1085 c -- var.elim.: 1085/1085 c -- var.elim.: 741/741 c -- var.elim.: 112/112 c -- subsuming c -- var.elim.: 147/147 c | 37816 | 137386 472895 | -- 37172 -- -- | -- | -306/379 c | 37816 | 137386 472895 | 54954 37172 1156853 31.1 | 0.074 % | c ============================================================================== c (current CPU-time: 98.2901 s) c ============================================================================== c [1mFound solution: 1104[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 37837 | 138946 477179 | 41683 37193 1160482 31.2 | 0.074 % | c -- subsuming c -- var.elim.: 1000/2607 c -- var.elim.: 2000/2607 c -- var.elim.: 2607/2607 c -- var.elim.: 1000/1515 c -- var.elim.: 1515/1515 c -- var.elim.: 10/10 c -- var.elim.: 16/16 c -- subsuming c -- var.elim.: 26/26 c | 37837 | 138035 477282 | -- 37193 -- -- | -- | -911/104 c | 37837 | 138035 477282 | 55214 37193 1160482 31.2 | 0.074 % | c ============================================================================== c (current CPU-time: 100.235 s) c ============================================================================== c [1mFound solution: 785[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 37913 | 138262 478139 | 41478 37269 1173373 31.5 | 0.074 % | c -- subsuming c -- var.elim.: 598/598 c -- var.elim.: 432/432 c | 37913 | 138118 480051 | -- 37269 -- -- | -- | -144/1913 c | 37913 | 138118 480051 | 55247 37269 1173373 31.5 | 0.074 % | c | 38013 | 138080 477715 | 60755 37368 1185586 31.7 | 0.093 % | c | 38164 | 137952 477188 | 66768 37475 1187423 31.7 | 0.144 % | c ============================================================================== c (current CPU-time: 104.617 s) c ============================================================================== c [1mFound solution: 744[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38178 | 137976 477326 | 41392 37489 1191699 31.8 | 0.144 % | c -- subsuming c -- var.elim.: 526/526 c -- var.elim.: 1000/1066 c -- var.elim.: 1066/1066 c -- var.elim.: 671/671 c -- var.elim.: 451/451 c -- subsuming c -- var.elim.: 806/806 c -- var.elim.: 5/5 c | 38178 | 137922 479083 | -- 37489 -- -- | -- | -54/1758 c | 38178 | 137922 479083 | 55168 37074 1080637 29.1 | 0.144 % | c | 38278 | 137922 479083 | 60685 37174 1083254 29.1 | 0.148 % | c ============================================================================== c (current CPU-time: 108.321 s) c ============================================================================== c [1mFound solution: 668[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38342 | 138024 479830 | 41407 37238 1084026 29.1 | 0.148 % | c -- subsuming c -- var.elim.: 946/946 c -- var.elim.: 572/572 c -- var.elim.: 295/295 c -- var.elim.: 108/108 c | 38342 | 137951 480677 | -- 37238 -- -- | -- | -68/860 c | 38342 | 137951 480677 | 55180 37238 1084026 29.1 | 0.148 % | c ============================================================================== c (current CPU-time: 109.697 s) c ============================================================================== c [1mFound solution: 662[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38354 | 137978 480823 | 41393 37250 1084144 29.1 | 0.148 % | c -- subsuming c -- var.elim.: 200/200 c -- var.elim.: 101/101 c -- var.elim.: 81/81 c | 38354 | 137959 480797 | -- 37250 -- -- | -- | -19/-25 c | 38354 | 137959 480797 | 55183 37250 1084144 29.1 | 0.148 % | c ============================================================================== c (current CPU-time: 110.712 s) c ============================================================================== c [1mFound solution: 660[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38355 | 137986 480943 | 41395 37251 1084162 29.1 | 0.148 % | c -- subsuming c -- var.elim.: 116/116 c -- var.elim.: 101/101 c -- var.elim.: 81/81 c | 38355 | 137967 480920 | -- 37251 -- -- | -- | -19/-22 c | 38355 | 137967 480920 | 55186 37251 1084162 29.1 | 0.148 % | c ============================================================================== c (current CPU-time: 111.857 s) c ============================================================================== c [1mFound solution: 577[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38368 | 138026 481486 | 41407 37264 1085415 29.1 | 0.148 % | c -- subsuming c -- var.elim.: 499/499 c -- var.elim.: 465/465 c -- var.elim.: 90/90 c -- var.elim.: 112/112 c | 38368 | 137987 481967 | -- 37264 -- -- | -- | -39/482 c | 38368 | 137987 481967 | 55194 37264 1085415 29.1 | 0.148 % | c ============================================================================== c (current CPU-time: 113.995 s) c ============================================================================== c [1mFound solution: 500[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38418 | 138131 482665 | 41439 37314 1096771 29.4 | 0.148 % | c -- subsuming c -- var.elim.: 550/550 c -- var.elim.: 440/440 c | 38418 | 138010 482789 | -- 37314 -- -- | -- | -121/125 c | 38418 | 138010 482789 | 55204 37314 1096771 29.4 | 0.148 % | c | 38520 | 137933 481853 | 60690 37413 1108522 29.6 | 0.205 % | c | 38670 | 137636 480431 | 66615 37492 1118120 29.8 | 0.331 % | c ============================================================================== c (current CPU-time: 117.613 s) c ============================================================================== c [1mFound solution: 468[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38677 | 137659 480672 | 41297 37499 1118575 29.8 | 0.331 % | c -- subsuming c -- var.elim.: 1000/1560 c -- var.elim.: 1560/1560 c -- var.elim.: 805/805 c -- var.elim.: 79/79 c -- subsuming c -- var.elim.: 629/629 c -- var.elim.: 10/10 c | 38677 | 137592 481285 | -- 37499 -- -- | -- | -67/614 c | 38677 | 137592 481285 | 55036 37290 1073090 28.8 | 0.331 % | c | 38777 | 137592 481285 | 60540 37390 1075888 28.8 | 0.334 % | c | 38927 | 137592 481285 | 66594 37540 1077926 28.7 | 0.334 % | c ============================================================================== c (current CPU-time: 127.163 s) c ============================================================================== c [1mFound solution: 280[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 39121 | 137373 479807 | 41211 37141 944406 25.4 | 0.334 % | c -- subsuming c -- var.elim.: 525/525 c -- var.elim.: 406/406 c -- var.elim.: 79/79 c | 39121 | 137348 479785 | -- 37141 -- -- | -- | -25/-21 c | 39121 | 137348 479785 | 54939 37141 944406 25.4 | 0.334 % | c ============================================================================== c (current CPU-time: 129.274 s) c ============================================================================== c [1mFound solution: 277[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 39148 | 137419 480374 | 41225 37168 949616 25.5 | 0.334 % | c -- subsuming c -- var.elim.: 507/507 c -- var.elim.: 463/463 c -- var.elim.: 197/197 c -- var.elim.: 112/112 c | 39148 | 137363 480572 | -- 37168 -- -- | -- | -56/199 c | 39148 | 137363 480572 | 54945 36671 912999 24.9 | 0.334 % | c | 39248 | 137363 480572 | 60439 36771 924080 25.1 | 0.434 % | c | 39398 | 137363 480572 | 66483 36921 929239 25.2 | 0.434 % | c ============================================================================== c (current CPU-time: 132.689 s) c ============================================================================== c [1mFound solution: 208[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 39412 | 137388 480816 | 41216 36935 933314 25.3 | 0.434 % | c -- subsuming c -- var.elim.: 217/217 c -- var.elim.: 203/203 c | 39412 | 137378 481180 | -- 36935 -- -- | -- | -10/365 c | 39412 | 137378 481180 | 54951 36935 933314 25.3 | 0.434 % | c ============================================================================== c (current CPU-time: 134.312 s) c ============================================================================== c [1mFound solution: 190[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 2407 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 39455 | 143994 499853 | 43198 36978 939333 25.4 | 0.434 % | c -- subsuming c -- var.elim.: 1000/2718 c -- var.elim.: 2000/2718 c -- var.elim.: 2718/2718 c -- var.elim.: 42/42 c | 39455 | 143992 499866 | -- 36978 -- -- | -- | -2/16 c | 39455 | 143992 499866 | 57596 36978 939333 25.4 | 0.434 % | c | 39556 | 143992 499866 | 63356 37079 969262 26.1 | 0.409 % | c | 39709 | 143992 499866 | 69692 37232 1099247 29.5 | 0.409 % | c ============================================================================== c (current CPU-time: 140.843 s) c ============================================================================== c [1mFound solution: 128[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 527 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 39786 | 145189 503106 | 43556 37309 1118960 30.0 | 0.409 % | c -- subsuming c -- var.elim.: 862/862 c -- var.elim.: 56/56 c | 39786 | 145182 503101 | -- 37309 -- -- | -- | -7/-2 c | 39786 | 145182 503101 | 58072 37309 1118960 30.0 | 0.409 % | c ============================================================================== c (current CPU-time: 142.079 s) c ============================================================================== c [1mFound solution: 124[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 265 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 39845 | 145958 505367 | 43787 37368 1134303 30.4 | 0.409 % | c -- subsuming c -- var.elim.: 768/768 c -- var.elim.: 16/16 c | 39845 | 145947 505336 | -- 37368 -- -- | -- | -11/-28 c | 39845 | 145947 505336 | 58378 37368 1134303 30.4 | 0.409 % | c | 39945 | 145947 505336 | 64216 37468 1163151 31.0 | 0.407 % | c | 40095 | 145947 505336 | 70638 37618 1165911 31.0 | 0.407 % | c | 40320 | 145656 504321 | 77547 37745 1190324 31.5 | 0.516 % | c | 40659 | 145656 504321 | 85301 38084 1265009 33.2 | 0.516 % | c ============================================================================== c (current CPU-time: 165.649 s) c ============================================================================== c [1mFound solution: 87[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 0 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 40998 | 145656 504321 | 43696 38423 1323811 34.5 | 0.516 % | c -- subsuming c -- var.elim.: 1000/3769 c -- var.elim.: 2000/3769 c -- var.elim.: 3000/3769 c -- var.elim.: 3769/3769 c -- var.elim.: 1000/2702 c -- var.elim.: 2000/2702 c -- var.elim.: 2702/2702 c -- var.elim.: 1000/1034 c -- var.elim.: 1034/1034 c -- var.elim.: 846/846 c -- var.elim.: 638/638 c -- var.elim.: 36/36 c -- subsuming c -- var.elim.: 576/576 c -- var.elim.: 18/18 c | 40998 | 138259 475816 | -- 38423 -- -- | -- | -743/-1419 c | 40998 | 138259 475816 | 55303 32245 681880 21.1 | 0.516 % | c ============================================================================== c [1mOptimal solution: 87[0m s OPTIMUM FOUND v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 x318 c _______________________________________________________________________________ c c restarts : 72 c conflicts : 41004 (241 /sec) c decisions : 132187 (776 /sec) c propagations : 42923789 (251987 /sec) c inspects : 175612799 (1030948 /sec) c CPU time : 170.341 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): 1.04 0.99 0.89 2/54 1754 Raw data (stat): 1754 (runsolver) R 1753 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429528948 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0009 s] Raw data (loadavg): 1.03 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 8879 0 0 0 959 32 0 0 25 0 1 0 429528948 38989824 8374 4294967295 134512640 134672761 3221224576 3221222880 134621829 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9519 8374 603 41 0 9478 0 vsize: 38076 [startup+20.0015 s] Raw data (loadavg): 1.03 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9382 0 0 0 1957 33 0 0 25 0 1 0 429528948 39256064 8452 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9584 8452 603 41 0 9543 0 vsize: 38336 [startup+30.0019 s] Raw data (loadavg): 1.02 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9573 0 0 0 2957 33 0 0 25 0 1 0 429528948 40046592 8643 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9777 8643 603 41 0 9736 0 vsize: 39108 [startup+40.0023 s] Raw data (loadavg): 1.02 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9670 0 0 0 3956 34 0 0 25 0 1 0 429528948 40341504 8740 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9849 8740 603 41 0 9808 0 vsize: 39396 [startup+50.0027 s] Raw data (loadavg): 1.01 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9903 0 0 0 4955 35 0 0 25 0 1 0 429528948 41402368 8973 4294967295 134512640 134672761 3221224576 3221223396 1075755419 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10108 8973 603 41 0 10067 0 vsize: 40432 [startup+60.0032 s] Raw data (loadavg): 1.01 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 12371 0 0 0 5946 43 0 0 25 0 1 0 429528948 42967040 9223 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10490 9223 603 41 0 10449 0 vsize: 41960 [startup+70.0042 s] Raw data (loadavg): 1.01 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 12512 0 0 0 6946 43 0 0 25 0 1 0 429528948 43626496 9364 4294967295 134512640 134672761 3221224576 3221223760 134615576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10651 9364 603 41 0 10610 0 vsize: 42604 [startup+80.005 s] Raw data (loadavg): 1.01 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 15411 0 0 0 7936 53 0 0 25 0 1 0 429528948 44793856 9701 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10936 9701 603 41 0 10895 0 vsize: 43744 [startup+90.0054 s] Raw data (loadavg): 1.01 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 17779 0 0 0 8928 61 0 0 25 0 1 0 429528948 45281280 9778 4294967295 134512640 134672761 3221224576 3221223744 134615859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11055 9778 603 41 0 11014 0 vsize: 44220 [startup+100.006 s] Raw data (loadavg): 1.00 0.99 0.90 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 24129 0 0 0 9907 82 0 0 25 0 1 0 429528948 45887488 9972 4294967295 134512640 134672761 3221224576 3221223296 134564856 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11203 9972 603 41 0 11162 0 vsize: 44812 [startup+110.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 30931 0 0 0 10883 106 0 0 25 0 1 0 429528948 53121024 11582 4294967295 134512640 134672761 3221224576 3221222792 1075349620 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12969 11582 603 41 0 12928 0 vsize: 51876 [startup+120.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 41691 0 0 0 11847 141 0 0 25 0 1 0 429528948 47714304 10286 4294967295 134512640 134672761 3221224576 3221223120 134621122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11649 10286 603 41 0 11608 0 vsize: 46596 [startup+130.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 44001 0 0 0 12838 150 0 0 25 0 1 0 429528948 45895680 9989 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11205 9989 603 41 0 11164 0 vsize: 44820 [startup+140.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 50096 0 0 0 13817 170 0 0 25 0 1 0 429528948 45969408 10061 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11223 10061 603 41 0 11182 0 vsize: 44892 [startup+150.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 54850 0 0 0 14802 184 0 0 25 0 1 0 429528948 47083520 10289 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11495 10289 603 41 0 11454 0 vsize: 45980 [startup+160.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 54968 0 0 0 15802 184 0 0 25 0 1 0 429528948 47476736 10407 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11591 10407 603 41 0 11550 0 vsize: 46364 [startup+170.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 57621 0 0 0 16794 193 0 0 25 0 1 0 429528948 49856512 10821 4294967295 134512640 134672761 3221224576 3221223120 134621041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12172 10821 603 41 0 12131 0 vsize: 48688 [startup+172.466 s] Raw data (loadavg): 1.00 0.99 0.91 1/53 1754 Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 57621 0 0 0 16794 193 0 0 25 0 1 0 429528948 49856512 10821 4294967295 134512640 134672761 3221224576 3221223120 134621041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12172 10821 603 41 0 12131 0 vsize: 0 Child status: 30 Real time (s): 172.466 CPU time (s): 172.335 CPU user time (s): 170.365 CPU system time (s): 1.9697 CPU usage (%): 99.9239 Max. virtual memory (Kb): 51876 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 87 #### END VERIFIER DATA ####