Name | normalized-opb/mps-v2-13-7/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-nazareth.opb |
MD5SUM | 25b0f49e8e3ab43f9f405cabc9317ea8 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -1048575 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 55 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 3162109 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 5244800 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 19924855 |
Number of bits of the biggest sum of numbers | 25 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.008998 |
Number of variables | 55 |
Total number of constraints | 3 |
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 | 3 |
Minimum length of a constraint | 14 |
Maximum length of a constraint | 41 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-05-27 10:40:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23925 boxname=wulflinc21 idbench=1569 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 25b0f49e8e3ab43f9f405cabc9317ea8 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-nazareth.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-nazareth.opb IDLAUNCH: 23925 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 824828 kB Buffers: 14280 kB Cached: 174808 kB SwapCached: 972 kB Active: 17708 kB Inactive: 173492 kB HighTotal: 131008 kB HighFree: 9912 kB LowTotal: 903652 kB LowFree: 814916 kB SwapTotal: 2097892 kB SwapFree: 2096008 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5128 kB Slab: 12836 kB Committed_AS: 63916 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 10:40:45 (client local time) WITH STATUS 30 IN 0.243961 SECONDS stats: 23925 0 0.243961 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 3 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 2]---> BDD-cost: 13 c ---[ 1]---> BDD-cost: 157 c ---[ 0]---> BDD-cost: 377 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1014 2798 | 338 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -2067[0m c ---[ 0]---> Sorter-cost: 389 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1856 4772 | 618 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -753667[0m c ---[ 0]---> Sorter-cost: 45 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1881 4846 | 627 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -1013735[0m c ---[ 0]---> Sorter-cost: 44 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2 | 1807 4655 | 602 2 7 3.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1013743[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2 | 1823 4690 | 607 2 7 3.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1032174[0m c ---[ 0]---> Sorter-cost: 66 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4 | 1831 4695 | 610 2 6 3.0 | 0.000 % | c ============================================================================== c [1mFound solution: -1032182[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5 | 1850 4736 | 616 3 11 3.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1032185[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12 | 1862 4761 | 620 10 30 3.0 | 0.000 % | c ============================================================================== c [1mFound solution: -1033848[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15 | 1810 4630 | 603 12 38 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1042173[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16 | 1733 4434 | 577 13 41 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1043068[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 1749 4471 | 583 14 45 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1043191[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 1763 4503 | 587 14 45 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1043197[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 1770 4519 | 590 14 45 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1043321[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 1783 4548 | 594 14 45 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1043323[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 1798 4582 | 599 14 45 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1043325[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 1812 4613 | 604 14 45 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1043832[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19 | 1821 4634 | 607 16 60 3.8 | 0.000 % | c ============================================================================== c [1mFound solution: -1045276[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20 | 1696 4327 | 565 15 57 3.8 | 0.000 % | c ============================================================================== c [1mFound solution: -1045369[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24 | 1654 4234 | 551 16 65 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1045373[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24 | 1657 4241 | 552 16 65 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1045399[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 1668 4267 | 556 17 71 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1045402[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 1681 4298 | 560 17 71 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1045433[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 1693 4325 | 564 17 71 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1045436[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 1704 4350 | 568 17 71 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1045463[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 1714 4373 | 571 17 71 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1045464[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 1726 4400 | 575 17 71 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1045465[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 1738 4427 | 579 17 71 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1047453[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26 | 1687 4293 | 562 18 75 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1047513[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27 | 1690 4300 | 563 19 82 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1047517[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27 | 1698 4318 | 566 19 82 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1047529[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28 | 1707 4338 | 569 20 88 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1047531[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28 | 1718 4362 | 572 20 88 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1047532[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29 | 1729 4386 | 576 21 93 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1047801[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30 | 1627 4136 | 542 22 95 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1047932[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30 | 1632 4148 | 544 22 95 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1047997[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30 | 1640 4166 | 546 22 95 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048317[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33 | 1538 3911 | 512 19 79 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1048445[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34 | 1443 3675 | 481 17 72 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1048508[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35 | 1350 3443 | 450 17 73 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048509[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35 | 1353 3450 | 451 17 73 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048534[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36 | 1262 3224 | 420 17 74 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1048536[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36 | 1265 3231 | 421 17 74 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1048537[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36 | 1268 3238 | 422 17 74 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1048538[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36 | 1271 3245 | 423 17 74 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1048541[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36 | 1274 3252 | 424 17 74 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1048554[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37 | 1183 3028 | 394 16 66 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1048555[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38 | 1186 3035 | 395 17 68 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: -1048556[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38 | 1189 3042 | 396 17 68 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: -1048557[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38 | 1194 3053 | 398 17 68 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: -1048559[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39 | 1080 2763 | 360 18 71 3.9 | 0.000 % | c ============================================================================== c [1mFound solution: -1048564[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41 | 1032 2656 | 344 9 30 3.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048565[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41 | 1035 2663 | 345 9 30 3.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048573[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41 | 786 2049 | 262 5 16 3.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1048575[0m c [1mOptimal solution: -1048575[0m s OPTIMUM FOUND v -CLNAM1_bit_7 -CLNAM1_bit_6 -CLNAM1_bit_5 -CLNAM1_bit_4 -CLNAM1_bit_3 -CLNAM1_bit_2 -CLNAM1_bit_1 -CLNAM1_bit0 -CLNAM1_bit1 -CLNAM1_bit2 -CLNAM1_bit3 -CLNAM1_bit4 -CLNAM1_bit5 -CLNAM1_bit6 CLNAM2_bit_7 CLNAM2_bit_6 CLNAM2_bit_5 CLNAM2_bit_4 CLNAM2_bit_3 CLNAM2_bit_2 CLNAM2_bit_1 CLNAM2_bit0 CLNAM2_bit1 CLNAM2_bit2 CLNAM2_bit3 CLNAM2_bit4 CLNAM2_bit5 CLNAM2_bit6 CLNAM2_bit7 CLNAM2_bit8 CLNAM2_bit9 CLNAM2_bit10 CLNAM2_bit11 CLNAM2_bit12 -CLNAM3_bit_7 -CLNAM3_bit_6 -CLNAM3_bit_5 -CLNAM3_bit_4 -CLNAM3_bit_3 -CLNAM3_bit_2 -CLNAM3_bit_1 -CLNAM3_bit0 -CLNAM3_bit1 -CLNAM3_bit2 -CLNAM3_bit3 -CLNAM3_bit4 -CLNAM3_bit5 -CLNAM3_bit6 -CLNAM3_bit7 -CLNAM3_bit8 -CLNAM3_bit9 -CLNAM3_bit10 -CLNAM3_bit11 -CLNAM3_bit12 -CLNAM3_bit13 c _______________________________________________________________________________ c c restarts : 53 c conflicts : 41 (187 /sec) c decisions : 14412 (65818 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 0.218966 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.90 2/55 29392 Raw data (stat): 29392 (runsolver) R 29391 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 732781874 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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+0.256776 s] Raw data (loadavg): 0.91 0.95 0.90 1/54 29396 Raw data (stat): 29392 (runsolver) R 29391 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 732781874 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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): 0.256474 CPU time (s): 0.243961 CPU user time (s): 0.223965 CPU system time (s): 0.019996 CPU usage (%): 95.1211 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK -1048575 #### END VERIFIER DATA ####