PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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
Trace number 13759

#### 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 ####