Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-flugpl.opb |
MD5SUM | 61de485815c789896436963a585e8ab7 |
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.183971 |
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 wulflinc19 THE 2005-04-21 05:36:55 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16858 boxname=wulflinc19 idbench=1297 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 61de485815c789896436963a585e8ab7 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-flugpl.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-flugpl.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-flugpl.opb IDLAUNCH: 16858 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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.037 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: 683568 kB Buffers: 22128 kB Cached: 301200 kB SwapCached: 556 kB Active: 80428 kB Inactive: 244960 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 683316 kB SwapTotal: 2097892 kB SwapFree: 2096436 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5200 kB Slab: 20016 kB Committed_AS: 63820 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 05:37:01 (client local time) WITH STATUS 30 IN 6.09407 SECONDS stats: 16858 0 6.09407 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]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 33]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 32]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 31]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 30]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 29]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 28]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 27]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 26]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 25]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 24]---> Adder-cost: 8 maxlim: 12 bits: 5/4 c ---[ 20]---> Adder-cost: 30 maxlim: 35840 bits: 17/16 c ---[ 18]---> Adder-cost: 50 maxlim: 532 bits: 10/10 c ---[ 16]---> Adder-cost: 50 maxlim: 532 bits: 10/10 c ---[ 14]---> Adder-cost: 50 maxlim: 532 bits: 10/10 c ---[ 12]---> Adder-cost: 50 maxlim: 532 bits: 10/10 c ---[ 11]---> Adder-cost: 40 maxlim: 268799 bits: 20/19 c ---[ 10]---> Adder-cost: 79 maxlim: 454399 bits: 20/19 c ---[ 9]---> Adder-cost: 79 maxlim: 326399 bits: 20/19 c ---[ 8]---> Adder-cost: 80 maxlim: 582399 bits: 21/20 c ---[ 7]---> Adder-cost: 79 maxlim: 454399 bits: 20/19 c ---[ 6]---> Adder-cost: 80 maxlim: 838399 bits: 21/20 c ---[ 5]---> Adder-cost: 0 maxlim: 108542 bits: 18/17 c ---[ 4]---> Adder-cost: 49 maxlim: 116222 bits: 18/17 c ---[ 3]---> Adder-cost: 49 maxlim: 116222 bits: 18/17 c ---[ 2]---> Adder-cost: 49 maxlim: 116222 bits: 18/17 c ---[ 1]---> Adder-cost: 49 maxlim: 116222 bits: 18/17 c ---[ 0]---> Adder-cost: 49 maxlim: 116222 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 5695 20694 | 1898 0 0 nan | 0.000 % | c | 101 | 5688 20671 | 2087 100 528 5.3 | 20.947 % | c | 253 | 5670 20611 | 2296 251 1564 6.2 | 21.162 % | c | 479 | 5596 20343 | 2526 313 1912 6.1 | 21.377 % | c ============================================================================== c [1mFound solution: 2284161[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 494 maxlim: 2949497 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 549 | 8963 32417 | 2987 383 2498 6.5 | 21.377 % | c ============================================================================== c [1mFound solution: 2173113[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 3060545 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 595 | 8990 32600 | 2996 429 2747 6.4 | 21.377 % | c | 695 | 8830 32017 | 3295 467 3787 8.1 | 16.894 % | c ============================================================================== c [1mFound solution: 2154411[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 244 maxlim: 2894927 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 775 | 10512 38066 | 3504 547 4302 7.9 | 16.894 % | c | 875 | 10512 38066 | 3854 647 4941 7.6 | 15.299 % | c ============================================================================== c [1mFound solution: 2038544[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 278 maxlim: 2626794 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1022 | 11426 41419 | 3808 687 5781 8.4 | 15.299 % | c | 1122 | 11426 41419 | 4188 787 6768 8.6 | 17.375 % | c | 1273 | 11426 41419 | 4607 938 8896 9.5 | 17.375 % | c | 1499 | 11275 40876 | 5068 1152 10904 9.5 | 17.664 % | c | 1836 | 11275 40876 | 5575 1489 16435 11.0 | 17.662 % | c ============================================================================== c [1mFound solution: 2019067[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 170 maxlim: 2461951 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2156 | 12430 45010 | 4143 1809 19973 11.0 | 17.662 % | c | 2257 | 12430 45010 | 4557 1910 22006 11.5 | 16.711 % | c ============================================================================== c [1mFound solution: 1969823[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 158 maxlim: 2326875 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2339 | 13305 48172 | 4435 1988 22651 11.4 | 16.711 % | c | 2439 | 13305 48172 | 4878 2088 24598 11.8 | 16.278 % | c ============================================================================== c [1mFound solution: 1936905[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2359793 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2486 | 13318 48289 | 4439 2135 25132 11.8 | 16.278 % | c | 2587 | 13318 48289 | 4882 2236 26403 11.8 | 16.466 % | c | 2738 | 13318 48289 | 5371 2387 27636 11.6 | 16.464 % | c | 2963 | 13318 48289 | 5908 2612 30208 11.6 | 16.464 % | c ============================================================================== c [1mFound solution: 1868543[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2428155 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3048 | 13335 48439 | 4445 2697 31248 11.6 | 16.464 % | c | 3149 | 13335 48439 | 4889 2798 32897 11.8 | 16.696 % | c ============================================================================== c [1mFound solution: 1851387[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2445311 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3238 | 13339 48463 | 4446 2887 33670 11.7 | 16.696 % | c | 3339 | 13339 48463 | 4890 2988 35248 11.8 | 16.757 % | c | 3490 | 13339 48463 | 5379 3139 37357 11.9 | 16.755 % | c | 3715 | 13332 48440 | 5917 3362 42260 12.6 | 16.793 % | c ============================================================================== c [1mFound solution: 1850381[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2446317 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3953 | 13349 48598 | 4449 3600 45406 12.6 | 16.793 % | c | 4053 | 13349 48598 | 4893 3700 46865 12.7 | 17.009 % | c ============================================================================== c [1mFound solution: 1850379[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2446319 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4070 | 13317 48490 | 4439 3701 47089 12.7 | 17.009 % | c ============================================================================== c [1mFound solution: 1850377[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2446321 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4101 | 13319 48512 | 4439 3732 47762 12.8 | 17.009 % | c | 4201 | 13319 48512 | 4882 3832 48689 12.7 | 17.090 % | c ============================================================================== c [1mFound solution: 1850375[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2446323 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4320 | 13320 48532 | 4440 3951 50663 12.8 | 17.090 % | c | 4420 | 13320 48532 | 4884 4051 51451 12.7 | 17.120 % | c | 4570 | 13305 48481 | 5372 4199 54227 12.9 | 17.191 % | c ============================================================================== c [1mFound solution: 1849212[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447486 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4594 | 13318 48631 | 4439 4223 54638 12.9 | 17.191 % | c | 4694 | 13318 48631 | 4882 4323 57165 13.2 | 17.395 % | c | 4847 | 13318 48631 | 5371 4476 59498 13.3 | 17.395 % | c | 5074 | 13318 48631 | 5908 4703 64183 13.6 | 17.395 % | c | 5411 | 13318 48631 | 6499 5040 69989 13.9 | 17.393 % | c | 5918 | 13318 48631 | 7149 5547 81123 14.6 | 17.395 % | c ============================================================================== c [1mFound solution: 1849211[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447487 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6304 | 13320 48648 | 4440 5933 85920 14.5 | 17.395 % | c ============================================================================== c [1mFound solution: 1849149[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447549 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6343 | 13328 48747 | 4442 3006 43602 14.5 | 17.395 % | c ============================================================================== c [1mFound solution: 1849083[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447615 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6359 | 13330 48763 | 4443 3022 43683 14.5 | 17.395 % | c ============================================================================== c [1mFound solution: 1848931[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447767 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6366 | 13335 48819 | 4445 3029 43745 14.4 | 17.395 % | c | 6466 | 13335 48819 | 4889 3129 45782 14.6 | 17.639 % | c ============================================================================== c [1mFound solution: 1848915[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447783 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6472 | 13339 48859 | 4446 3135 45940 14.7 | 17.639 % | c ============================================================================== c [1mFound solution: 1848883[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447815 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6472 | 13342 48895 | 4447 3135 45940 14.7 | 17.639 % | c ============================================================================== c [1mFound solution: 1848851[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447847 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6476 | 13346 48930 | 4448 3139 45952 14.6 | 17.639 % | c ============================================================================== c [1mFound solution: 1848847[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447851 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6476 | 13348 48952 | 4449 3139 45952 14.6 | 17.639 % | c ============================================================================== c [1mFound solution: 1848843[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2447855 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6482 | 13350 48969 | 4450 3145 46016 14.6 | 17.639 % | c ============================================================================== c [1mFound solution: 1847163[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449535 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6512 | 13355 49000 | 4451 3175 46708 14.7 | 17.639 % | c | 6612 | 13355 49000 | 4896 3275 47948 14.6 | 17.879 % | c ============================================================================== c [1mFound solution: 1847103[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449595 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6695 | 13363 49078 | 4454 3358 49824 14.8 | 17.879 % | c | 6796 | 13363 49078 | 4899 3459 51027 14.8 | 17.965 % | c ============================================================================== c [1mFound solution: 1847099[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449599 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6810 | 13365 49096 | 4455 3473 51276 14.8 | 17.965 % | c | 6910 | 13365 49096 | 4900 3573 53087 14.9 | 17.987 % | c ============================================================================== c [1mFound solution: 1847067[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449631 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6914 | 13367 49114 | 4455 3577 53114 14.8 | 17.987 % | c ============================================================================== c [1mFound solution: 1847063[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449635 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6919 | 13368 49134 | 4456 3582 53241 14.9 | 17.987 % | c ============================================================================== c [1mFound solution: 1847051[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449647 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6920 | 13370 49152 | 4456 3583 53244 14.9 | 17.987 % | c ============================================================================== c [1mFound solution: 1847047[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449651 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6925 | 13372 49174 | 4457 3588 53261 14.8 | 17.987 % | c ============================================================================== c [1mFound solution: 1847043[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449655 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6933 | 13374 49193 | 4458 3596 53431 14.9 | 17.987 % | c | 7033 | 13374 49193 | 4903 3696 55614 15.0 | 18.106 % | c | 7183 | 13374 49193 | 5394 3846 57794 15.0 | 18.103 % | c | 7411 | 13374 49193 | 5933 4074 61002 15.0 | 18.104 % | c ============================================================================== c [1mFound solution: 1847041[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449657 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7440 | 13376 49215 | 4458 4103 61561 15.0 | 18.104 % | c ============================================================================== c [1mFound solution: 1847040[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2449658 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7445 | 13378 49239 | 4459 4108 61588 15.0 | 18.104 % | c | 7545 | 13378 49239 | 4904 4208 62937 15.0 | 18.149 % | c | 7695 | 12754 47003 | 5395 1841 20132 10.9 | 19.284 % | c | 7920 | 12754 47003 | 5934 2066 23364 11.3 | 19.284 % | c ============================================================================== c [1mFound solution: 1847035[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 190 maxlim: 2157823 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8238 | 14002 51460 | 4667 2384 29123 12.2 | 19.284 % | c | 8338 | 14002 51460 | 5133 2484 30581 12.3 | 18.387 % | c | 8488 | 13993 51429 | 5647 2630 32639 12.4 | 18.419 % | c | 8715 | 13993 51429 | 6211 2857 34904 12.2 | 18.419 % | c ============================================================================== c [1mFound solution: 1846589[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2158269 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8731 | 14005 51548 | 4668 2873 35225 12.3 | 18.419 % | c | 8831 | 14005 51548 | 5134 2973 36651 12.3 | 18.577 % | c ============================================================================== c [1mFound solution: 1846334[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2158524 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8869 | 14017 51672 | 4672 3011 37040 12.3 | 18.577 % | c | 8971 | 14017 51672 | 5139 3113 40287 12.9 | 18.730 % | c | 9121 | 14017 51672 | 5653 3263 42789 13.1 | 18.727 % | c ============================================================================== c [1mFound solution: 1846237[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2158621 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9167 | 14028 51766 | 4676 3309 43401 13.1 | 18.727 % | c ============================================================================== c [1mFound solution: 1845569[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2159289 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9197 | 14039 51863 | 4679 3339 43758 13.1 | 18.727 % | c ============================================================================== c [1mFound solution: 1844667[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2160191 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9292 | 14043 51903 | 4681 3434 45852 13.4 | 18.727 % | c | 9392 | 14043 51903 | 5149 3534 47223 13.4 | 19.028 % | c | 9542 | 14043 51903 | 5664 3684 51956 14.1 | 19.028 % | c | 9767 | 14043 51903 | 6230 3909 53640 13.7 | 19.028 % | c | 10104 | 14043 51903 | 6853 4246 57002 13.4 | 19.028 % | c | 10610 | 14043 51903 | 7538 4752 66299 14.0 | 19.028 % | c | 11369 | 14043 51903 | 8292 5511 79083 14.4 | 19.028 % | c | 12508 | 14043 51903 | 9121 6650 102636 15.4 | 19.028 % | c ============================================================================== c [1mFound solution: 1844255[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2160603 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13165 | 14055 52006 | 4685 7307 114710 15.7 | 19.028 % | c | 13266 | 14055 52006 | 5153 3755 58386 15.5 | 19.149 % | c ============================================================================== c [1mFound solution: 1844235[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2160623 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13307 | 14059 52038 | 4686 3796 58757 15.5 | 19.149 % | c | 13408 | 14059 52038 | 5154 3897 59948 15.4 | 19.185 % | c | 13558 | 14059 52038 | 5670 4047 62046 15.3 | 19.185 % | c ============================================================================== c [1mFound solution: 1844219[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2160639 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13710 | 14060 52048 | 4686 4199 65067 15.5 | 19.185 % | c | 13812 | 14060 52048 | 5154 4301 66677 15.5 | 19.214 % | c ============================================================================== c [1mFound solution: 1843915[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2160943 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13892 | 14064 52096 | 4688 4381 67786 15.5 | 19.214 % | c | 13992 | 14064 52096 | 5156 4481 68818 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843851[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161007 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14066 | 14068 52143 | 4689 4555 70002 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843723[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161135 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14085 | 14076 52207 | 4692 4574 70403 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843531[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161327 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14129 | 14083 52264 | 4694 4618 70821 15.3 | 19.281 % | c ============================================================================== c [1mFound solution: 1843515[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161343 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14154 | 14085 52281 | 4695 4643 71347 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843467[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161391 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14172 | 14089 52315 | 4696 4661 71514 15.3 | 19.281 % | c ============================================================================== c [1mFound solution: 1843459[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161399 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14186 | 14082 52302 | 4694 3936 60542 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843451[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161407 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14192 | 14083 52315 | 4694 3942 60560 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843323[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161535 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14206 | 14084 52328 | 4694 3956 61075 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843259[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161599 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14284 | 14083 52334 | 4694 3975 61145 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843227[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161631 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14293 | 14084 52346 | 4694 3984 61418 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843207[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161651 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14300 | 14087 52374 | 4695 3991 61464 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843203[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161655 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14300 | 14089 52391 | 4696 3991 61464 15.4 | 19.281 % | c ============================================================================== c [1mFound solution: 1843200[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 2161658 bits: 22/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14323 | 14093 52428 | 4697 4014 61682 15.4 | 19.281 % | 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 : 112 c conflicts : 14356 (2371 /sec) c decisions : 38045 (6283 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 6.05508 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.91 0.95 0.91 2/55 20708 Raw data (stat): 20708 (runsolver) R 20707 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542606501 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+6.10875 s] Raw data (loadavg): 0.93 0.95 0.91 1/54 20708 Raw data (stat): 20708 (runsolver) R 20707 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542606501 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: 0 Child status: 30 Real time (s): 6.10818 CPU time (s): 6.09407 CPU user time (s): 6.05908 CPU system time (s): 0.034994 CPU usage (%): 99.7691 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1843200 #### END VERIFIER DATA ####