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 wulflinc19 THE 2005-04-20 21:56:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=20395 boxname=wulflinc19 idbench=1569 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 25b0f49e8e3ab43f9f405cabc9317ea8 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-nazareth.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-nazareth.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-nazareth.opb IDLAUNCH: 20395 /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: 781944 kB Buffers: 34264 kB Cached: 184920 kB SwapCached: 660 kB Active: 89120 kB Inactive: 132204 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 781692 kB SwapTotal: 2097892 kB SwapFree: 2096432 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5200 kB Slab: 25652 kB Committed_AS: 63816 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 21:56:05 (client local time) WITH STATUS 30 IN 0.989849 SECONDS stats: 20395 0 0.989849 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]---> Sorter-cost: 439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 1303 3161 | 390 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 547/547 c -- var.elim.: 280/280 c -- subsuming c -- var.elim.: 255/255 c -- var.elim.: 140/140 c -- subsuming c | 0 | 996 3172 | -- 0 -- -- | -- | -307/16 c | 0 | 996 3172 | 398 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.087986 s) c ============================================================================== c [1mFound solution: -196602[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 390 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 14 | 1865 5199 | 559 14 41 2.9 | 0.000 % | c -- subsuming c -- var.elim.: 392/392 c -- var.elim.: 204/204 c -- subsuming c -- var.elim.: 135/135 c -- var.elim.: 31/31 c | 14 | 1667 5398 | -- 14 -- -- | -- | -177/252 c | 14 | 1667 5398 | 666 13 39 3.0 | 0.000 % | c ============================================================================== c (current CPU-time: 0.142978 s) c ============================================================================== c [1mFound solution: -527576[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 48 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 15 | 1873 5908 | 561 14 44 3.1 | 0.000 % | c -- subsuming c -- var.elim.: 297/297 c -- var.elim.: 165/165 c -- var.elim.: 13/13 c -- var.elim.: 6/6 c -- subsuming c -- var.elim.: 36/36 c -- var.elim.: 18/18 c | 15 | 1678 5525 | -- 14 -- -- | -- | -160/-214 c | 15 | 1678 5525 | 671 14 44 3.1 | 0.000 % | c ============================================================================== c (current CPU-time: 0.177972 s) c ============================================================================== c [1mFound solution: -649145[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 17 | 1785 5788 | 535 16 54 3.4 | 0.000 % | c -- subsuming c -- var.elim.: 149/149 c -- var.elim.: 87/87 c | 17 | 1710 5616 | -- 16 -- -- | -- | -75/-171 c | 17 | 1710 5616 | 684 16 54 3.4 | 0.000 % | c ============================================================================== c (current CPU-time: 0.204968 s) c ============================================================================== c [1mFound solution: -719357[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 20 | 1812 5866 | 543 19 64 3.4 | 0.000 % | c -- subsuming c -- var.elim.: 152/152 c -- var.elim.: 85/85 c | 20 | 1752 5795 | -- 19 -- -- | -- | -60/-70 c | 20 | 1752 5795 | 700 19 64 3.4 | 0.000 % | c ============================================================================== c (current CPU-time: 0.234964 s) c ============================================================================== c [1mFound solution: -792461[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 44 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 22 | 1860 6062 | 557 21 73 3.5 | 0.000 % | c -- subsuming c -- var.elim.: 167/167 c -- var.elim.: 99/99 c -- var.elim.: 32/32 c -- var.elim.: 22/22 c | 22 | 1743 5903 | -- 21 -- -- | -- | -77/-8 c | 22 | 1743 5903 | 697 18 55 3.1 | 0.000 % | c ============================================================================== c (current CPU-time: 0.271958 s) c ============================================================================== c [1mFound solution: -889849[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 26 | 1815 6082 | 544 22 65 3.0 | 0.000 % | c -- subsuming c -- var.elim.: 113/113 c -- var.elim.: 154/154 c -- var.elim.: 98/98 c -- var.elim.: 95/95 c | 26 | 1725 6098 | -- 22 -- -- | -- | -90/17 c | 26 | 1725 6098 | 690 20 60 3.0 | 0.000 % | c ============================================================================== c (current CPU-time: 0.315951 s) c ============================================================================== c [1mFound solution: -899405[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 27 | 1795 6279 | 538 21 63 3.0 | 0.000 % | c -- subsuming c -- var.elim.: 199/199 c -- var.elim.: 66/66 c | 27 | 1736 6111 | -- 21 -- -- | -- | -59/-167 c | 27 | 1736 6111 | 694 21 63 3.0 | 0.000 % | c ============================================================================== c (current CPU-time: 0.353946 s) c ============================================================================== c [1mFound solution: -943176[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 43 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 31 | 1819 6325 | 545 25 71 2.8 | 0.000 % | c -- subsuming c -- var.elim.: 194/194 c -- var.elim.: 82/82 c -- var.elim.: 57/57 c -- var.elim.: 42/42 c -- var.elim.: 5/5 c -- var.elim.: 5/5 c -- var.elim.: 8/8 c -- var.elim.: 5/5 c -- var.elim.: 5/5 c -- var.elim.: 8/8 c -- var.elim.: 5/5 c -- var.elim.: 5/5 c -- var.elim.: 8/8 c -- var.elim.: 5/5 c -- var.elim.: 5/5 c -- var.elim.: 8/8 c -- var.elim.: 5/5 c -- var.elim.: 5/5 c -- var.elim.: 8/8 c -- var.elim.: 5/5 c -- var.elim.: 5/5 c -- var.elim.: 9/9 c -- var.elim.: 8/8 c -- var.elim.: 5/5 c -- var.elim.: 7/7 c -- var.elim.: 8/8 c -- var.elim.: 5/5 c -- var.elim.: 7/7 c -- var.elim.: 7/7 c -- var.elim.: 6/6 c -- var.elim.: 7/7 c | 31 | 1190 4176 | -- 25 -- -- | -- | -549/-1513 c | 31 | 1190 4176 | 476 3 11 3.7 | 0.000 % | c ============================================================================== c (current CPU-time: 0.404938 s) c ============================================================================== c [1mFound solution: -960489[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 31 | 1257 4348 | 377 3 11 3.7 | 0.000 % | c -- subsuming c -- var.elim.: 106/106 c -- var.elim.: 66/66 c | 31 | 1216 4302 | -- 3 -- -- | -- | -41/-45 c | 31 | 1216 4302 | 486 3 11 3.7 | 0.000 % | c ============================================================================== c (current CPU-time: 0.442932 s) c ============================================================================== c [1mFound solution: -1028973[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 62 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 32 | 1304 4519 | 391 4 16 4.0 | 0.000 % | c -- subsuming c -- var.elim.: 115/115 c -- var.elim.: 66/66 c -- var.elim.: 39/39 c -- var.elim.: 54/54 c -- var.elim.: 56/56 c -- var.elim.: 39/39 c -- var.elim.: 122/122 c -- var.elim.: 42/42 c -- var.elim.: 8/8 c | 32 | 963 3062 | -- 4 -- -- | -- | -299/-1276 c | 32 | 963 3062 | 385 4 16 4.0 | 0.000 % | c ============================================================================== c (current CPU-time: 0.497924 s) c ============================================================================== c [1mFound solution: -1045865[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 35 | 1011 3178 | 303 7 27 3.9 | 0.000 % | c -- subsuming c -- var.elim.: 93/93 c -- var.elim.: 66/66 c -- var.elim.: 28/28 c -- var.elim.: 46/46 c -- var.elim.: 42/42 c -- var.elim.: 54/54 c -- var.elim.: 39/39 c -- var.elim.: 21/21 c -- subsuming c -- var.elim.: 5/5 c -- var.elim.: 5/5 c | 35 | 764 2431 | -- 7 -- -- | -- | -170/-486 c | 35 | 764 2431 | 305 3 7 2.3 | 0.000 % | c ============================================================================== c (current CPU-time: 0.541917 s) c ============================================================================== c [1mFound solution: -1045885[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 35 | 875 2689 | 262 3 7 2.3 | 0.000 % | c -- subsuming c -- var.elim.: 131/131 c -- var.elim.: 70/70 c -- var.elim.: 1/1 c | 35 | 812 2628 | -- 3 -- -- | -- | -63/-60 c | 35 | 812 2628 | 324 3 7 2.3 | 0.000 % | c ============================================================================== c (current CPU-time: 0.580911 s) c ============================================================================== c [1mFound solution: -1045889[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 100 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 37 | 1043 3273 | 312 5 18 3.6 | 0.000 % | c -- subsuming c -- var.elim.: 140/140 c -- var.elim.: 75/75 c | 37 | 1012 3276 | -- 5 -- -- | -- | -31/6 c | 37 | 1012 3276 | 404 5 18 3.6 | 0.000 % | c ============================================================================== c (current CPU-time: 0.615906 s) c ============================================================================== c [1mFound solution: -1046789[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 90 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38 | 1227 3889 | 368 6 21 3.5 | 0.000 % | c -- subsuming c -- var.elim.: 135/135 c -- var.elim.: 91/91 c -- var.elim.: 35/35 c | 38 | 1146 3956 | -- 6 -- -- | -- | -47/175 c | 38 | 1146 3956 | 458 6 21 3.5 | 0.000 % | c ============================================================================== c (current CPU-time: 0.657899 s) c ============================================================================== c [1mFound solution: -1046811[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 99 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 42 | 1380 4620 | 413 10 33 3.3 | 0.000 % | c -- subsuming c -- var.elim.: 138/138 c -- var.elim.: 77/77 c | 42 | 1347 4695 | -- 10 -- -- | -- | -33/78 c | 42 | 1347 4695 | 538 10 33 3.3 | 0.000 % | c ============================================================================== c (current CPU-time: 0.698893 s) c ============================================================================== c [1mFound solution: -1046901[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 66 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 42 | 1514 5167 | 454 10 33 3.3 | 0.000 % | c -- subsuming c -- var.elim.: 119/119 c -- var.elim.: 59/59 c | 42 | 1485 5136 | -- 10 -- -- | -- | -29/-28 c | 42 | 1485 5136 | 594 10 33 3.3 | 0.000 % | c ============================================================================== c (current CPU-time: 0.736887 s) c ============================================================================== c [1mFound solution: -1046907[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 54 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 42 | 1619 5513 | 485 10 33 3.3 | 0.000 % | c -- subsuming c -- var.elim.: 81/81 c -- var.elim.: 41/41 c | 42 | 1603 5512 | -- 10 -- -- | -- | -16/2 c | 42 | 1603 5512 | 641 10 33 3.3 | 0.000 % | c ============================================================================== c (current CPU-time: 0.772882 s) c ============================================================================== c [1mFound solution: -1047163[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 16 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 44 | 1652 5649 | 495 12 45 3.8 | 0.000 % | c -- subsuming c -- var.elim.: 42/42 c -- var.elim.: 21/21 c | 44 | 1643 5642 | -- 12 -- -- | -- | -9/-4 c | 44 | 1643 5642 | 657 12 45 3.8 | 0.000 % | c ============================================================================== c (current CPU-time: 0.807877 s) c ============================================================================== c [1mFound solution: -1047493[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 40 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 64 | 1754 5954 | 526 32 124 3.9 | 0.000 % | c -- subsuming c -- var.elim.: 86/86 c -- var.elim.: 36/36 c | 64 | 1731 5929 | -- 32 -- -- | -- | -23/-22 c | 64 | 1731 5929 | 692 32 124 3.9 | 0.000 % | c ============================================================================== c (current CPU-time: 0.843871 s) c ============================================================================== c [1mFound solution: -1048517[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 | 64 | 1731 5929 | 519 32 124 3.9 | 0.000 % | c -- subsuming c -- var.elim.: 173/173 c -- var.elim.: 126/126 c -- var.elim.: 113/113 c -- var.elim.: 48/48 c -- var.elim.: 33/33 c -- var.elim.: 25/25 c -- var.elim.: 21/21 c -- var.elim.: 23/23 c -- var.elim.: 15/15 c -- var.elim.: 12/12 c -- var.elim.: 8/8 c -- var.elim.: 6/6 c -- subsuming c -- var.elim.: 3/3 c | 64 | 159 505 | -- 32 -- -- | -- | -761/-2299 c | 64 | 159 505 | 63 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.894863 s) 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 : 21 c conflicts : 64 (69 /sec) c decisions : 1799 (1935 /sec) c propagations : 9356 (10062 /sec) c inspects : 31037 (33378 /sec) c CPU time : 0.929858 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.84 0.94 0.90 2/55 14615 Raw data (stat): 14615 (runsolver) R 14614 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539841055 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+1.0011 s] Raw data (loadavg): 0.84 0.94 0.90 1/54 14615 Raw data (stat): 14615 (runsolver) R 14614 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539841055 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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): 1.00088 CPU time (s): 0.989849 CPU user time (s): 0.931858 CPU system time (s): 0.057991 CPU usage (%): 98.8981 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK -1048575 #### END VERIFIER DATA ####