Name | normalized-opb/mps-v2-13-7/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-maros.opb |
MD5SUM | 1ae5b04b2d0e1f5ab82e29e98b8350c0 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 43097 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 64 |
Biggest coefficient in the objective function | 4718592 |
Number of bits for the biggest coefficient in the objective function | 23 |
Sum of the numbers in the objective function | 14745570 |
Number of bits of the sum of numbers in the objective function | 24 |
Biggest number in a constraint | 4718592 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 14745570 |
Number of bits of the biggest sum of numbers | 24 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02384 |
Number of variables | 64 |
Total number of constraints | 6 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 12 |
Maximum length of a constraint | 64 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-04-20 21:56:19 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=20382 boxname=wulflinc19 idbench=1568 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1ae5b04b2d0e1f5ab82e29e98b8350c0 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-maros.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-maros.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-maros.opb IDLAUNCH: 20382 /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: 781952 kB Buffers: 34288 kB Cached: 184964 kB SwapCached: 660 kB Active: 89140 kB Inactive: 132220 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 781700 kB SwapTotal: 2097892 kB SwapFree: 2096432 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5200 kB Slab: 25628 kB Committed_AS: 63820 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 21:56:44 (client local time) WITH STATUS 30 IN 24.8152 SECONDS stats: 20382 0 24.8152 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 6 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): s c ---[ 5]---> BDD-cost: 11 c ---[ 3]---> Sorter-cost: 961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 410 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 1]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> BDD-cost: 8 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 4458 10461 | 1337 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/1600 c -- var.elim.: 1600/1600 c -- var.elim.: 834/834 c -- var.elim.: 11/11 c -- subsuming c -- var.elim.: 320/320 c -- var.elim.: 225/225 c -- subsuming c -- var.elim.: 53/53 c -- var.elim.: 22/22 c | 0 | 3721 11304 | -- 0 -- -- | -- | -734/856 c | 0 | 3721 11304 | 1488 0 0 nan | 0.000 % | c | 100 | 3721 11304 | 1637 100 1347 13.5 | 2.792 % | c ============================================================================== c (current CPU-time: 0.287956 s) c ============================================================================== c [1mFound solution: 48352[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 989 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 | 140 | 6029 16699 | 1808 140 1632 11.7 | 2.792 % | c -- subsuming c -- var.elim.: 907/907 c -- var.elim.: 481/481 c -- var.elim.: 4/4 c -- var.elim.: 5/5 c -- subsuming c -- var.elim.: 152/152 c -- var.elim.: 79/79 c | 140 | 5624 17306 | -- 140 -- -- | -- | -405/608 c | 140 | 5624 17306 | 2249 140 1632 11.7 | 2.792 % | c | 240 | 5624 17306 | 2474 240 3624 15.1 | 1.936 % | c | 391 | 5624 17306 | 2722 391 6618 16.9 | 1.936 % | c | 617 | 5624 17306 | 2994 617 11028 17.9 | 1.936 % | c | 954 | 5624 17306 | 3293 954 19301 20.2 | 1.936 % | c ============================================================================== c (current CPU-time: 0.840872 s) c ============================================================================== c [1mFound solution: 47488[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 1438 | 5767 17717 | 1730 1438 32197 22.4 | 1.936 % | c -- subsuming c -- var.elim.: 315/315 c -- var.elim.: 158/158 c | 1438 | 5665 17604 | -- 1438 -- -- | -- | -102/-112 c | 1438 | 5665 17604 | 2266 1438 32197 22.4 | 1.936 % | c | 1538 | 5665 17604 | 2492 1538 34254 22.3 | 2.005 % | c | 1688 | 5665 17604 | 2741 1688 37198 22.0 | 2.005 % | c ============================================================================== c (current CPU-time: 1.05684 s) c ============================================================================== c [1mFound solution: 44550[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 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 | 1818 | 5737 17812 | 1721 1818 41196 22.7 | 2.005 % | c -- subsuming c -- var.elim.: 166/166 c -- var.elim.: 92/92 c | 1818 | 5699 17900 | -- 1818 -- -- | -- | -38/89 c | 1818 | 5699 17900 | 2279 1818 41196 22.7 | 2.005 % | c | 1919 | 5699 17900 | 2507 1919 43246 22.5 | 2.075 % | c | 2074 | 5699 17900 | 2758 2074 47736 23.0 | 2.075 % | c | 2300 | 5699 17900 | 3034 2300 54335 23.6 | 2.076 % | c ============================================================================== c (current CPU-time: 1.45778 s) c ============================================================================== c [1mFound solution: 44549[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2599 | 5754 18071 | 1726 2599 61794 23.8 | 2.076 % | c -- subsuming c -- var.elim.: 126/126 c -- var.elim.: 79/79 c | 2599 | 5718 18127 | -- 2599 -- -- | -- | -36/57 c | 2599 | 5718 18127 | 2287 2599 61794 23.8 | 2.076 % | c | 2701 | 5718 18127 | 2515 1835 40818 22.2 | 2.150 % | c | 2851 | 5718 18127 | 2767 1985 45065 22.7 | 2.150 % | c | 3076 | 5718 18127 | 3044 2210 50312 22.8 | 2.150 % | c | 3413 | 5718 18127 | 3348 2547 57526 22.6 | 2.150 % | c ============================================================================== c (current CPU-time: 1.89671 s) c ============================================================================== c [1mFound solution: 44457[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3563 | 5748 18199 | 1724 2119 46969 22.2 | 2.150 % | c -- subsuming c -- var.elim.: 142/142 c -- var.elim.: 123/123 c | 3563 | 5705 18281 | -- 2119 -- -- | -- | -43/83 c | 3563 | 5705 18281 | 2282 1290 18238 14.1 | 2.150 % | c ============================================================================== c (current CPU-time: 1.9887 s) c ============================================================================== c [1mFound solution: 44368[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 3652 | 5752 18437 | 1725 1379 19998 14.5 | 2.150 % | c -- subsuming c -- var.elim.: 112/112 c -- var.elim.: 77/77 c | 3652 | 5720 18478 | -- 1379 -- -- | -- | -32/42 c | 3652 | 5720 18478 | 2288 1379 19998 14.5 | 2.150 % | c | 3758 | 5720 18478 | 2516 1485 22396 15.1 | 2.623 % | c ============================================================================== c (current CPU-time: 2.13167 s) c ============================================================================== c [1mFound solution: 43999[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3903 | 5761 18623 | 1728 1630 28342 17.4 | 2.623 % | c -- subsuming c -- var.elim.: 103/103 c -- var.elim.: 75/75 c | 3903 | 5733 18702 | -- 1630 -- -- | -- | -28/80 c | 3903 | 5733 18702 | 2293 1630 28342 17.4 | 2.623 % | c | 4003 | 5733 18702 | 2522 1730 31933 18.5 | 2.696 % | c | 4153 | 5733 18702 | 2774 1880 38040 20.2 | 2.696 % | c | 4378 | 5733 18702 | 3052 2105 44917 21.3 | 2.696 % | c | 4715 | 5733 18702 | 3357 2442 53422 21.9 | 2.696 % | c ============================================================================== c (current CPU-time: 2.54961 s) c ============================================================================== c [1mFound solution: 43810[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 4845 | 5790 18882 | 1736 2572 57905 22.5 | 2.696 % | c -- subsuming c -- var.elim.: 119/119 c -- var.elim.: 82/82 c | 4845 | 5755 19009 | -- 2572 -- -- | -- | -35/128 c | 4845 | 5755 19009 | 2302 2572 57905 22.5 | 2.696 % | c | 4945 | 5755 19009 | 2532 1815 42135 23.2 | 2.767 % | c | 5095 | 5755 19009 | 2785 1965 47273 24.1 | 2.767 % | c | 5321 | 5755 19009 | 3063 2191 54289 24.8 | 2.767 % | c | 5658 | 5755 19009 | 3370 2528 68409 27.1 | 2.767 % | c | 6164 | 5755 19009 | 3707 3034 85795 28.3 | 2.767 % | c | 6926 | 5755 19009 | 4078 3796 112086 29.5 | 2.767 % | c | 8067 | 5755 19009 | 4485 3538 105128 29.7 | 2.767 % | c ============================================================================== c (current CPU-time: 4.6093 s) c ============================================================================== c [1mFound solution: 43809[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 8991 | 5809 19181 | 1742 4462 137429 30.8 | 2.767 % | c -- subsuming c -- var.elim.: 118/118 c -- var.elim.: 80/80 c | 8991 | 5770 19154 | -- 4462 -- -- | -- | -39/-26 c | 8991 | 5770 19154 | 2308 4462 137429 30.8 | 2.767 % | c | 9091 | 5770 19154 | 2538 2084 46241 22.2 | 2.837 % | c | 9246 | 5770 19154 | 2792 2239 49738 22.2 | 2.838 % | c | 9474 | 5770 19154 | 3071 2467 55902 22.7 | 2.837 % | c | 9813 | 5770 19154 | 3379 2806 66968 23.9 | 2.837 % | c | 10320 | 5770 19154 | 3717 3313 87049 26.3 | 2.837 % | c ============================================================================== c (current CPU-time: 5.49116 s) c ============================================================================== c [1mFound solution: 43806[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 10783 | 5829 19337 | 1748 3776 99954 26.5 | 2.837 % | c -- subsuming c -- var.elim.: 121/121 c -- var.elim.: 82/82 c | 10783 | 5792 19444 | -- 3776 -- -- | -- | -37/108 c | 10783 | 5792 19444 | 2316 3776 99954 26.5 | 2.837 % | c | 10883 | 5792 19444 | 2548 1779 33715 19.0 | 2.907 % | c | 11038 | 5792 19444 | 2803 1934 38864 20.1 | 2.907 % | c | 11265 | 5792 19444 | 3083 2161 46560 21.5 | 2.907 % | c | 11603 | 5792 19444 | 3392 2499 60955 24.4 | 2.907 % | c | 12109 | 5792 19444 | 3731 3005 77632 25.8 | 2.907 % | c ============================================================================== c (current CPU-time: 6.20106 s) c ============================================================================== c [1mFound solution: 43765[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 12120 | 5849 19619 | 1754 3016 78177 25.9 | 2.907 % | c -- subsuming c -- var.elim.: 118/118 c -- var.elim.: 80/80 c | 12120 | 5810 19574 | -- 3016 -- -- | -- | -39/-44 c | 12120 | 5810 19574 | 2324 3016 78177 25.9 | 2.907 % | c | 12221 | 5810 19574 | 2556 2112 50555 23.9 | 2.980 % | c | 12371 | 5810 19574 | 2812 2262 57269 25.3 | 2.976 % | c | 12598 | 5810 19574 | 3093 2489 65878 26.5 | 2.976 % | c | 12935 | 5810 19574 | 3402 2826 77887 27.6 | 2.976 % | c ============================================================================== c (current CPU-time: 6.70598 s) c ============================================================================== c [1mFound solution: 43753[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 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 | 13057 | 5850 19699 | 1754 2948 80603 27.3 | 2.976 % | c -- subsuming c -- var.elim.: 93/93 c -- var.elim.: 59/59 c | 13057 | 5825 19721 | -- 2948 -- -- | -- | -25/23 c | 13057 | 5825 19721 | 2330 2948 80603 27.3 | 2.976 % | c ============================================================================== c (current CPU-time: 6.79197 s) c ============================================================================== c [1mFound solution: 43657[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 13078 | 5884 19901 | 1765 1987 44356 22.3 | 2.976 % | c -- subsuming c -- var.elim.: 118/118 c -- var.elim.: 79/79 c | 13078 | 5845 20017 | -- 1987 -- -- | -- | -39/117 c | 13078 | 5845 20017 | 2338 1987 44356 22.3 | 2.976 % | c | 13179 | 5845 20017 | 2571 2088 48841 23.4 | 3.115 % | c | 13329 | 5845 20017 | 2828 2238 53543 23.9 | 3.116 % | c | 13555 | 5845 20017 | 3111 2464 59686 24.2 | 3.116 % | c ============================================================================== c (current CPU-time: 7.07792 s) c ============================================================================== c [1mFound solution: 43619[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 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 | 13575 | 5883 20132 | 1764 2484 60317 24.3 | 3.116 % | c -- subsuming c -- var.elim.: 88/88 c -- var.elim.: 52/52 c | 13575 | 5858 20143 | -- 2484 -- -- | -- | -25/12 c | 13575 | 5858 20143 | 2343 2484 60317 24.3 | 3.116 % | c | 13678 | 5858 20143 | 2577 1759 33978 19.3 | 3.186 % | c ============================================================================== c (current CPU-time: 7.2299 s) c ============================================================================== c [1mFound solution: 43602[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 13768 | 5918 20328 | 1775 1849 36788 19.9 | 3.186 % | c -- subsuming c -- var.elim.: 121/121 c -- var.elim.: 81/81 c | 13768 | 5880 20519 | -- 1849 -- -- | -- | -38/192 c | 13768 | 5880 20519 | 2352 1849 36788 19.9 | 3.186 % | c ============================================================================== c (current CPU-time: 7.29289 s) c ============================================================================== c [1mFound solution: 43561[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 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 | 13773 | 5921 20646 | 1776 1854 36860 19.9 | 3.186 % | c -- subsuming c -- var.elim.: 104/104 c -- var.elim.: 59/59 c | 13773 | 5891 20565 | -- 1854 -- -- | -- | -30/-80 c | 13773 | 5891 20565 | 2356 1854 36860 19.9 | 3.186 % | c | 13874 | 5891 20565 | 2592 1955 41742 21.4 | 3.326 % | c ============================================================================== c (current CPU-time: 7.46586 s) c ============================================================================== c [1mFound solution: 43560[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 13998 | 5941 20724 | 1782 2079 46369 22.3 | 3.326 % | c -- subsuming c -- var.elim.: 108/108 c -- var.elim.: 76/76 c | 13998 | 5909 20785 | -- 2079 -- -- | -- | -32/62 c | 13998 | 5909 20785 | 2363 2079 46369 22.3 | 3.326 % | c | 14098 | 5909 20785 | 2599 2179 50090 23.0 | 3.395 % | c | 14249 | 5909 20785 | 2859 2330 53929 23.1 | 3.395 % | c | 14474 | 5909 20785 | 3145 2555 65588 25.7 | 3.395 % | c | 14813 | 5909 20785 | 3460 2894 78250 27.0 | 3.395 % | c | 15319 | 5909 20785 | 3806 3400 100890 29.7 | 3.395 % | c | 16078 | 5909 20785 | 4187 2776 77710 28.0 | 3.395 % | c | 17217 | 5909 20785 | 4605 3915 128590 32.8 | 3.395 % | c | 18926 | 5909 20785 | 5066 4061 148566 36.6 | 3.395 % | c ============================================================================== c (current CPU-time: 11.4313 s) c ============================================================================== c [1mFound solution: 43558[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 20817 | 5973 20975 | 1791 4207 142474 33.9 | 3.395 % | c -- subsuming c -- var.elim.: 122/122 c -- var.elim.: 81/81 c | 20817 | 5934 21122 | -- 4207 -- -- | -- | -39/148 c | 20817 | 5934 21122 | 2373 4207 142474 33.9 | 3.395 % | c | 20917 | 5934 21122 | 2610 1970 42971 21.8 | 3.464 % | c ============================================================================== c (current CPU-time: 11.6472 s) c ============================================================================== c [1mFound solution: 43555[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 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 | 21048 | 5974 21246 | 1792 2101 47253 22.5 | 3.464 % | c -- subsuming c -- var.elim.: 90/90 c -- var.elim.: 58/58 c | 21048 | 5945 21215 | -- 2101 -- -- | -- | -29/-30 c | 21048 | 5945 21215 | 2378 2101 47253 22.5 | 3.464 % | c | 21148 | 5945 21215 | 2615 2201 52251 23.7 | 3.533 % | c | 21298 | 5945 21215 | 2877 2351 57415 24.4 | 3.533 % | c | 21524 | 5945 21215 | 3165 2577 68857 26.7 | 3.533 % | c ============================================================================== c (current CPU-time: 11.9562 s) c ============================================================================== c [1mFound solution: 43550[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 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 | 21565 | 5982 21323 | 1794 2618 71134 27.2 | 3.533 % | c -- subsuming c -- var.elim.: 70/70 c -- var.elim.: 47/47 c | 21565 | 5959 21360 | -- 2618 -- -- | -- | -23/38 c | 21565 | 5959 21360 | 2383 2618 71134 27.2 | 3.533 % | c | 21665 | 5959 21360 | 2621 1846 42584 23.1 | 3.602 % | c | 21815 | 5959 21360 | 2884 1996 49413 24.8 | 3.602 % | c ============================================================================== c (current CPU-time: 12.2241 s) c ============================================================================== c [1mFound solution: 43549[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 21961 | 6015 21534 | 1804 2142 55511 25.9 | 3.602 % | c -- subsuming c -- var.elim.: 115/115 c -- var.elim.: 79/79 c | 21961 | 5979 21644 | -- 2142 -- -- | -- | -36/111 c | 21961 | 5979 21644 | 2391 2142 55511 25.9 | 3.602 % | c | 22062 | 5979 21644 | 2630 2243 59768 26.6 | 3.670 % | c | 22213 | 5979 21644 | 2893 2394 63820 26.7 | 3.670 % | c | 22438 | 5979 21644 | 3183 2619 74647 28.5 | 3.670 % | c ============================================================================== c (current CPU-time: 12.5661 s) c ============================================================================== c [1mFound solution: 43491[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 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 | 22468 | 6008 21730 | 1802 2649 76703 29.0 | 3.670 % | c -- subsuming c -- var.elim.: 75/75 c -- var.elim.: 38/38 c | 22468 | 5989 21724 | -- 2649 -- -- | -- | -19/-5 c | 22468 | 5989 21724 | 2395 2649 76703 29.0 | 3.670 % | c | 22568 | 5989 21724 | 2635 1866 40755 21.8 | 3.738 % | c | 22718 | 5989 21724 | 2898 2016 43937 21.8 | 3.738 % | c | 22944 | 5989 21724 | 3188 2242 54424 24.3 | 3.738 % | c ============================================================================== c (current CPU-time: 12.98 s) c ============================================================================== c [1mFound solution: 43411[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 23128 | 6032 21865 | 1809 2426 64176 26.5 | 3.738 % | c -- subsuming c -- var.elim.: 97/97 c -- var.elim.: 70/70 c | 23128 | 6005 21890 | -- 2426 -- -- | -- | -27/26 c | 23128 | 6005 21890 | 2402 2426 64176 26.5 | 3.738 % | c | 23228 | 6005 21890 | 2642 2526 67835 26.9 | 3.802 % | c | 23378 | 6005 21890 | 2906 2676 73580 27.5 | 3.803 % | c | 23605 | 6005 21890 | 3197 2903 86480 29.8 | 3.805 % | c ============================================================================== c (current CPU-time: 13.355 s) c ============================================================================== c [1mFound solution: 43405[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 23876 | 6063 22068 | 1818 3174 93230 29.4 | 3.805 % | c -- subsuming c -- var.elim.: 117/117 c -- var.elim.: 80/80 c | 23876 | 6026 22122 | -- 3174 -- -- | -- | -37/55 c | 23876 | 6026 22122 | 2410 3174 93230 29.4 | 3.805 % | c ============================================================================== c (current CPU-time: 13.5039 s) c ============================================================================== c [1mFound solution: 43354[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 23975 | 6086 22307 | 1825 2215 53841 24.3 | 3.805 % | c -- subsuming c -- var.elim.: 122/122 c -- var.elim.: 82/82 c | 23975 | 6048 22433 | -- 2215 -- -- | -- | -38/127 c | 23975 | 6048 22433 | 2419 2215 53841 24.3 | 3.805 % | c | 24076 | 6048 22433 | 2661 2316 58984 25.5 | 3.931 % | c | 24227 | 6048 22433 | 2927 2467 64172 26.0 | 3.931 % | c | 24452 | 6048 22433 | 3219 2692 77743 28.9 | 3.931 % | c ============================================================================== c (current CPU-time: 14.0199 s) c ============================================================================== c [1mFound solution: 43296[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 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 | 24785 | 6097 22592 | 1829 3025 95906 31.7 | 3.931 % | c -- subsuming c -- var.elim.: 116/116 c -- var.elim.: 77/77 c | 24785 | 6061 22497 | -- 3025 -- -- | -- | -36/-94 c | 24785 | 6061 22497 | 2424 3025 95906 31.7 | 3.931 % | c | 24887 | 6061 22497 | 2666 2119 61088 28.8 | 3.994 % | c | 25037 | 5939 21701 | 2874 1939 45978 23.7 | 5.200 % | c ============================================================================== c (current CPU-time: 14.2908 s) c ============================================================================== c [1mFound solution: 43264[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 425 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 | 25069 | 6825 23788 | 2047 1971 47158 23.9 | 5.200 % | c -- subsuming c -- var.elim.: 628/628 c -- var.elim.: 290/290 c -- var.elim.: 6/6 c -- var.elim.: 7/7 c -- subsuming c -- var.elim.: 90/90 c -- var.elim.: 30/30 c | 25069 | 6618 23995 | -- 1971 -- -- | -- | -207/208 c | 25069 | 6618 23995 | 2647 1685 29869 17.7 | 5.200 % | c | 25169 | 6618 23995 | 2911 1785 34104 19.1 | 4.762 % | c | 25319 | 6618 23995 | 3203 1935 42287 21.9 | 4.762 % | c | 25544 | 6618 23995 | 3523 2160 50242 23.3 | 4.762 % | c | 25882 | 6618 23995 | 3875 2498 63597 25.5 | 4.762 % | c ============================================================================== c (current CPU-time: 15.0677 s) c ============================================================================== c [1mFound solution: 43262[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 26306 | 6701 24232 | 2010 2922 81400 27.9 | 4.762 % | c -- subsuming c -- var.elim.: 177/177 c -- var.elim.: 96/96 c | 26306 | 6651 24296 | -- 2922 -- -- | -- | -50/65 c | 26306 | 6651 24296 | 2660 2922 81400 27.9 | 4.762 % | c | 26406 | 6651 24296 | 2926 2048 49932 24.4 | 4.811 % | c ============================================================================== c (current CPU-time: 15.2497 s) c ============================================================================== c [1mFound solution: 43259[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 26465 | 6708 24468 | 2012 2107 51873 24.6 | 4.811 % | c -- subsuming c -- var.elim.: 122/122 c -- var.elim.: 79/79 c | 26465 | 6668 24413 | -- 2107 -- -- | -- | -40/-54 c | 26465 | 6668 24413 | 2667 2107 51873 24.6 | 4.811 % | c | 26565 | 6668 24413 | 2933 2207 56732 25.7 | 4.865 % | c | 26715 | 6668 24413 | 3227 2357 61901 26.3 | 4.867 % | c | 26940 | 6668 24413 | 3550 2582 71746 27.8 | 4.865 % | c | 27278 | 6668 24413 | 3905 2920 88656 30.4 | 4.865 % | c | 27784 | 6528 22336 | 4205 3020 91421 30.3 | 4.935 % | c ============================================================================== c (current CPU-time: 16.2415 s) c ============================================================================== c [1mFound solution: 43250[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 28058 | 6601 22546 | 1980 3294 105031 31.9 | 4.935 % | c -- subsuming c -- var.elim.: 176/176 c -- var.elim.: 105/105 c -- var.elim.: 50/50 c -- var.elim.: 6/6 c | 28058 | 6540 22320 | -- 3294 -- -- | -- | -61/-225 c | 28058 | 6540 22320 | 2616 2538 53066 20.9 | 4.935 % | c | 28160 | 6540 22320 | 2877 2640 58215 22.1 | 5.000 % | c | 28314 | 6540 22320 | 3165 2794 69439 24.9 | 5.000 % | c | 28540 | 6540 22320 | 3481 3020 84033 27.8 | 5.000 % | c | 28878 | 6540 22320 | 3830 3358 100386 29.9 | 5.000 % | c | 29384 | 6540 22320 | 4213 3864 131256 34.0 | 5.000 % | c ============================================================================== c (current CPU-time: 17.2374 s) c ============================================================================== c [1mFound solution: 43248[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 29513 | 6601 22502 | 1980 3993 134859 33.8 | 5.000 % | c -- subsuming c -- var.elim.: 128/128 c -- var.elim.: 82/82 c | 29513 | 6558 22453 | -- 3993 -- -- | -- | -43/-48 c | 29513 | 6558 22453 | 2623 3993 134859 33.8 | 5.000 % | c | 29614 | 6558 22453 | 2885 2763 92851 33.6 | 5.054 % | c | 29764 | 6538 22393 | 3164 2910 98834 34.0 | 5.256 % | c ============================================================================== c (current CPU-time: 17.5333 s) c ============================================================================== c [1mFound solution: 43246[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 29795 | 6611 22602 | 1983 2941 99699 33.9 | 5.256 % | c -- subsuming c -- var.elim.: 160/160 c -- var.elim.: 97/97 c | 29795 | 6567 22643 | -- 2941 -- -- | -- | -44/42 c | 29795 | 6567 22643 | 2626 2941 99699 33.9 | 5.256 % | c | 29896 | 6567 22643 | 2889 1928 48852 25.3 | 5.313 % | c | 30047 | 6567 22643 | 3178 2079 55845 26.9 | 5.313 % | c | 30272 | 6567 22643 | 3496 2304 66422 28.8 | 5.313 % | c ============================================================================== c (current CPU-time: 18.0083 s) c ============================================================================== c [1mFound solution: 43231[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 248 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 | 30495 | 6820 22344 | 2045 2523 74760 29.6 | 5.313 % | c -- subsuming c -- var.elim.: 583/583 c -- var.elim.: 403/403 c -- var.elim.: 81/81 c -- var.elim.: 13/13 c -- subsuming c -- var.elim.: 149/149 c -- var.elim.: 70/70 c | 30495 | 6373 20708 | -- 2523 -- -- | -- | -317/-864 c | 30495 | 6373 20708 | 2549 2523 74760 29.6 | 5.313 % | c | 30597 | 6327 20477 | 2783 2623 76395 29.1 | 8.149 % | c ============================================================================== c (current CPU-time: 18.2312 s) c ============================================================================== c [1mFound solution: 43229[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 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 | 30664 | 6410 20712 | 1922 2690 78526 29.2 | 8.149 % | c -- subsuming c -- var.elim.: 234/234 c -- var.elim.: 144/144 c -- var.elim.: 26/26 c | 30664 | 6342 20791 | -- 2690 -- -- | -- | -68/80 c | 30664 | 6342 20791 | 2536 1691 24336 14.4 | 8.149 % | c | 30764 | 6235 20325 | 2743 1790 26243 14.7 | 9.141 % | c | 30914 | 6235 20325 | 3017 1940 31028 16.0 | 9.140 % | c ============================================================================== c (current CPU-time: 18.5332 s) c ============================================================================== c [1mFound solution: 43228[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 31110 | 6282 20457 | 1884 2133 35867 16.8 | 9.140 % | c -- subsuming c -- var.elim.: 295/295 c -- var.elim.: 162/162 c -- subsuming c -- var.elim.: 48/48 c | 31110 | 6228 20401 | -- 2133 -- -- | -- | -52/-51 c | 31110 | 6228 20401 | 2491 2097 33873 16.2 | 9.140 % | c | 31210 | 6216 20340 | 2735 2196 36665 16.7 | 9.660 % | c | 31360 | 6216 20340 | 3008 2346 39984 17.0 | 9.660 % | c ============================================================================== c (current CPU-time: 18.7891 s) c ============================================================================== c [1mFound solution: 43202[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 31434 | 6288 20533 | 1886 2415 41565 17.2 | 9.660 % | c -- subsuming c -- var.elim.: 171/171 c -- var.elim.: 108/108 c | 31434 | 6237 20700 | -- 2415 -- -- | -- | -50/170 c | 31434 | 6237 20700 | 2494 2415 41565 17.2 | 9.660 % | c | 31535 | 6237 20700 | 2744 2516 43568 17.3 | 9.925 % | c | 31685 | 6237 20700 | 3018 2666 48462 18.2 | 9.926 % | c | 31910 | 6202 20585 | 3301 2492 42533 17.1 | 10.402 % | c ============================================================================== c (current CPU-time: 19.1821 s) c ============================================================================== c [1mFound solution: 43190[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 32089 | 6262 20733 | 1878 2657 47012 17.7 | 10.402 % | c -- subsuming c -- var.elim.: 210/210 c -- var.elim.: 109/109 c | 32089 | 6205 20753 | -- 2657 -- -- | -- | -57/21 c | 32089 | 6205 20753 | 2482 2523 42930 17.0 | 10.402 % | c | 32189 | 6205 20753 | 2730 2623 46635 17.8 | 10.741 % | c | 32340 | 6205 20753 | 3003 2774 51904 18.7 | 10.741 % | c | 32565 | 6205 20753 | 3303 2999 58185 19.4 | 10.742 % | c ============================================================================== c (current CPU-time: 19.695 s) c ============================================================================== c [1mFound solution: 43151[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 32815 | 6275 20956 | 1882 3249 67116 20.7 | 10.742 % | c -- subsuming c -- var.elim.: 144/144 c -- var.elim.: 83/83 c | 32815 | 6227 20862 | -- 3249 -- -- | -- | -48/-93 c | 32815 | 6227 20862 | 2490 3249 67116 20.7 | 10.742 % | c | 32915 | 6227 20862 | 2739 2266 44375 19.6 | 10.787 % | c | 33066 | 6227 20862 | 3013 2417 48436 20.0 | 10.787 % | c | 33292 | 6227 20862 | 3315 2643 57390 21.7 | 10.787 % | c | 33630 | 6227 20862 | 3646 2981 72527 24.3 | 10.787 % | c ============================================================================== c (current CPU-time: 20.4409 s) c ============================================================================== c [1mFound solution: 43149[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 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 | 34008 | 6286 21023 | 1885 3359 83766 24.9 | 10.787 % | c -- subsuming c -- var.elim.: 100/100 c -- var.elim.: 61/61 c | 34008 | 6252 21024 | -- 3359 -- -- | -- | -34/2 c | 34008 | 6252 21024 | 2500 3359 83766 24.9 | 10.787 % | c | 34108 | 6252 21024 | 2750 2340 52959 22.6 | 10.833 % | c ============================================================================== c (current CPU-time: 20.6259 s) c ============================================================================== c [1mFound solution: 43145[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 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 34130 | 6332 21249 | 1899 2362 53530 22.7 | 10.833 % | c -- subsuming c -- var.elim.: 141/141 c -- var.elim.: 87/87 c | 34130 | 6283 21295 | -- 2362 -- -- | -- | -49/47 c | 34130 | 6283 21295 | 2513 2362 53530 22.7 | 10.833 % | c | 34232 | 6283 21295 | 2764 2464 56737 23.0 | 10.879 % | c | 34382 | 6283 21295 | 3040 2614 65170 24.9 | 10.878 % | c ============================================================================== c (current CPU-time: 20.9478 s) c ============================================================================== c [1mFound solution: 43133[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 34593 | 6362 21518 | 1908 2825 72418 25.6 | 10.878 % | c -- subsuming c -- var.elim.: 141/141 c -- var.elim.: 87/87 c | 34593 | 6313 21548 | -- 2825 -- -- | -- | -49/31 c | 34593 | 6313 21548 | 2525 2825 72418 25.6 | 10.878 % | c | 34694 | 6313 21548 | 2777 1985 43156 21.7 | 10.924 % | c | 34844 | 6313 21548 | 3055 2135 49450 23.2 | 10.924 % | c | 35069 | 6313 21548 | 3361 2360 56990 24.1 | 10.924 % | c | 35408 | 6313 21548 | 3697 2699 69772 25.9 | 10.925 % | c ============================================================================== c (current CPU-time: 21.7577 s) c ============================================================================== c [1mFound solution: 43132[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 35838 | 6383 21751 | 1914 3129 92092 29.4 | 10.925 % | c -- subsuming c -- var.elim.: 135/135 c -- var.elim.: 84/84 c | 35838 | 6340 21744 | -- 3129 -- -- | -- | -43/-6 c | 35838 | 6340 21744 | 2536 3129 92092 29.4 | 10.925 % | c | 35938 | 6340 21744 | 2789 2186 56295 25.8 | 10.969 % | c ============================================================================== c (current CPU-time: 21.9687 s) c ============================================================================== c [1mFound solution: 43130[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 36030 | 6423 21977 | 1926 2278 62950 27.6 | 10.969 % | c -- subsuming c -- var.elim.: 145/145 c -- var.elim.: 89/89 c | 36030 | 6374 22065 | -- 2278 -- -- | -- | -49/89 c | 36030 | 6374 22065 | 2549 2278 62950 27.6 | 10.969 % | c | 36132 | 6374 22065 | 2804 2380 68873 28.9 | 11.014 % | c ============================================================================== c (current CPU-time: 22.1596 s) c ============================================================================== c [1mFound solution: 43127[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 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 36195 | 6444 22267 | 1933 2443 71275 29.2 | 11.014 % | c -- subsuming c -- var.elim.: 137/137 c -- var.elim.: 83/83 c | 36195 | 6398 22201 | -- 2443 -- -- | -- | -46/-65 c | 36195 | 6398 22201 | 2559 2443 71275 29.2 | 11.014 % | c | 36296 | 6398 22201 | 2815 2544 75813 29.8 | 11.059 % | c | 36447 | 6398 22201 | 3096 2695 82388 30.6 | 11.059 % | c ============================================================================== c (current CPU-time: 22.4926 s) c ============================================================================== c [1mFound solution: 43104[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 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 | 36574 | 6467 22404 | 1940 2822 86041 30.5 | 11.059 % | c -- subsuming c -- var.elim.: 132/132 c -- var.elim.: 84/84 c | 36574 | 6424 22387 | -- 2822 -- -- | -- | -43/-16 c | 36574 | 6424 22387 | 2569 2822 86041 30.5 | 11.059 % | c | 36674 | 6424 22387 | 2826 1982 52285 26.4 | 11.104 % | c | 36824 | 6424 22387 | 3109 2132 57707 27.1 | 11.104 % | c | 37052 | 6424 22387 | 3420 2360 73773 31.3 | 11.104 % | c | 37389 | 6424 22387 | 3762 2697 85447 31.7 | 11.104 % | c ============================================================================== c (current CPU-time: 23.1735 s) c ============================================================================== c [1mFound solution: 43101[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 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 | 37678 | 6502 22609 | 1950 2986 94540 31.7 | 11.104 % | c -- subsuming c -- var.elim.: 140/140 c -- var.elim.: 87/87 c | 37678 | 6454 22669 | -- 2986 -- -- | -- | -48/61 c | 37678 | 6454 22669 | 2581 2986 94540 31.7 | 11.104 % | c | 37778 | 6454 22669 | 2839 2091 48825 23.4 | 11.149 % | c ============================================================================== c (current CPU-time: 23.4074 s) c ============================================================================== c [1mFound solution: 43100[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 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 | 37907 | 6522 22869 | 1956 2220 55768 25.1 | 11.149 % | c -- subsuming c -- var.elim.: 134/134 c -- var.elim.: 84/84 c | 37907 | 6480 22852 | -- 2220 -- -- | -- | -42/-16 c | 37907 | 6480 22852 | 2592 2220 55768 25.1 | 11.149 % | c | 38008 | 6480 22852 | 2851 2321 58381 25.2 | 11.193 % | c ============================================================================== c (current CPU-time: 23.5844 s) c ============================================================================== c [1mFound solution: 43099[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 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 | 38041 | 6545 23044 | 1963 2354 59395 25.2 | 11.193 % | c -- subsuming c -- var.elim.: 125/125 c -- var.elim.: 81/81 c | 38041 | 6506 23035 | -- 2354 -- -- | -- | -39/-8 c | 38041 | 6506 23035 | 2602 2354 59395 25.2 | 11.193 % | c | 38141 | 6506 23035 | 2862 2454 61891 25.2 | 11.237 % | c | 38293 | 6506 23035 | 3148 2606 73686 28.3 | 11.237 % | c | 38518 | 6506 23035 | 3463 2831 80971 28.6 | 11.237 % | c | 38855 | 6506 23035 | 3810 3168 96893 30.6 | 11.237 % | c ============================================================================== c (current CPU-time: 24.2013 s) c ============================================================================== c [1mFound solution: 43097[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 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 | 38969 | 6582 23253 | 1974 3282 100712 30.7 | 11.237 % | c -- subsuming c -- var.elim.: 138/138 c -- var.elim.: 87/87 c | 38969 | 6536 23307 | -- 3282 -- -- | -- | -46/55 c | 38969 | 6536 23307 | 2614 3282 100712 30.7 | 11.237 % | c | 39071 | 6536 23307 | 2875 2290 58506 25.5 | 11.281 % | c | 39221 | 6536 23307 | 3163 2440 66308 27.2 | 11.281 % | c | 39446 | 5425 18600 | 2888 1533 18232 11.9 | 22.163 % | c ============================================================================== c [1mOptimal solution: 43097[0m s OPTIMUM FOUND v -VOL1_bit_7 -VOL1_bit_6 VOL1_bit_5 VOL1_bit_4 -VOL1_bit_3 VOL1_bit_2 -VOL1_bit_1 VOL1_bit0 VOL1_bit1 -VOL1_bit2 -VOL1_bit3 -VOL1_bit4 -VOL1_bit5 -VOL1_bit6 -VOL1_bit7 -VOL1_bit8 -VOL1_bit9 -VOL1_bit10 -VOL1_bit11 -VOL1_bit12 VOL2_bit_7 -VOL2_bit_6 -VOL2_bit_5 VOL2_bit_4 -VOL2_bit_3 VOL2_bit_2 -VOL2_bit_1 VOL2_bit0 -VOL2_bit1 VOL2_bit2 VOL2_bit3 -VOL2_bit4 -VOL2_bit5 -VOL2_bit6 -VOL2_bit7 -VOL2_bit8 -VOL2_bit9 -VOL2_bit10 -VOL2_bit11 -VOL2_bit12 -VOL3_bit_7 -VOL3_bit_6 -VOL3_bit_5 -VOL3_bit_4 -VOL3_bit_3 -VOL3_bit_2 -VOL3_bit_1 -VOL3_bit0 VOL3_bit1 VOL3_bit2 VOL3_bit3 VOL3_bit4 -VOL4_bit_7 -VOL4_bit_6 -VOL4_bit_5 -VOL4_bit_4 -VOL4_bit_3 -VOL4_bit_2 -VOL4_bit_1 -VOL4_bit0 -VOL4_bit1 -VOL4_bit2 -VOL4_bit3 -VOL4_bit4 c _______________________________________________________________________________ c c restarts : 182 c conflicts : 39447 (1603 /sec) c decisions : 58525 (2378 /sec) c propagations : 6200774 (251959 /sec) c inspects : 42406348 (1723117 /sec) c CPU time : 24.6103 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.73 0.91 0.89 2/55 14797 Raw data (stat): 14797 (runsolver) R 14796 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539842577 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99964 s] Raw data (loadavg): 0.77 0.91 0.89 2/55 14797 Raw data (stat): 14797 (minisat+) R 14796 22929 22928 0 -1 0 1546 0 0 0 991 7 0 0 25 0 1 0 539842577 5373952 929 4294967295 134512640 134672761 3221224544 3221223536 134565143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1312 929 603 41 0 1271 0 vsize: 5248 [startup+19.9996 s] Raw data (loadavg): 0.80 0.91 0.89 2/55 14797 Raw data (stat): 14797 (minisat+) R 14796 22929 22928 0 -1 0 3215 0 0 0 1982 15 0 0 25 0 1 0 539842577 6225920 1109 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1520 1109 603 41 0 1479 0 vsize: 6080 [startup+24.8448 s] Raw data (loadavg): 0.82 0.91 0.89 1/54 14797 Raw data (stat): 14797 (minisat+) R 14796 22929 22928 0 -1 0 3215 0 0 0 1982 15 0 0 25 0 1 0 539842577 6225920 1109 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1520 1109 603 41 0 1479 0 vsize: 0 Child status: 30 Real time (s): 24.8446 CPU time (s): 24.8152 CPU user time (s): 24.6133 CPU system time (s): 0.201969 CPU usage (%): 99.8819 Max. virtual memory (Kb): 6080 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 43097 #### END VERIFIER DATA ####