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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos1.opb
MD5SUM	3fce91583b30a82646d8d8e778b97a89
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	19
Optimality of the best value was proved	NO
Number of terms in the objective function	288
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	288
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	5
Number of bits of the biggest number in a constraint	3
Biggest sum of numbers in a constraint	288
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07084
Number of variables	2112
Total number of constraints	7132
Number of constraints which are clauses	4128
Number of constraints which are cardinality constraints (but not clauses)	2328
Number of constraints which are nor clauses,nor cardinality constraints	676
Minimum length of a constraint	1
Maximum length of a constraint	32
Trace number 14001

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-20 22:53:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19654 boxname=wulflinc17 idbench=1512 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3fce91583b30a82646d8d8e778b97a89  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-neos1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-neos1.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-neos1.opb
IDLAUNCH: 19654
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        668096 kB
Buffers:         33460 kB
Cached:         300712 kB
SwapCached:         48 kB
Active:          96312 kB
Inactive:       240788 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        667844 kB
SwapTotal:     2097892 kB
SwapFree:      2097840 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           7032 kB
Slab:            23796 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:55:06 (client local time) WITH STATUS 30 IN 106.745 SECONDS
stats: 19654 0 106.745 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5120 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[5118]---> Sorter-cost:  383     Base:
c ---[5116]---> Sorter-cost:  265     Base:
c ---[5114]---> Sorter-cost:  265     Base:
c ---[5112]---> Sorter-cost:  383     Base:
c ---[5110]---> Sorter-cost:  383     Base:
c ---[5108]---> Sorter-cost:  383     Base:
c ---[5106]---> Sorter-cost:  265     Base:
c ---[5104]---> Sorter-cost:  265     Base:
c ---[5102]---> Sorter-cost:  383     Base:
c ---[5100]---> Sorter-cost:  383     Base:
c ---[5098]---> Sorter-cost:  383     Base:
c ---[5096]---> Sorter-cost:  265     Base:
c ---[5094]---> Sorter-cost:  265     Base:
c ---[5092]---> Sorter-cost:  265     Base:
c ---[5090]---> Sorter-cost:  345     Base:
c ---[5088]---> Sorter-cost:  383     Base:
c ---[5086]---> Sorter-cost:  265     Base:
c ---[5084]---> Sorter-cost:  265     Base:
c ---[5082]---> Sorter-cost:  265     Base:
c ---[5080]---> Sorter-cost:  345     Base:
c ---[5078]---> Sorter-cost:  245     Base:
c ---[5076]---> Sorter-cost:  325     Base:
c ---[5074]---> Sorter-cost:  325     Base:
c ---[5072]---> Sorter-cost:  207     Base:
c ---[5070]---> Sorter-cost:  189     Base:
c ---[5068]---> Sorter-cost:  269     Base:
c ---[5066]---> Sorter-cost:  269     Base:
c ---[5064]---> Sorter-cost:  151     Base:
c ---[5062]---> Sorter-cost:  363     Base:
c ---[5060]---> Sorter-cost:  207     Base:
c ---[5058]---> Sorter-cost:  325     Base:
c ---[5056]---> Sorter-cost:  287     Base:
c ---[5054]---> Sorter-cost:  307     Base:
c ---[5052]---> Sorter-cost:  307     Base:
c ---[5050]---> Sorter-cost:  189     Base:
c ---[5048]---> Sorter-cost:  231     Base:
c ---[5046]---> Sorter-cost:  363     Base:
c ---[5044]---> Sorter-cost:  325     Base:
c ---[5042]---> Sorter-cost:  325     Base:
c ---[5040]---> Sorter-cost:  169     Base:
c ---[5038]---> Sorter-cost:  227     Base:
c ---[5036]---> Sorter-cost:  307     Base:
c ---[5034]---> Sorter-cost:  269     Base:
c ---[5032]---> Sorter-cost:  231     Base:
c ---[5030]---> Sorter-cost:  363     Base:
c ---[5028]---> Sorter-cost:  207     Base:
c ---[5026]---> Sorter-cost:  325     Base:
c ---[5024]---> Sorter-cost:  169     Base:
c ---[5022]---> Sorter-cost:  227     Base:
c ---[5020]---> Sorter-cost:  307     Base:
c ---[5018]---> Sorter-cost:  269     Base:
c ---[5016]---> Sorter-cost:  231     Base:
c ---[5014]---> Sorter-cost:  363     Base:
c ---[5012]---> Sorter-cost:  207     Base:
c ---[5010]---> Sorter-cost:  325     Base:
c ---[5008]---> Sorter-cost:  207     Base:
c ---[5006]---> Sorter-cost:  189     Base:
c ---[5004]---> Sorter-cost:  307     Base:
c ---[5002]---> Sorter-cost:  189     Base:
c ---[5000]---> Sorter-cost:  231     Base:
c ---[4998]---> Sorter-cost:  245     Base:
c ---[4996]---> Sorter-cost:  325     Base:
c ---[4994]---> Sorter-cost:  325     Base:
c ---[4992]---> Sorter-cost:  207     Base:
c ---[4990]---> Sorter-cost:  189     Base:
c ---[4988]---> Sorter-cost:  269     Base:
c ---[4986]---> Sorter-cost:  269     Base:
c ---[4984]---> Sorter-cost:  151     Base:
c ---[4982]---> Sorter-cost:  363     Base:
c ---[4980]---> Sorter-cost:  207     Base:
c ---[4978]---> Sorter-cost:  325     Base:
c ---[4976]---> Sorter-cost:  287     Base:
c ---[4974]---> Sorter-cost:  307     Base:
c ---[4972]---> Sorter-cost:  307     Base:
c ---[4970]---> Sorter-cost:  189     Base:
c ---[4968]---> Sorter-cost:  231     Base:
c ---[4966]---> Sorter-cost:  363     Base:
c ---[4964]---> Sorter-cost:  325     Base:
c ---[4962]---> Sorter-cost:  325     Base:
c ---[4960]---> Sorter-cost:  169     Base:
c ---[4958]---> Sorter-cost:  227     Base:
c ---[4956]---> Sorter-cost:  307     Base:
c ---[4954]---> Sorter-cost:  269     Base:
c ---[4952]---> Sorter-cost:  231     Base:
c ---[4950]---> Sorter-cost:  363     Base:
c ---[4948]---> Sorter-cost:  207     Base:
c ---[4946]---> Sorter-cost:  325     Base:
c ---[4944]---> Sorter-cost:  169     Base:
c ---[4942]---> Sorter-cost:  227     Base:
c ---[4940]---> Sorter-cost:  307     Base:
c ---[4938]---> Sorter-cost:  269     Base:
c ---[4936]---> Sorter-cost:  231     Base:
c ---[4934]---> Sorter-cost:  363     Base:
c ---[4932]---> Sorter-cost:  207     Base:
c ---[4930]---> Sorter-cost:  325     Base:
c ---[4928]---> Sorter-cost:  207     Base:
c ---[4926]---> Sorter-cost:  189     Base:
c ---[4924]---> Sorter-cost:  307     Base:
c ---[4922]---> Sorter-cost:  189     Base:
c ---[4920]---> Sorter-cost:  231     Base:
c ---[4919]---> BDD-cost:   27
c ---[4918]---> BDD-cost:   27
c ---[4917]---> BDD-cost:   27
c ---[4916]---> BDD-cost:   27
c ---[4915]---> BDD-cost:   27
c ---[4914]---> BDD-cost:   27
c ---[4913]---> BDD-cost:   27
c ---[4912]---> BDD-cost:   27
c ---[4911]---> BDD-cost:   27
c ---[4910]---> BDD-cost:   27
c ---[4909]---> BDD-cost:   27
c ---[4908]---> BDD-cost:   27
c ---[4907]---> BDD-cost:   27
c ---[4906]---> BDD-cost:   27
c ---[4905]---> BDD-cost:   27
c ---[4904]---> BDD-cost:   27
c ---[4903]---> BDD-cost:   27
c ---[4902]---> BDD-cost:   27
c ---[4901]---> BDD-cost:   27
c ---[4900]---> BDD-cost:   27
c ---[4899]---> BDD-cost:    0
c ---[4898]---> BDD-cost:    0
c ---[4897]---> BDD-cost:    0
c ---[4896]---> BDD-cost:    0
c ---[4895]---> BDD-cost:    0
c ---[4894]---> BDD-cost:    0
c ---[4893]---> BDD-cost:    0
c ---[4892]---> BDD-cost:    0
c ---[4891]---> BDD-cost:    0
c ---[4890]---> BDD-cost:    0
c ---[4889]---> BDD-cost:    0
c ---[4888]---> BDD-cost:    0
c ---[4887]---> BDD-cost:    0
c ---[4886]---> BDD-cost:    0
c ---[4885]---> BDD-cost:    0
c ---[4884]---> BDD-cost:    0
c ---[4883]---> BDD-cost:    0
c ---[4882]---> BDD-cost:    0
c ---[4881]---> BDD-cost:    0
c ---[4880]---> BDD-cost:    0
c ---[4879]---> BDD-cost:   27
c ---[4878]---> BDD-cost:   27
c ---[4877]---> BDD-cost:   27
c ---[4876]---> BDD-cost:   27
c ---[4875]---> BDD-cost:   27
c ---[4874]---> BDD-cost:    0
c ---[4873]---> BDD-cost:    0
c ---[4872]---> BDD-cost:    0
c ---[4871]---> BDD-cost:    0
c ---[4870]---> BDD-cost:    0
c ---[4869]---> BDD-cost:   27
c ---[4868]---> BDD-cost:   27
c ---[4867]---> BDD-cost:   27
c ---[4866]---> BDD-cost:   27
c ---[4865]---> BDD-cost:   27
c ---[4864]---> BDD-cost:    0
c ---[4863]---> BDD-cost:    0
c ---[4862]---> BDD-cost:    0
c ---[4861]---> BDD-cost:    0
c ---[4860]---> BDD-cost:    0
c ---[4859]---> BDD-cost:   27
c ---[4858]---> BDD-cost:   27
c ---[4857]---> BDD-cost:   27
c ---[4856]---> BDD-cost:   27
c ---[4855]---> BDD-cost:   27
c ---[4854]---> BDD-cost:    0
c ---[4853]---> BDD-cost:    0
c ---[4852]---> BDD-cost:    0
c ---[4851]---> BDD-cost:    0
c ---[4850]---> BDD-cost:    0
c ---[4849]---> BDD-cost:   27
c ---[4848]---> BDD-cost:   27
c ---[4847]---> BDD-cost:   27
c ---[4846]---> BDD-cost:   27
c ---[4845]---> BDD-cost:   27
c ---[4844]---> BDD-cost:    0
c ---[4843]---> BDD-cost:    0
c ---[4842]---> BDD-cost:    0
c ---[4841]---> BDD-cost:    0
c ---[4840]---> BDD-cost:    0
c ---[4839]---> BDD-cost:   27
c ---[4838]---> BDD-cost:   27
c ---[4837]---> BDD-cost:   27
c ---[4836]---> BDD-cost:   27
c ---[4835]---> BDD-cost:   27
c ---[4834]---> BDD-cost:    0
c ---[4833]---> BDD-cost:    0
c ---[4832]---> BDD-cost:    0
c ---[4831]---> BDD-cost:    0
c ---[4830]---> BDD-cost:    0
c ---[4829]---> BDD-cost:   27
c ---[4828]---> BDD-cost:   27
c ---[4827]---> BDD-cost:   27
c ---[4826]---> BDD-cost:   27
c ---[4825]---> BDD-cost:   27
c ---[4824]---> BDD-cost:    0
c ---[4823]---> BDD-cost:    0
c ---[4822]---> BDD-cost:    0
c ---[4821]---> BDD-cost:    0
c ---[4820]---> BDD-cost:    0
c ---[4819]---> BDD-cost:   27
c ---[4818]---> BDD-cost:   27
c ---[4817]---> BDD-cost:   27
c ---[4816]---> BDD-cost:   27
c ---[4815]---> BDD-cost:   27
c ---[4814]---> BDD-cost:    0
c ---[4813]---> BDD-cost:    0
c ---[4812]---> BDD-cost:    0
c ---[4811]---> BDD-cost:    0
c ---[4810]---> BDD-cost:    0
c ---[4809]---> BDD-cost:   27
c ---[4808]---> BDD-cost:   27
c ---[4807]---> BDD-cost:   27
c ---[4806]---> BDD-cost:   27
c ---[4805]---> BDD-cost:   27
c ---[4804]---> BDD-cost:    0
c ---[4803]---> BDD-cost:    0
c ---[4802]---> BDD-cost:    0
c ---[4801]---> BDD-cost:    0
c ---[4800]---> BDD-cost:    0
c ---[4799]---> BDD-cost:   27
c ---[4798]---> BDD-cost:   27
c ---[4797]---> BDD-cost:   27
c ---[4796]---> BDD-cost:   27
c ---[4795]---> BDD-cost:   27
c ---[4794]---> BDD-cost:    0
c ---[4793]---> BDD-cost:    0
c ---[4792]---> BDD-cost:    0
c ---[4791]---> BDD-cost:    0
c ---[4790]---> BDD-cost:    0
c ---[4789]---> BDD-cost:   27
c ---[4788]---> BDD-cost:   27
c ---[4787]---> BDD-cost:   27
c ---[4786]---> BDD-cost:   27
c ---[4785]---> BDD-cost:   27
c ---[4784]---> BDD-cost:    0
c ---[4783]---> BDD-cost:    0
c ---[4782]---> BDD-cost:    0
c ---[4781]---> BDD-cost:    0
c ---[4780]---> BDD-cost:    0
c ---[4779]---> BDD-cost:   27
c ---[4778]---> BDD-cost:   27
c ---[4777]---> BDD-cost:   27
c ---[4776]---> BDD-cost:   27
c ---[4775]---> BDD-cost:   27
c ---[4774]---> BDD-cost:    0
c ---[4773]---> BDD-cost:    0
c ---[4772]---> BDD-cost:    0
c ---[4771]---> BDD-cost:    0
c ---[4770]---> BDD-cost:    0
c ---[4769]---> BDD-cost:   27
c ---[4768]---> BDD-cost:   27
c ---[4767]---> BDD-cost:   27
c ---[4766]---> BDD-cost:   27
c ---[4765]---> BDD-cost:   27
c ---[4764]---> BDD-cost:    0
c ---[4763]---> BDD-cost:    0
c ---[4762]---> BDD-cost:    0
c ---[4761]---> BDD-cost:    0
c ---[4760]---> BDD-cost:    0
c ---[4759]---> BDD-cost:   27
c ---[4758]---> BDD-cost:   27
c ---[4757]---> BDD-cost:   27
c ---[4756]---> BDD-cost:   27
c ---[4755]---> BDD-cost:   27
c ---[4754]---> BDD-cost:    0
c ---[4753]---> BDD-cost:    0
c ---[4752]---> BDD-cost:    0
c ---[4751]---> BDD-cost:    0
c ---[4750]---> BDD-cost:    0
c ---[4749]---> BDD-cost:   27
c ---[4748]---> BDD-cost:   27
c ---[4747]---> BDD-cost:   27
c ---[4746]---> BDD-cost:   27
c ---[4745]---> BDD-cost:   27
c ---[4744]---> BDD-cost:    0
c ---[4743]---> BDD-cost:    0
c ---[4742]---> BDD-cost:    0
c ---[4741]---> BDD-cost:    0
c ---[4740]---> BDD-cost:    0
c ---[4739]---> BDD-cost:    5
c ---[4738]---> BDD-cost:    5
c ---[4737]---> BDD-cost:    5
c ---[4736]---> BDD-cost:    5
c ---[4735]---> BDD-cost:    5
c ---[4734]---> BDD-cost:    5
c ---[4733]---> BDD-cost:    5
c ---[4732]---> BDD-cost:    5
c ---[4731]---> BDD-cost:    5
c ---[4730]---> BDD-cost:    5
c ---[4729]---> BDD-cost:    5
c ---[4728]---> BDD-cost:    5
c ---[4727]---> BDD-cost:    5
c ---[4726]---> BDD-cost:    5
c ---[4725]---> BDD-cost:    5
c ---[4724]---> BDD-cost:    5
c ---[4723]---> BDD-cost:    5
c ---[4722]---> BDD-cost:    5
c ---[4721]---> BDD-cost:    5
c ---[4720]---> BDD-cost:    5
c ---[4719]---> BDD-cost:    5
c ---[4718]---> BDD-cost:    5
c ---[4717]---> BDD-cost:    5
c ---[4716]---> BDD-cost:    5
c ---[4715]---> BDD-cost:    5
c ---[4714]---> BDD-cost:    5
c ---[4713]---> BDD-cost:    5
c ---[4712]---> BDD-cost:    5
c ---[4711]---> BDD-cost:    5
c ---[4710]---> BDD-cost:    5
c ---[4709]---> BDD-cost:    5
c ---[4708]---> BDD-cost:    5
c ---[4707]---> BDD-cost:    5
c ---[4706]---> BDD-cost:    5
c ---[4705]---> BDD-cost:    5
c ---[4704]---> BDD-cost:    5
c ---[4703]---> BDD-cost:    5
c ---[4702]---> BDD-cost:    5
c ---[4701]---> BDD-cost:    5
c ---[4700]---> BDD-cost:    5
c ---[4699]---> BDD-cost:    5
c ---[4698]---> BDD-cost:    5
c ---[4697]---> BDD-cost:    5
c ---[4696]---> BDD-cost:    5
c ---[4695]---> BDD-cost:    5
c ---[4694]---> BDD-cost:    5
c ---[4693]---> BDD-cost:    5
c ---[4692]---> BDD-cost:    5
c ---[4691]---> BDD-cost:    5
c ---[4690]---> BDD-cost:    5
c ---[4689]---> BDD-cost:    5
c ---[4688]---> BDD-cost:    5
c ---[4687]---> BDD-cost:    5
c ---[4686]---> BDD-cost:    5
c ---[4685]---> BDD-cost:    5
c ---[4684]---> BDD-cost:    5
c ---[4683]---> BDD-cost:    5
c ---[4682]---> BDD-cost:    5
c ---[4681]---> BDD-cost:    5
c ---[4680]---> BDD-cost:    5
c ---[4679]---> BDD-cost:    5
c ---[4678]---> BDD-cost:    5
c ---[4677]---> BDD-cost:    5
c ---[4676]---> BDD-cost:    5
c ---[4675]---> BDD-cost:    5
c ---[4674]---> BDD-cost:    5
c ---[4673]---> BDD-cost:    5
c ---[4672]---> BDD-cost:    5
c ---[4671]---> BDD-cost:    5
c ---[4670]---> BDD-cost:    5
c ---[4669]---> BDD-cost:    5
c ---[4668]---> BDD-cost:    5
c ---[4667]---> BDD-cost:    5
c ---[4666]---> BDD-cost:    5
c ---[4665]---> BDD-cost:    5
c ---[4664]---> BDD-cost:    5
c ---[4663]---> BDD-cost:    5
c ---[4662]---> BDD-cost:    5
c ---[4661]---> BDD-cost:    5
c ---[4660]---> BDD-cost:    5
c ---[4659]---> BDD-cost:    5
c ---[4658]---> BDD-cost:    5
c ---[4657]---> BDD-cost:    5
c ---[4656]---> BDD-cost:    5
c ---[4655]---> BDD-cost:    5
c ---[4654]---> BDD-cost:    5
c ---[4653]---> BDD-cost:    5
c ---[4652]---> BDD-cost:    5
c ---[4651]---> BDD-cost:    5
c ---[4650]---> BDD-cost:    5
c ---[4649]---> BDD-cost:    5
c ---[4648]---> BDD-cost:    5
c ---[4647]---> BDD-cost:    5
c ---[4646]---> BDD-cost:    5
c ---[4645]---> BDD-cost:    5
c ---[4644]---> BDD-cost:    5
c ---[4643]---> BDD-cost:    5
c ---[4642]---> BDD-cost:    5
c ---[4641]---> BDD-cost:    5
c ---[4640]---> BDD-cost:    5
c ---[4639]---> BDD-cost:    5
c ---[4638]---> BDD-cost:    5
c ---[4637]---> BDD-cost:    5
c ---[4636]---> BDD-cost:    5
c ---[4635]---> BDD-cost:    5
c ---[4634]---> BDD-cost:    5
c ---[4633]---> BDD-cost:    5
c ---[4632]---> BDD-cost:    5
c ---[4631]---> BDD-cost:    5
c ---[4630]---> BDD-cost:    5
c ---[4629]---> BDD-cost:    5
c ---[4628]---> BDD-cost:    5
c ---[4627]---> BDD-cost:    5
c ---[4626]---> BDD-cost:    5
c ---[4625]---> BDD-cost:    5
c ---[4624]---> BDD-cost:    5
c ---[4623]---> BDD-cost:    5
c ---[4622]---> BDD-cost:    5
c ---[4621]---> BDD-cost:    5
c ---[4620]---> BDD-cost:    5
c ---[4619]---> BDD-cost:    5
c ---[4618]---> BDD-cost:    5
c ---[4617]---> BDD-cost:    5
c ---[4616]---> BDD-cost:    5
c ---[4615]---> BDD-cost:    5
c ---[4614]---> BDD-cost:    5
c ---[4613]---> BDD-cost:    5
c ---[4612]---> BDD-cost:    5
c ---[4611]---> BDD-cost:    5
c ---[4610]---> BDD-cost:    5
c ---[4609]---> BDD-cost:    5
c ---[4608]---> BDD-cost:    5
c ---[4607]---> BDD-cost:    5
c ---[4606]---> BDD-cost:    5
c ---[4605]---> BDD-cost:    5
c ---[4604]---> BDD-cost:    5
c ---[4603]---> BDD-cost:    5
c ---[4602]---> BDD-cost:    5
c ---[4601]---> BDD-cost:    5
c ---[4600]---> BDD-cost:    5
c ---[4599]---> BDD-cost:    5
c ---[4598]---> BDD-cost:    5
c ---[4597]---> BDD-cost:    5
c ---[4596]---> BDD-cost:    5
c ---[4451]---> BDD-cost:    2
c ---[4450]---> BDD-cost:    2
c ---[4449]---> BDD-cost:    2
c ---[4448]---> BDD-cost:    2
c ---[4447]---> BDD-cost:    2
c ---[4446]---> BDD-cost:    2
c ---[4445]---> BDD-cost:    2
c ---[4444]---> BDD-cost:    2
c ---[4443]---> BDD-cost:    2
c ---[4442]---> BDD-cost:    2
c ---[4441]---> BDD-cost:    2
c ---[4440]---> BDD-cost:    2
c ---[4439]---> BDD-cost:    2
c ---[4438]---> BDD-cost:    2
c ---[4437]---> BDD-cost:    2
c ---[4436]---> BDD-cost:    2
c ---[4435]---> BDD-cost:    2
c ---[4434]---> BDD-cost:    2
c ---[4433]---> BDD-cost:    2
c ---[4432]---> BDD-cost:    2
c ---[4431]---> BDD-cost:    2
c ---[4430]---> BDD-cost:    2
c ---[4429]---> BDD-cost:    2
c ---[4428]---> BDD-cost:    2
c ---[4427]---> BDD-cost:    2
c ---[4426]---> BDD-cost:    2
c ---[4425]---> BDD-cost:    2
c ---[4424]---> BDD-cost:    2
c ---[4423]---> BDD-cost:    2
c ---[4422]---> BDD-cost:    2
c ---[4421]---> BDD-cost:    2
c ---[4420]---> BDD-cost:    2
c ---[4419]---> BDD-cost:    2
c ---[4418]---> BDD-cost:    2
c ---[4417]---> BDD-cost:    2
c ---[4416]---> BDD-cost:    2
c ---[4415]---> BDD-cost:    2
c ---[4414]---> BDD-cost:    2
c ---[4413]---> BDD-cost:    2
c ---[4412]---> BDD-cost:    2
c ---[4411]---> BDD-cost:    2
c ---[4410]---> BDD-cost:    2
c ---[4409]---> BDD-cost:    2
c ---[4408]---> BDD-cost:    2
c ---[4407]---> BDD-cost:    2
c ---[4406]---> BDD-cost:    2
c ---[4405]---> BDD-cost:    2
c ---[4404]---> BDD-cost:    2
c ---[4403]---> BDD-cost:    2
c ---[4402]---> BDD-cost:    2
c ---[4401]---> BDD-cost:    2
c ---[4400]---> BDD-cost:    2
c ---[4399]---> BDD-cost:    2
c ---[4398]---> BDD-cost:    2
c ---[4397]---> BDD-cost:    2
c ---[4396]---> BDD-cost:    2
c ---[4395]---> BDD-cost:    2
c ---[4394]---> BDD-cost:    2
c ---[4393]---> BDD-cost:    2
c ---[4392]---> BDD-cost:    2
c ---[4391]---> BDD-cost:    2
c ---[4390]---> BDD-cost:    2
c ---[4389]---> BDD-cost:    2
c ---[4388]---> BDD-cost:    2
c ---[4387]---> BDD-cost:    2
c ---[4386]---> BDD-cost:    2
c ---[4385]---> BDD-cost:    2
c ---[4384]---> BDD-cost:    2
c ---[4383]---> BDD-cost:    2
c ---[4382]---> BDD-cost:    2
c ---[4381]---> BDD-cost:    2
c ---[4380]---> BDD-cost:    2
c ---[4379]---> BDD-cost:    2
c ---[4378]---> BDD-cost:    2
c ---[4377]---> BDD-cost:    2
c ---[4376]---> BDD-cost:    2
c ---[4375]---> BDD-cost:    2
c ---[4374]---> BDD-cost:    2
c ---[4373]---> BDD-cost:    2
c ---[4372]---> BDD-cost:    2
c ---[4371]---> BDD-cost:    2
c ---[4370]---> BDD-cost:    2
c ---[4369]---> BDD-cost:    2
c ---[4368]---> BDD-cost:    2
c ---[4367]---> BDD-cost:    2
c ---[4366]---> BDD-cost:    2
c ---[4365]---> BDD-cost:    2
c ---[4364]---> BDD-cost:    2
c ---[4363]---> BDD-cost:    2
c ---[4362]---> BDD-cost:    2
c ---[4361]---> BDD-cost:    2
c ---[4360]---> BDD-cost:    2
c ---[4359]---> BDD-cost:    2
c ---[4358]---> BDD-cost:    2
c ---[4357]---> BDD-cost:    2
c ---[4356]---> BDD-cost:    2
c ---[4355]---> BDD-cost:    2
c ---[4354]---> BDD-cost:    2
c ---[4353]---> BDD-cost:    2
c ---[4352]---> BDD-cost:    2
c ---[4351]---> BDD-cost:    2
c ---[4350]---> BDD-cost:    2
c ---[4349]---> BDD-cost:    2
c ---[4348]---> BDD-cost:    2
c ---[4347]---> BDD-cost:    2
c ---[4346]---> BDD-cost:    2
c ---[4345]---> BDD-cost:    2
c ---[4344]---> BDD-cost:    2
c ---[4343]---> BDD-cost:    2
c ---[4342]---> BDD-cost:    2
c ---[4341]---> BDD-cost:    2
c ---[4340]---> BDD-cost:    2
c ---[4339]---> BDD-cost:    2
c ---[4338]---> BDD-cost:    2
c ---[4337]---> BDD-cost:    2
c ---[4336]---> BDD-cost:    2
c ---[4335]---> BDD-cost:    2
c ---[4334]---> BDD-cost:    2
c ---[4333]---> BDD-cost:    2
c ---[4332]---> BDD-cost:    2
c ---[4331]---> BDD-cost:    2
c ---[4330]---> BDD-cost:    2
c ---[4329]---> BDD-cost:    2
c ---[4328]---> BDD-cost:    2
c ---[4327]---> BDD-cost:    2
c ---[4326]---> BDD-cost:    2
c ---[4325]---> BDD-cost:    2
c ---[4324]---> BDD-cost:    2
c ---[4323]---> BDD-cost:    2
c ---[4322]---> BDD-cost:    2
c ---[4321]---> BDD-cost:    2
c ---[4320]---> BDD-cost:    2
c ---[4319]---> BDD-cost:    2
c ---[4318]---> BDD-cost:    2
c ---[4317]---> BDD-cost:    2
c ---[4316]---> BDD-cost:    2
c ---[4315]---> BDD-cost:    2
c ---[4314]---> BDD-cost:    2
c ---[4313]---> BDD-cost:    2
c ---[4312]---> BDD-cost:    2
c ---[4311]---> BDD-cost:    2
c ---[4310]---> BDD-cost:    2
c ---[4309]---> BDD-cost:    2
c ---[4308]---> BDD-cost:    2
c ---[4307]---> BDD-cost:    3
c ---[4306]---> BDD-cost:    3
c ---[4305]---> BDD-cost:    3
c ---[4304]---> BDD-cost:    3
c ---[4303]---> BDD-cost:    3
c ---[4302]---> BDD-cost:    3
c ---[4301]---> BDD-cost:    3
c ---[4300]---> BDD-cost:    3
c ---[4299]---> BDD-cost:    3
c ---[4298]---> BDD-cost:    3
c ---[4297]---> BDD-cost:    3
c ---[4296]---> BDD-cost:    3
c ---[4295]---> BDD-cost:    3
c ---[4294]---> BDD-cost:    3
c ---[4293]---> BDD-cost:    3
c ---[4292]---> BDD-cost:    3
c ---[4291]---> BDD-cost:    3
c ---[4290]---> BDD-cost:    3
c ---[4289]---> BDD-cost:    3
c ---[4288]---> BDD-cost:    3
c ---[4287]---> BDD-cost:    3
c ---[4286]---> BDD-cost:    3
c ---[4285]---> BDD-cost:    3
c ---[4284]---> BDD-cost:    3
c ---[4283]---> BDD-cost:    3
c ---[4282]---> BDD-cost:    3
c ---[4281]---> BDD-cost:    3
c ---[4280]---> BDD-cost:    3
c ---[4279]---> BDD-cost:    3
c ---[4278]---> BDD-cost:    3
c ---[4277]---> BDD-cost:    3
c ---[4276]---> BDD-cost:    3
c ---[4275]---> BDD-cost:    3
c ---[4274]---> BDD-cost:    3
c ---[4273]---> BDD-cost:    3
c ---[4272]---> BDD-cost:    3
c ---[4271]---> BDD-cost:    3
c ---[4270]---> BDD-cost:    3
c ---[4269]---> BDD-cost:    3
c ---[4268]---> BDD-cost:    3
c ---[4267]---> BDD-cost:    3
c ---[4266]---> BDD-cost:    3
c ---[4265]---> BDD-cost:    3
c ---[4264]---> BDD-cost:    3
c ---[4263]---> BDD-cost:    3
c ---[4262]---> BDD-cost:    3
c ---[4261]---> BDD-cost:    3
c ---[4260]---> BDD-cost:    3
c ---[4259]---> BDD-cost:    3
c ---[4258]---> BDD-cost:    3
c ---[4257]---> BDD-cost:    3
c ---[4256]---> BDD-cost:    3
c ---[4255]---> BDD-cost:    3
c ---[4254]---> BDD-cost:    3
c ---[4253]---> BDD-cost:    3
c ---[4252]---> BDD-cost:    3
c ---[4251]---> BDD-cost:    3
c ---[4250]---> BDD-cost:    3
c ---[4249]---> BDD-cost:    3
c ---[4248]---> BDD-cost:    3
c ---[4247]---> BDD-cost:    3
c ---[4246]---> BDD-cost:    3
c ---[4245]---> BDD-cost:    3
c ---[4244]---> BDD-cost:    3
c ---[4243]---> BDD-cost:    3
c ---[4242]---> BDD-cost:    3
c ---[4241]---> BDD-cost:    3
c ---[4240]---> BDD-cost:    3
c ---[4239]---> BDD-cost:    3
c ---[4238]---> BDD-cost:    3
c ---[4237]---> BDD-cost:    3
c ---[4236]---> BDD-cost:    3
c ---[4235]---> BDD-cost:    3
c ---[4234]---> BDD-cost:    3
c ---[4233]---> BDD-cost:    3
c ---[4232]---> BDD-cost:    3
c ---[4231]---> BDD-cost:    3
c ---[4230]---> BDD-cost:    3
c ---[4229]---> BDD-cost:    3
c ---[4228]---> BDD-cost:    3
c ---[4227]---> BDD-cost:    3
c ---[4226]---> BDD-cost:    3
c ---[4225]---> BDD-cost:    3
c ---[4224]---> BDD-cost:    3
c ---[4223]---> BDD-cost:    3
c ---[4222]---> BDD-cost:    3
c ---[4221]---> BDD-cost:    3
c ---[4220]---> BDD-cost:    3
c ---[4219]---> BDD-cost:    3
c ---[4218]---> BDD-cost:    3
c ---[4217]---> BDD-cost:    3
c ---[4216]---> BDD-cost:    3
c ---[4215]---> BDD-cost:    3
c ---[4214]---> BDD-cost:    3
c ---[4213]---> BDD-cost:    3
c ---[4212]---> BDD-cost:    3
c ---[4211]---> BDD-cost:    3
c ---[4210]---> BDD-cost:    3
c ---[4209]---> BDD-cost:    3
c ---[4208]---> BDD-cost:    3
c ---[4207]---> BDD-cost:    3
c ---[4206]---> BDD-cost:    3
c ---[4205]---> BDD-cost:    3
c ---[4204]---> BDD-cost:    3
c ---[4203]---> BDD-cost:    3
c ---[4202]---> BDD-cost:    3
c ---[4201]---> BDD-cost:    3
c ---[4200]---> BDD-cost:    3
c ---[4199]---> BDD-cost:    3
c ---[4198]---> BDD-cost:    3
c ---[4197]---> BDD-cost:    3
c ---[4196]---> BDD-cost:    3
c ---[4195]---> BDD-cost:    3
c ---[4194]---> BDD-cost:    3
c ---[4193]---> BDD-cost:    3
c ---[4192]---> BDD-cost:    3
c ---[4191]---> BDD-cost:    3
c ---[4190]---> BDD-cost:    3
c ---[4189]---> BDD-cost:    3
c ---[4188]---> BDD-cost:    3
c ---[4187]---> BDD-cost:    3
c ---[4186]---> BDD-cost:    3
c ---[4185]---> BDD-cost:    3
c ---[4184]---> BDD-cost:    3
c ---[4183]---> BDD-cost:    3
c ---[4182]---> BDD-cost:    3
c ---[4181]---> BDD-cost:    3
c ---[4180]---> BDD-cost:    3
c ---[4179]---> BDD-cost:    3
c ---[4178]---> BDD-cost:    3
c ---[4177]---> BDD-cost:    3
c ---[4176]---> BDD-cost:    3
c ---[4175]---> BDD-cost:    3
c ---[4174]---> BDD-cost:    3
c ---[4173]---> BDD-cost:    3
c ---[4172]---> BDD-cost:    3
c ---[4171]---> BDD-cost:    3
c ---[4170]---> BDD-cost:    3
c ---[4169]---> BDD-cost:    3
c ---[4168]---> BDD-cost:    3
c ---[4167]---> BDD-cost:    3
c ---[4166]---> BDD-cost:    3
c ---[4165]---> BDD-cost:    3
c ---[4164]---> BDD-cost:    3
c ---[4163]---> BDD-cost:    4
c ---[4162]---> BDD-cost:    4
c ---[4161]---> BDD-cost:    4
c ---[4160]---> BDD-cost:    4
c ---[4159]---> BDD-cost:    4
c ---[4158]---> BDD-cost:    4
c ---[4157]---> BDD-cost:    4
c ---[4156]---> BDD-cost:    4
c ---[4155]---> BDD-cost:    4
c ---[4154]---> BDD-cost:    4
c ---[4153]---> BDD-cost:    4
c ---[4152]---> BDD-cost:    4
c ---[4151]---> BDD-cost:    4
c ---[4150]---> BDD-cost:    4
c ---[4149]---> BDD-cost:    4
c ---[4148]---> BDD-cost:    4
c ---[4147]---> BDD-cost:    4
c ---[4146]---> BDD-cost:    4
c ---[4145]---> BDD-cost:    4
c ---[4144]---> BDD-cost:    4
c ---[4143]---> BDD-cost:    4
c ---[4142]---> BDD-cost:    4
c ---[4141]---> BDD-cost:    4
c ---[4140]---> BDD-cost:    4
c ---[4139]---> BDD-cost:    4
c ---[4138]---> BDD-cost:    4
c ---[4137]---> BDD-cost:    4
c ---[4136]---> BDD-cost:    4
c ---[4135]---> BDD-cost:    4
c ---[4134]---> BDD-cost:    4
c ---[4133]---> BDD-cost:    4
c ---[4132]---> BDD-cost:    4
c ---[4131]---> BDD-cost:    4
c ---[4130]---> BDD-cost:    4
c ---[4129]---> BDD-cost:    4
c ---[4128]---> BDD-cost:    4
c ---[4127]---> BDD-cost:    4
c ---[4126]---> BDD-cost:    4
c ---[4125]---> BDD-cost:    4
c ---[4124]---> BDD-cost:    4
c ---[4123]---> BDD-cost:    4
c ---[4122]---> BDD-cost:    4
c ---[4121]---> BDD-cost:    4
c ---[4120]---> BDD-cost:    4
c ---[4119]---> BDD-cost:    4
c ---[4118]---> BDD-cost:    4
c ---[4117]---> BDD-cost:    4
c ---[4116]---> BDD-cost:    4
c ---[4115]---> BDD-cost:    4
c ---[4114]---> BDD-cost:    4
c ---[4113]---> BDD-cost:    4
c ---[4112]---> BDD-cost:    4
c ---[4111]---> BDD-cost:    4
c ---[4110]---> BDD-cost:    4
c ---[4109]---> BDD-cost:    4
c ---[4108]---> BDD-cost:    4
c ---[4107]---> BDD-cost:    4
c ---[4106]---> BDD-cost:    4
c ---[4105]---> BDD-cost:    4
c ---[4104]---> BDD-cost:    4
c ---[4103]---> BDD-cost:    4
c ---[4102]---> BDD-cost:    4
c ---[4101]---> BDD-cost:    4
c ---[4100]---> BDD-cost:    4
c ---[4099]---> BDD-cost:    4
c ---[4098]---> BDD-cost:    4
c ---[4097]---> BDD-cost:    4
c ---[4096]---> BDD-cost:    4
c ---[4095]---> BDD-cost:    4
c ---[4094]---> BDD-cost:    4
c ---[4093]---> BDD-cost:    4
c ---[4092]---> BDD-cost:    4
c ---[4091]---> BDD-cost:    4
c ---[4090]---> BDD-cost:    4
c ---[4089]---> BDD-cost:    4
c ---[4088]---> BDD-cost:    4
c ---[4087]---> BDD-cost:    4
c ---[4086]---> BDD-cost:    4
c ---[4085]---> BDD-cost:    4
c ---[4084]---> BDD-cost:    4
c ---[4083]---> BDD-cost:    4
c ---[4082]---> BDD-cost:    4
c ---[4081]---> BDD-cost:    4
c ---[4080]---> BDD-cost:    4
c ---[4079]---> BDD-cost:    4
c ---[4078]---> BDD-cost:    4
c ---[4077]---> BDD-cost:    4
c ---[4076]---> BDD-cost:    4
c ---[4075]---> BDD-cost:    4
c ---[4074]---> BDD-cost:    4
c ---[4073]---> BDD-cost:    4
c ---[4072]---> BDD-cost:    4
c ---[4071]---> BDD-cost:    4
c ---[4070]---> BDD-cost:    4
c ---[4069]---> BDD-cost:    4
c ---[4068]---> BDD-cost:    4
c ---[4067]---> BDD-cost:    4
c ---[4066]---> BDD-cost:    4
c ---[4065]---> BDD-cost:    4
c ---[4064]---> BDD-cost:    4
c ---[4063]---> BDD-cost:    4
c ---[4062]---> BDD-cost:    4
c ---[4061]---> BDD-cost:    4
c ---[4060]---> BDD-cost:    4
c ---[4059]---> BDD-cost:    4
c ---[4058]---> BDD-cost:    4
c ---[4057]---> BDD-cost:    4
c ---[4056]---> BDD-cost:    4
c ---[4055]---> BDD-cost:    4
c ---[4054]---> BDD-cost:    4
c ---[4053]---> BDD-cost:    4
c ---[4052]---> BDD-cost:    4
c ---[4051]---> BDD-cost:    4
c ---[4050]---> BDD-cost:    4
c ---[4049]---> BDD-cost:    4
c ---[4048]---> BDD-cost:    4
c ---[4047]---> BDD-cost:    4
c ---[4046]---> BDD-cost:    4
c ---[4045]---> BDD-cost:    4
c ---[4044]---> BDD-cost:    4
c ---[4043]---> BDD-cost:    4
c ---[4042]---> BDD-cost:    4
c ---[4041]---> BDD-cost:    4
c ---[4040]---> BDD-cost:    4
c ---[4039]---> BDD-cost:    4
c ---[4038]---> BDD-cost:    4
c ---[4037]---> BDD-cost:    4
c ---[4036]---> BDD-cost:    4
c ---[4035]---> BDD-cost:    4
c ---[4034]---> BDD-cost:    4
c ---[4033]---> BDD-cost:    4
c ---[4032]---> BDD-cost:    4
c ---[4031]---> BDD-cost:    4
c ---[4030]---> BDD-cost:    4
c ---[4029]---> BDD-cost:    4
c ---[4028]---> BDD-cost:    4
c ---[4027]---> BDD-cost:    4
c ---[4026]---> BDD-cost:    4
c ---[4025]---> BDD-cost:    4
c ---[4024]---> BDD-cost:    4
c ---[4023]---> BDD-cost:    4
c ---[4022]---> BDD-cost:    4
c ---[4021]---> BDD-cost:    4
c ---[4020]---> BDD-cost:    4
c ---[3875]---> BDD-cost:   19
c ---[3874]---> BDD-cost:   19
c ---[3873]---> BDD-cost:   19
c ---[3872]---> BDD-cost:   19
c ---[3871]---> BDD-cost:   19
c ---[3870]---> BDD-cost:   19
c ---[3869]---> BDD-cost:   19
c ---[3868]---> BDD-cost:   19
c ---[3867]---> BDD-cost:   19
c ---[3866]---> BDD-cost:   19
c ---[3865]---> BDD-cost:   19
c ---[3864]---> BDD-cost:   19
c ---[3863]---> BDD-cost:   19
c ---[3862]---> BDD-cost:   19
c ---[3861]---> BDD-cost:   19
c ---[3860]---> BDD-cost:   19
c ---[3859]---> BDD-cost:   19
c ---[3858]---> BDD-cost:   19
c ---[3857]---> BDD-cost:   19
c ---[3856]---> BDD-cost:   19
c ---[3855]---> BDD-cost:   19
c ---[3854]---> BDD-cost:   19
c ---[3853]---> BDD-cost:   19
c ---[3852]---> BDD-cost:   19
c ---[3851]---> BDD-cost:   19
c ---[3850]---> BDD-cost:   19
c ---[3849]---> BDD-cost:   19
c ---[3848]---> BDD-cost:   19
c ---[3847]---> BDD-cost:   19
c ---[3846]---> BDD-cost:   19
c ---[3845]---> BDD-cost:   19
c ---[3844]---> BDD-cost:   19
c ---[3843]---> BDD-cost:   19
c ---[3842]---> BDD-cost:   19
c ---[3841]---> BDD-cost:   19
c ---[3840]---> BDD-cost:   19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   66576   162310 |   19972       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21862          
c   -- var.elim.:  2000/21862          
c   -- var.elim.:  3000/21862          
c   -- var.elim.:  4000/21862          
c   -- var.elim.:  5000/21862          
c   -- var.elim.:  6000/21862          
c   -- var.elim.:  7000/21862          
c   -- var.elim.:  8000/21862          
c   -- var.elim.:  9000/21862          
c   -- var.elim.:  10000/21862          
c   -- var.elim.:  11000/21862          
c   -- var.elim.:  12000/21862          
c   -- var.elim.:  13000/21862          
c   -- var.elim.:  14000/21862          
c   -- var.elim.:  15000/21862          
c   -- var.elim.:  16000/21862          
c   -- var.elim.:  17000/21862          
c   -- var.elim.:  18000/21862          
c   -- var.elim.:  19000/21862          
c   -- var.elim.:  20000/21862          
c   -- var.elim.:  21000/21862          
c   -- var.elim.:  21862/21862          
c   -- var.elim.:  1000/11152          
c   -- var.elim.:  2000/11152          
c   -- var.elim.:  3000/11152          
c   -- var.elim.:  4000/11152          
c   -- var.elim.:  5000/11152          
c   -- var.elim.:  6000/11152          
c   -- var.elim.:  7000/11152          
c   -- var.elim.:  8000/11152          
c   -- var.elim.:  9000/11152          
c   -- var.elim.:  10000/11152          
c   -- var.elim.:  11000/11152          
c   -- var.elim.:  11152/11152          
c   -- var.elim.:  194/194          
c   -- subsuming                       
c   -- var.elim.:  1000/3714          
c   -- var.elim.:  2000/3714          
c   -- var.elim.:  3000/3714          
c   -- var.elim.:  3714/3714          
c   -- var.elim.:  1000/2448          
c   -- var.elim.:  2000/2448          
c   -- var.elim.:  2448/2448          
c   -- subsuming                       
c   -- var.elim.:  356/356          
c   -- var.elim.:  144/144          
c   -- subsuming                       
c   -- var.elim.:  144/144          
c   -- var.elim.:  204/204          
c   -- var.elim.:  203/203          
c   -- var.elim.:  120/120          
c   -- subsuming                       
c   -- var.elim.:  144/144          
c   -- var.elim.:  144/144          
c |         0 |   55061   163570 |      --       0       --      -- |     --   | -11161/3852
c |         0 |   55061   163570 |   22024       0        0     nan |  0.000 % |
c |       101 |   54682   162141 |   24060      80      419     5.2 | 12.193 % |
c |       251 |   53930   159503 |   26102     164      904     5.5 | 13.009 % |
c |       476 |   52537   154525 |   27970     267     1346     5.0 | 14.437 % |
c |       813 |   50901   148794 |   29809     447     2145     4.8 | 16.126 % |
c |      1319 |   48294   139838 |   31111     757     3806     5.0 | 18.898 % |
c |      2078 |   45486   130375 |   32232    1282     6806     5.3 | 22.050 % |
c |      3217 |   41220   115916 |   32130    2048    11451     5.6 | 26.757 % |
c |      4925 |   35510    96979 |   30447    3058    18262     6.0 | 33.505 % |
c ==============================================================================
c (current CPU-time: 7.10092 s)
c ==============================================================================
c [1mFound solution: 47[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10236     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5918 |   43997   113858 |   13199    3752    22457     6.0 | 33.505 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12783          
c   -- var.elim.:  2000/12783          
c   -- var.elim.:  3000/12783          
c   -- var.elim.:  4000/12783          
c   -- var.elim.:  5000/12783          
c   -- var.elim.:  6000/12783          
c   -- var.elim.:  7000/12783          
c   -- var.elim.:  8000/12783          
c   -- var.elim.:  9000/12783          
c   -- var.elim.:  10000/12783          
c   -- var.elim.:  11000/12783          
c   -- var.elim.:  12000/12783          
c   -- var.elim.:  12783/12783          
c   -- var.elim.:  1000/7431          
c   -- var.elim.:  2000/7431          
c   -- var.elim.:  3000/7431          
c   -- var.elim.:  4000/7431          
c   -- var.elim.:  5000/7431          
c   -- var.elim.:  6000/7431          
c   -- var.elim.:  7000/7431          
c   -- var.elim.:  7431/7431          
c   -- var.elim.:  929/929          
c   -- var.elim.:  95/95          
c   -- var.elim.:  95/95          
c   -- subsuming                       
c   -- var.elim.:  1000/4378          
c   -- var.elim.:  2000/4378          
c   -- var.elim.:  3000/4378          
c   -- var.elim.:  4000/4378          
c   -- var.elim.:  4378/4378          
c   -- var.elim.:  1000/1121          
c   -- var.elim.:  1121/1121          
c   -- var.elim.:  1000/1325          
c   -- var.elim.:  1325/1325          
c   -- var.elim.:  1000/1772          
c   -- var.elim.:  1772/1772          
c   -- var.elim.:  1000/1518          
c   -- var.elim.:  1518/1518          
c   -- var.elim.:  1000/1471          
c   -- var.elim.:  1471/1471          
c   -- var.elim.:  1000/1135          
c   -- var.elim.:  1135/1135          
c   -- subsuming                       
c   -- var.elim.:  1000/2107          
c   -- var.elim.:  2000/2107          
c   -- var.elim.:  2107/2107          
c   -- var.elim.:  363/363          
c   -- var.elim.:  12/12          
c   -- var.elim.:  6/6          
c   -- subsuming                       
c   -- var.elim.:  277/277          
c   -- var.elim.:  170/170          
c   -- subsuming                       
c   -- var.elim.:  207/207          
c   -- var.elim.:  10/10          
c |      5918 |   36756   134145 |      --    3752       --      -- |     --   | -7241/20288
c |      5918 |   36756   134145 |   14702    3752    22457     6.0 | 33.505 % |
c |      6018 |   36360   132760 |   15998    1273     4294     3.4 | 34.046 % |
c |      6168 |   35932   131230 |   17391    1381     4857     3.5 | 34.395 % |
c |      6393 |   35293   128985 |   18789    1528     5687     3.7 | 34.959 % |
c |      6730 |   34366   125709 |   20126    1794     7032     3.9 | 35.834 % |
c |      7236 |   33380   122310 |   21503    2145     9029     4.2 | 36.735 % |
c ==============================================================================
c (current CPU-time: 26.8119 s)
c ==============================================================================
c [1mFound solution: 43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7586 |   32959   120762 |    9887    2417    10821     4.5 | 36.735 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1988          
c   -- var.elim.:  1988/1988          
c   -- var.elim.:  1000/1477          
c   -- var.elim.:  1477/1477          
c   -- var.elim.:  287/287          
c   -- var.elim.:  62/62          
c   -- var.elim.:  40/40          
c   -- subsuming                       
c   -- var.elim.:  550/550          
c   -- var.elim.:  180/180          
c   -- subsuming                       
c   -- var.elim.:  122/122          
c   -- var.elim.:  95/95          
c |      7586 |   32099   120139 |      --    2417       --      -- |     --   | -860/-622
c |      7586 |   32099   120139 |   12839    1815     7128     3.9 | 36.735 % |
c |      7687 |   31751   118886 |   13970    1909     7634     4.0 | 38.820 % |
c |      7837 |   31566   118232 |   15277    2029     8357     4.1 | 39.009 % |
c |      8062 |   31289   117293 |   16658    2189     9341     4.3 | 39.238 % |
c |      8399 |   31217   117026 |   18281    2520    12779     5.1 | 39.309 % |
c |      8905 |   31133   116579 |   20056    3019    23823     7.9 | 39.460 % |
c ==============================================================================
c (current CPU-time: 29.7185 s)
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9227 |   31192   116621 |    9357    3316    27198     8.2 | 39.460 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2389          
c   -- var.elim.:  2000/2389          
c   -- var.elim.:  2389/2389          
c   -- var.elim.:  735/735          
c   -- var.elim.:  33/33          
c   -- var.elim.:  22/22          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  354/354          
c   -- var.elim.:  73/73          
c |      9227 |   30851   116530 |      --    3316       --      -- |     --   | -338/-84
c |      9227 |   30851   116530 |   12340    2944    20025     6.8 | 39.460 % |
c |      9327 |   30851   116530 |   13574    3044    20974     6.9 | 39.954 % |
c ==============================================================================
c (current CPU-time: 31.9431 s)
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9448 |   30945   116753 |    9283    3164    23826     7.5 | 39.954 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2186          
c   -- var.elim.:  2000/2186          
c   -- var.elim.:  2186/2186          
c   -- var.elim.:  1000/2097          
c   -- var.elim.:  2000/2097          
c   -- var.elim.:  2097/2097          
c   -- var.elim.:  1000/1329          
c   -- var.elim.:  1329/1329          
c   -- var.elim.:  635/635          
c   -- var.elim.:  128/128          
c   -- subsuming                       
c   -- var.elim.:  1000/1485          
c   -- var.elim.:  1485/1485          
c   -- var.elim.:  10/10          
c |      9448 |   30318   111425 |      --    3164       --      -- |     --   | -280/4960
c |      9448 |   30318   111425 |   12127    3006    15340     5.1 | 39.954 % |
c |      9549 |   30295   111298 |   13329    3106    19796     6.4 | 41.090 % |
c |      9700 |   30295   111298 |   14662    3257    23478     7.2 | 41.090 % |
c |      9927 |   30295   111298 |   16129    3484    29922     8.6 | 41.090 % |
c |     10266 |   30293   111287 |   17740    3818    38043    10.0 | 41.097 % |
c |     10772 |   30268   111161 |   19498    4312    52488    12.2 | 41.117 % |
c |     11532 |   30266   111151 |   21447    5071    80375    15.8 | 41.124 % |
c |     12672 |   30266   111151 |   23591    6211   123470    19.9 | 41.124 % |
c |     14381 |   30220   110995 |   25911    7908   190280    24.1 | 41.170 % |
c ==============================================================================
c (current CPU-time: 48.1257 s)
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14413 |   30272   111118 |    9081    7940   191239    24.1 | 41.170 % |
c   -- subsuming                       
c   -- var.elim.:  299/299          
c   -- var.elim.:  74/74          
c   -- var.elim.:  8/8          
c |     14413 |   30224   111066 |      --    7940       --      -- |     --   | -48/-51
c |     14413 |   30224   111066 |   12089    7929   191079    24.1 | 41.170 % |
c |     14514 |   30224   111066 |   13298    8030   193987    24.2 | 41.205 % |
c |     14665 |   30224   111066 |   14628    8181   197114    24.1 | 41.205 % |
c |     14892 |   30224   111066 |   16091    8408   205286    24.4 | 41.205 % |
c |     15230 |   30224   111066 |   17700    8746   217030    24.8 | 41.205 % |
c ==============================================================================
c (current CPU-time: 50.3673 s)
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15310 |   30240   111104 |    9071    8826   219634    24.9 | 41.205 % |
c   -- subsuming                       
c   -- var.elim.:  142/142          
c   -- var.elim.:  887/887          
c |     15310 |   30205   110953 |      --    8826       --      -- |     --   | -13/-8
c |     15310 |   30205   110953 |   12082    8643   210219    24.3 | 41.205 % |
c |     15410 |   30205   110953 |   13290    8743   213621    24.4 | 41.241 % |
c ==============================================================================
c (current CPU-time: 52.2741 s)
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15476 |   33553   120452 |   10065    8809   215266    24.4 | 41.241 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5745          
c   -- var.elim.:  2000/5745          
c   -- var.elim.:  3000/5745          
c   -- var.elim.:  4000/5745          
c   -- var.elim.:  5000/5745          
c   -- var.elim.:  5745/5745          
c   -- var.elim.:  1000/2898          
c   -- var.elim.:  2000/2898          
c   -- var.elim.:  2898/2898          
c   -- var.elim.:  1000/1885          
c   -- var.elim.:  1885/1885          
c   -- var.elim.:  1000/1318          
c   -- var.elim.:  1318/1318          
c   -- subsuming                       
c   -- var.elim.:  1000/2211          
c   -- var.elim.:  2000/2211          
c   -- var.elim.:  2211/2211          
c   -- var.elim.:  1000/1248          
c   -- var.elim.:  1248/1248          
c   -- var.elim.:  1000/1437          
c   -- var.elim.:  1437/1437          
c   -- var.elim.:  1000/1312          
c   -- var.elim.:  1312/1312          
c |     15476 |   30262   114501 |      --    8809       --      -- |     --   | -3291/-5950
c |     15476 |   30262   114501 |   12104    8809   215266    24.4 | 41.241 % |
c |     15577 |   30237   114408 |   13304    8909   218894    24.6 | 41.190 % |
c |     15729 |   30237   114408 |   14634    9061   224880    24.8 | 41.190 % |
c |     15954 |   30237   114408 |   16098    9286   232245    25.0 | 41.190 % |
c |     16294 |   30237   114408 |   17707    9626   243646    25.3 | 41.190 % |
c ==============================================================================
c (current CPU-time: 68.1836 s)
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16355 |   30256   114454 |    9076    9687   245694    25.4 | 41.190 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1379          
c   -- var.elim.:  1379/1379          
c   -- var.elim.:  399/399          
c |     16355 |   30153   111624 |      --    9687       --      -- |     --   | -44/-2252
c |     16355 |   30153   111624 |   12061    8752   194435    22.2 | 41.190 % |
c |     16455 |   30153   111624 |   13267    8852   198056    22.4 | 41.316 % |
c |     16607 |   30132   111524 |   14583    9000   203334    22.6 | 41.363 % |
c |     16833 |   30116   111456 |   16033    9225   211114    22.9 | 41.369 % |
c |     17170 |   30116   111456 |   17637    9562   222061    23.2 | 41.369 % |
c |     17676 |   30116   111456 |   19400   10068   240419    23.9 | 41.369 % |
c |     18435 |   30106   111423 |   21333   10825   271341    25.1 | 41.383 % |
c ==============================================================================
c (current CPU-time: 75.8315 s)
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     18778 |   30142   111393 |    9042   11166   282063    25.3 | 41.383 % |
c   -- subsuming                       
c   -- var.elim.:  632/632          
c   -- var.elim.:  74/74          
c   -- var.elim.:  8/8          
c |     18778 |   30095   111007 |      --   11166       --      -- |     --   | -47/-385
c |     18778 |   30095   111007 |   12038    8494   166778    19.6 | 41.383 % |
c |     18878 |   30095   111007 |   13241    8594   169420    19.7 | 41.485 % |
c |     19029 |   30080   110953 |   14558    8743   174858    20.0 | 41.499 % |
c |     19254 |   30080   110953 |   16014    8968   181799    20.3 | 41.499 % |
c |     19591 |   30080   110953 |   17616    9305   191285    20.6 | 41.499 % |
c |     20098 |   30080   110953 |   19377    9812   206873    21.1 | 41.499 % |
c |     20857 |   30080   110953 |   21315   10571   228978    21.7 | 41.499 % |
c |     21996 |   30080   110953 |   23446   11710   262455    22.4 | 41.499 % |
c |     23704 |   30059   110882 |   25773   13413   317400    23.7 | 41.519 % |
c |     26266 |   30032   110795 |   28325   15972   391454    24.5 | 41.539 % |
c |     30110 |   29633   109399 |   30744    9473   155048    16.4 | 42.024 % |
c ==============================================================================
c [1mOptimal solution: 19[0m
s OPTIMUM FOUND
v C1825_bit0 -C1826_bit0 -C1827_bit0 -C1828_bit0 -C1829_bit0 -C1830_bit0 -C1831_bit0 -C1832_bit0 -C1833_bit0 -C1834_bit0 -C1835_bit0 -C1836_bit0 -C1837_bit0 -C1838_bit0 -C1839_bit0 -C1840_bit0 -C1841_bit0 -C1842_bit0 -C1843_bit0 -C1844_bit0 -C1845_bit0 -C1846_bit0 -C1847_bit0 -C1848_bit0 -C1849_bit0 -C1850_bit0 -C1851_bit0 -C1852_bit0 -C1853_bit0 -C1854_bit0 -C1855_bit0 -C1856_bit0 -C1857_bit0 C1858_bit0 -C1859_bit0 -C1860_bit0 -C1861_bit0 -C1862_bit0 -C1863_bit0 -C1864_bit0 -C1865_bit0 -C1866_bit0 -C1867_bit0 -C1868_bit0 -C1869_bit0 -C1870_bit0 -C1871_bit0 -C1872_bit0 -C1873_bit0 C1874_bit0 -C1875_bit0 -C1876_bit0 -C1877_bit0 -C1878_bit0 -C1879_bit0 -C1880_bit0 -C1881_bit0 -C1882_bit0 -C1883_bit0 -C1884_bit0 -C1885_bit0 -C1886_bit0 -C1887_bit0 -C1888_bit0 -C1889_bit0 -C1890_bit0 -C1891_bit0 -C1892_bit0 -C1893_bit0 -C1894_bit0 C1895_bit0 -C1896_bit0 -C1897_bit0 -C1898_bit0 -C1899_bit0 -C1900_bit0 C1901_bit0 -C1902_bit0 -C1903_bit0 -C1904_bit0 -C1905_bit0 -C1906_bit0 -C1907_bit0 C1908_bit0 -C1909_bit0 -C1910_bit0 -C1911_bit0 -C1912_bit0 -C1913_bit0 -C1914_bit0 -C1915_bit0 -C1916_bit0 -C1917_bit0 -C1918_bit0 -C1919_bit0 -C1920_bit0 C1921_bit0 -C1922_bit0 -C1923_bit0 -C1924_bit0 -C1925_bit0 -C1926_bit0 -C1927_bit0 -C1928_bit0 -C1929_bit0 -C1930_bit0 -C1931_bit0 -C1932_bit0 -C1933_bit0 -C1934_bit0 C1935_bit0 -C1936_bit0 -C1937_bit0 -C1938_bit0 -C1939_bit0 -C1940_bit0 -C1941_bit0 -C1942_bit0 -C1943_bit0 -C1944_bit0 -C1945_bit0 -C1946_bit0 -C1947_bit0 -C1948_bit0 -C1949_bit0 -C1950_bit0 -C1951_bit0 -C1952_bit0 -C1953_bit0 -C1954_bit0 -C1955_bit0 -C1956_bit0 -C1957_bit0 -C1958_bit0 -C1959_bit0 -C1960_bit0 -C1961_bit0 -C1962_bit0 -C1963_bit0 -C1964_bit0 -C1965_bit0 -C1966_bit0 -C1967_bit0 C1968_bit0 C1969_bit0 -C1970_bit0 -C1971_bit0 -C1972_bit0 -C1973_bit0 -C1974_bit0 -C1975_bit0 -C1976_bit0 -C1977_bit0 -C1978_bit0 -C1979_bit0 -C1980_bit0 -C1981_bit0 C1982_bit0 -C1983_bit0 -C1984_bit0 -C1985_bit0 C1986_bit0 -C1987_bit0 -C1988_bit0 -C1989_bit0 -C1990_bit0 -C1991_bit0 -C1992_bit0 -C1993_bit0 -C1994_bit0 -C1995_bit0 -C1996_bit0 -C1997_bit0 -C1998_bit0 -C1999_bit0 C2000_bit0 C2001_bit0 C2002_bit0 -C2003_bit0 -C2004_bit0 -C2005_bit0 -C2006_bit0 -C2007_bit0 -C2008_bit0 -C2009_bit0 -C2010_bit0 -C2011_bit0 -C2012_bit0 -C2013_bit0 -C2014_bit0 C2015_bit0 -C2016_bit0 -C2017_bit0 -C2018_bit0 -C2019_bit0 -C2020_bit0 -C2021_bit0 -C2022_bit0 -C2023_bit0 -C2024_bit0 -C2025_bit0 -C2026_bit0 -C2027_bit0 -C2028_bit0 -C2029_bit0 -C2030_bit0 -C2031_bit0 -C2032_bit0 C2033_bit0 -C2034_bit0 -C2035_bit0 -C2036_bit0 -C2037_bit0 -C2038_bit0 -C2039_bit0 -C2040_bit0 -C2041_bit0 -C2042_bit0 -C2043_bit0 -C2044_bit0 -C2045_bit0 -C2046_bit0 -C2047_bit0 -C2048_bit0 -C2049_bit0 -C2050_bit0 -C2051_bit0 -C2052_bit0 -C2053_bit0 -C2054_bit0 -C2055_bit0 -C2056_bit0 C2057_bit0 -C2058_bit0 -C2059_bit0 -C2060_bit0 -C2061_bit0 -C2062_bit0 -C2063_bit0 -C2064_bit0 -C2065_bit0 -C2066_bit0 -C2067_bit0 -C2068_bit0 -C2069_bit0 -C2070_bit0 -C2071_bit0 -C2072_bit0 -C2073_bit0 -C2074_bit0 -C2075_bit0 -C2076_bit0 -C2077_bit0 -C2078_bit0 -C2079_bit0 -C2080_bit0 -C2081_bit0 -C2082_bit0 -C2083_bit0 -C2084_bit0 -C2085_bit0 -C2086_bit0 -C2087_bit0 -C2088_bit0 -C2089_bit0 -C2090_bit0 -C2091_bit0 -C2092_bit0 -C2093_bit0 -C2094_bit0 -C2095_bit0 -C2096_bit0 -C2097_bit0 -C2098_bit0 -C2099_bit0 -C2100_bit0 -C2101_bit0 -C2102_bit0 -C2103_bit0 -C2104_bit0 C2105_bit0 -C2106_bit0 -C2107_bit0 -C2108_bit0 -C2109_bit0 -C2110_bit0 -C2111_bit0 -C2112_bit0 C0001_bit0 -C0002_bit0 -C0003_bit0 -C0004_bit0 -C0005_bit0 -C0006_bit0 -C0007_bit0 -C0008_bit0 -C0009_bit0 -C0010_bit0 -C0011_bit0 -C0012_bit0 -C0013_bit0 -C0014_bit0 -C0015_bit0 -C0016_bit0 -C0017_bit0 -C0018_bit0 -C0019_bit0 -C0020_bit0 -C0021_bit0 -C0022_bit0 -C0023_bit0 -C0024_bit0 -C0025_bit0 -C0026_bit0 -C0027_bit0 -C0028_bit0 -C0029_bit0 -C0030_bit0 -C0031_bit0 -C0032_bit0 -C0033_bit0 -C0034_bit0 -C0035_bit0 -C0036_bit0 -C0037_bit0 -C0038_bit0 -C0039_bit0 -C0040_bit0 -C0041_bit0 -C0042_bit0 -C0043_bit0 -C0044_bit0 -C0045_bit0 -C0046_bit0 -C0047_bit0 -C0048_bit0 -C0049_bit0 -C0050_bit0 -C0051_bit0 -C0052_bit0 -C0053_bit0 -C0054_bit0 -C0055_bit0 -C0056_bit0 -C0057_bit0 -C0058_bit0 -C0059_bit0 -C0060_bit0 -C0061_bit0 -C0062_bit0 -C0063_bit0 -C0064_bit0 -C0065_bit0 -C0066_bit0 -C0067_bit0 -C0068_bit0 -C0069_bit0 -C0070_bit0 -C0071_bit0 -C0072_bit0 -C0073_bit0 -C0074_bit0 -C0075_bit0 -C0076_bit0 -C0077_bit0 -C0078_bit0 -C0079_bit0 -C0080_bit0 -C0081_bit0 -C0082_bit0 -C0083_bit0 -C0084_bit0 -C0085_bit0 -C0086_bit0 -C0087_bit0 -C0088_bit0 -C0089_bit0 -C0090_bit0 -C0091_bit0 -C0092_bit0 -C0093_bit0 -C0094_bit0 -C0095_bit0 -C0096_bit0 -C0097_bit0 -C0098_bit0 -C0099_bit0 -C0100_bit0 -C0101_bit0 -C0102_bit0 -C0103_bit0 -C0104_bit0 -C0105_bit0 -C0106_bit0 -C0107_bit0 -C0108_bit0 -C0109_bit0 -C0110_bit0 -C0111_bit0 -C0112_bit0 -C0113_bit0 -C0114_bit0 -C0115_bit0 -C0116_bit0 -C0117_bit0 -C0118_bit0 -C0119_bit0 -C0120_bit0 -C0121_bit0 -C0122_bit0 -C0123_bit0 -C0124_bit0 -C0125_bit0 -C0126_bit0 -C0127_bit0 -C0128_bit0 -C0129_bit0 -C0130_bit0 -C0131_bit0 -C0132_bit0 -C0133_bit0 -C0134_bit0 -C0135_bit0 -C0136_bit0 -C0137_bit0 -C0138_bit0 -C0139_bit0 -C0140_bit0 -C0141_bit0 -C0142_bit0 -C0143_bit0 -C0144_bit0 -C0145_bit0 -C0146_bit0 -C0147_bit0 -C0148_bit0 -C0149_bit0 -C0150_bit0 -C0151_bit0 -C0152_bit0 -C0153_bit0 -C0154_bit0 -C0155_bit0 -C0156_bit0 -C0157_bit0 -C0158_bit0 -C0159_bit0 -C0160_bit0 -C0161_bit0 -C0162_bit0 -C0163_bit0 -C0164_bit0 -C0165_bit0 C0166_bit0 -C0167_bit0 C0168_bit0 -C0169_bit0 -C0170_bit0 -C0171_bit0 -C0172_bit0 -C0173_bit0 -C0174_bit0 -C0175_bit0 -C0176_bit0 -C0177_bit0 -C0178_bit0 -C0179_bit0 -C0180_bit0 -C0181_bit0 -C0182_bit0 -C0183_bit0 -C0184_bit0 -C0185_bit0 -C0186_bit0 -C0187_bit0 -C0188_bit0 -C0189_bit0 -C0190_bit0 -C0191_bit0 -C0192_bit0 -C0193_bit0 -C0194_bit0 -C0195_bit0 -C0196_bit0 -C0197_bit0 -C0198_bit0 -C0199_bit0 -C0200_bit0 -C0201_bit0 -C0202_bit0 -C0203_bit0 -C0204_bit0 -C0205_bit0 -C0206_bit0 -C0207_bit0 -C0208_bit0 -C0209_bit0 -C0210_bit0 -C0211_bit0 -C0212_bit0 -C0213_bit0 -C0214_bit0 -C0215_bit0 -C0216_bit0 -C0217_bit0 -C0218_bit0 -C0219_bit0 -C0220_bit0 -C0221_bit0 -C0222_bit0 -C0223_bit0 -C0224_bit0 -C0225_bit0 -C0226_bit0 -C0227_bit0 -C0228_bit0 -C0229_bit0 -C0230_bit0 -C0231_bit0 -C0232_bit0 -C0233_bit0 -C0234_bit0 -C0235_bit0 -C0236_bit0 -C0237_bit0 -C0238_bit0 -C0239_bit0 -C0240_bit0 -C0241_bit0 -C0242_bit0 -C0243_bit0 -C0244_bit0 -C0245_bit0 -C0246_bit0 -C0247_bit0 -C0248_bit0 C0249_bit0 C0250_bit0 -C0251_bit0 -C0252_bit0 -C0253_bit0 -C0254_bit0 -C0255_bit0 -C0256_bit0 -C0257_bit0 -C0258_bit0 -C0259_bit0 -C0260_bit0 -C0261_bit0 -C0262_bit0 -C0263_bit0 -C0264_bit0 -C0265_bit0 -C0266_bit0 -C0267_bit0 -C0268_bit0 -C0269_bit0 -C0270_bit0 -C0271_bit0 -C0272_bit0 -C0273_bit0 -C0274_bit0 -C0275_bit0 -C0276_bit0 -C0277_bit0 -C0278_bit0 -C0279_bit0 -C0280_bit0 -C0281_bit0 -C0282_bit0 -C0283_bit0 -C0284_bit0 -C0285_bit0 -C0286_bit0 -C0287_bit0 -C0288_bit0 -C0289_bit0 -C0290_bit0 -C0291_bit0 -C0292_bit0 -C0293_bit0 -C0294_bit0 -C0295_bit0 -C0296_bit0 -C0297_bit0 -C0298_bit0 -C0299_bit0 -C0300_bit0 -C0301_bit0 -C0302_bit0 -C0303_bit0 -C0304_bit0 -C0305_bit0 -C0306_bit0 -C0307_bit0 -C0308_bit0 -C0309_bit0 -C0310_bit0 -C0311_bit0 -C0312_bit0 -C0313_bit0 -C0314_bit0 -C0315_bit0 -C0316_bit0 -C0317_bit0 -C0318_bit0 -C0319_bit0 -C0320_bit0 -C0321_bit0 -C0322_bit0 -C0323_bit0 -C0324_bit0 -C0325_bit0 -C0326_bit0 -C0327_bit0 -C0328_bit0 -C0329_bit0 -C0330_bit0 -C0331_bit0 -C0332_bit0 -C0333_bit0 -C0334_bit0 -C0335_bit0 -C0336_bit0 -C0337_bit0 -C0338_bit0 -C0339_bit0 -C0340_bit0 -C0341_bit0 -C0342_bit0 -C0343_bit0 -C0344_bit0 -C0345_bit0 -C0346_bit0 -C0347_bit0 -C0348_bit0 -C0349_bit0 -C0350_bit0 -C0351_bit0 C0352_bit0 -C0353_bit0 C0354_bit0 -C0355_bit0 -C0356_bit0 -C0357_bit0 -C0358_bit0 -C0359_bit0 -C0360_bit0 -C0361_bit0 -C0362_bit0 -C0363_bit0 -C0364_bit0 -C0365_bit0 -C0366_bit0 -C0367_bit0 -C0368_bit0 -C0369_bit0 -C0370_bit0 -C0371_bit0 -C0372_bit0 -C0373_bit0 -C0374_bit0 -C0375_bit0 -C0376_bit0 -C0377_bit0 -C0378_bit0 -C0379_bit0 -C0380_bit0 -C0381_bit0 C0382_bit0 -C0383_bit0 -C0384_bit0 -C0385_bit0 -C0386_bit0 -C0387_bit0 -C0388_bit0 -C0389_bit0 -C0390_bit0 -C0391_bit0 -C0392_bit0 -C0393_bit0 -C0394_bit0 -C0395_bit0 -C0396_bit0 -C0397_bit0 -C0398_bit0 -C0399_bit0 -C0400_bit0 -C0401_bit0 -C0402_bit0 -C0403_bit0 -C0404_bit0 -C0405_bit0 -C0406_bit0 -C0407_bit0 -C0408_bit0 -C0409_bit0 -C0410_bit0 -C0411_bit0 -C0412_bit0 -C0413_bit0 -C0414_bit0 -C0415_bit0 -C0416_bit0 C0417_bit0 -C0418_bit0 -C0419_bit0 -C0420_bit0 -C0421_bit0 -C0422_bit0 -C0423_bit0 -C0424_bit0 -C0425_bit0 -C0426_bit0 -C0427_bit0 -C0428_bit0 -C0429_bit0 -C0430_bit0 -C0431_bit0 -C0432_bit0 -C0433_bit0 -C0434_bit0 -C0435_bit0 -C0436_bit0 -C0437_bit0 -C0438_bit0 -C0439_bit0 -C0440_bit0 -C0441_bit0 -C0442_bit0 -C0443_bit0 -C0444_bit0 -C0445_bit0 -C0446_bit0 -C0447_bit0 -C0448_bit0 -C0449_bit0 -C0450_bit0 -C0451_bit0 -C0452_bit0 -C0453_bit0 -C0454_bit0 -C0455_bit0 -C0456_bit0 -C0457_bit0 -C0458_bit0 -C0459_bit0 -C0460_bit0 -C0461_bit0 -C0462_bit0 -C0463_bit0 -C0464_bit0 -C0465_bit0 -C0466_bit0 -C0467_bit0 -C0468_bit0 -C0469_bit0 -C0470_bit0 -C0471_bit0 -C0472_bit0 -C0473_bit0 -C0474_bit0 -C0475_bit0 -C0476_bit0 -C0477_bit0 -C0478_bit0 -C0479_bit0 -C0480_bit0 C0481_bit0 -C0482_bit0 C0483_bit0 C0484_bit0 -C0485_bit0 -C0486_bit0 -C0487_bit0 -C0488_bit0 -C0489_bit0 -C0490_bit0 -C0491_bit0 -C0492_bit0 -C0493_bit0 -C0494_bit0 -C0495_bit0 -C0496_bit0 -C0497_bit0 -C0498_bit0 -C0499_bit0 -C0500_bit0 -C0501_bit0 -C0502_bit0 -C0503_bit0 -C0504_bit0 -C0505_bit0 -C0506_bit0 -C0507_bit0 -C0508_bit0 -C0509_bit0 -C0510_bit0 -C0511_bit0 -C0512_bit0 -C0513_bit0 -C0514_bit0 -C0515_bit0 -C0516_bit0 -C0517_bit0 -C0518_bit0 -C0519_bit0 -C0520_bit0 -C0521_bit0 -C0522_bit0 -C0523_bit0 -C0524_bit0 -C0525_bit0 -C0526_bit0 -C0527_bit0 -C0528_bit0 -C0529_bit0 -C0530_bit0 -C0531_bit0 -C0532_bit0 -C0533_bit0 -C0534_bit0 -C0535_bit0 -C0536_bit0 -C0537_bit0 -C0538_bit0 -C0539_bit0 -C0540_bit0 -C0541_bit0 -C0542_bit0 -C0543_bit0 -C0544_bit0 -C0545_bit0 -C0546_bit0 -C0547_bit0 -C0548_bit0 -C0549_bit0 -C0550_bit0 -C0551_bit0 C0552_bit0 -C0553_bit0 -C0554_bit0 -C0555_bit0 -C0556_bit0 -C0557_bit0 -C0558_bit0 -C0559_bit0 -C0560_bit0 -C0561_bit0 -C0562_bit0 -C0563_bit0 -C0564_bit0 -C0565_bit0 -C0566_bit0 -C0567_bit0 -C0568_bit0 -C0569_bit0 -C0570_bit0 -C0571_bit0 -C0572_bit0 -C0573_bit0 -C0574_bit0 -C0575_bit0 -C0576_bit0 -C0577_bit0 -C0578_bit0 -C0579_bit0 -C0580_bit0 -C0581_bit0 -C0582_bit0 -C0583_bit0 -C0584_bit0 -C0585_bit0 -C0586_bit0 -C0587_bit0 -C0588_bit0 -C0589_bit0 -C0590_bit0 -C0591_bit0 -C0592_bit0 -C0593_bit0 -C0594_bit0 -C0595_bit0 -C0596_bit0 -C0597_bit0 -C0598_bit0 -C0599_bit0 -C0600_bit0 -C0601_bit0 -C0602_bit0 -C0603_bit0 -C0604_bit0 -C0605_bit0 -C0606_bit0 -C0607_bit0 -C0608_bit0 -C0609_bit0 -C0610_bit0 -C0611_bit0 -C0612_bit0 -C0613_bit0 -C0614_bit0 -C0615_bit0 -C0616_bit0 -C0617_bit0 -C0618_bit0 -C0619_bit0 -C0620_bit0 -C0621_bit0 -C0622_bit0 -C0623_bit0 -C0624_bit0 -C0625_bit0 -C0626_bit0 -C0627_bit0 -C0628_bit0 -C0629_bit0 -C0630_bit0 -C0631_bit0 -C0632_bit0 -C0633_bit0 -C0634_bit0 -C0635_bit0 -C0636_bit0 -C0637_bit0 -C0638_bit0 -C0639_bit0 -C0640_bit0 -C0641_bit0 -C0642_bit0 -C0643_bit0 -C0644_bit0 -C0645_bit0 -C0646_bit0 -C0647_bit0 -C0648_bit0 -C0649_bit0 -C0650_bit0 -C0651_bit0 -C0652_bit0 -C0653_bit0 -C0654_bit0 -C0655_bit0 -C0656_bit0 -C0657_bit0 -C0658_bit0 -C0659_bit0 -C0660_bit0 -C0661_bit0 -C0662_bit0 -C0663_bit0 -C0664_bit0 -C0665_bit0 -C0666_bit0 -C0667_bit0 -C0668_bit0 -C0669_bit0 -C0670_bit0 -C0671_bit0 -C0672_bit0 -C0673_bit0 -C0674_bit0 -C0675_bit0 -C0676_bit0 -C0677_bit0 -C0678_bit0 -C0679_bit0 -C0680_bit0 -C0681_bit0 -C0682_bit0 -C0683_bit0 -C0684_bit0 -C0685_bit0 -C0686_bit0 -C0687_bit0 -C0688_bit0 -C0689_bit0 -C0690_bit0 -C0691_bit0 -C0692_bit0 -C0693_bit0 -C0694_bit0 -C0695_bit0 -C0696_bit0 -C0697_bit0 -C0698_bit0 -C0699_bit0 -C0700_bit0 -C0701_bit0 -C0702_bit0 -C0703_bit0 -C0704_bit0 -C0705_bit0 -C0706_bit0 -C0707_bit0 -C0708_bit0 -C0709_bit0 -C0710_bit0 -C0711_bit0 -C0712_bit0 -C0713_bit0 -C0714_bit0 -C0715_bit0 -C0716_bit0 -C0717_bit0 C0718_bit0 C0719_bit0 -C0720_bit0 -C0721_bit0 C0722_bit0 -C0723_bit0 -C0724_bit0 -C0725_bit0 -C0726_bit0 -C0727_bit0 -C0728_bit0 -C0729_bit0 -C0730_bit0 -C0731_bit0 -C0732_bit0 -C0733_bit0 -C0734_bit0 -C0735_bit0 -C0736_bit0 -C0737_bit0 -C0738_bit0 -C0739_bit0 -C0740_bit0 -C0741_bit0 -C0742_bit0 -C0743_bit0 -C0744_bit0 -C0745_bit0 -C0746_bit0 -C0747_bit0 -C0748_bit0 -C0749_bit0 -C0750_bit0 -C0751_bit0 -C0752_bit0 -C0753_bit0 -C0754_bit0 -C0755_bit0 -C0756_bit0 -C0757_bit0 -C0758_bit0 -C0759_bit0 -C0760_bit0 -C0761_bit0 -C0762_bit0 -C0763_bit0 -C0764_bit0 -C0765_bit0 -C0766_bit0 -C0767_bit0 -C0768_bit0 -C0769_bit0 -C0770_bit0 -C0771_bit0 -C0772_bit0 -C0773_bit0 -C0774_bit0 -C0775_bit0 -C0776_bit0 -C0777_bit0 -C0778_bit0 -C0779_bit0 -C0780_bit0 -C0781_bit0 -C0782_bit0 -C0783_bit0 -C0784_bit0 -C0785_bit0 C0786_bit0 -C0787_bit0 C0788_bit0 C0789_bit0 -C0790_bit0 -C0791_bit0 -C0792_bit0 -C0793_bit0 -C0794_bit0 -C0795_bit0 -C0796_bit0 -C0797_bit0 -C0798_bit0 -C0799_bit0 -C0800_bit0 -C0801_bit0 -C0802_bit0 -C0803_bit0 -C0804_bit0 -C0805_bit0 -C0806_bit0 -C0807_bit0 C0808_bit0 C0809_bit0 -C0810_bit0 -C0811_bit0 -C0812_bit0 -C0813_bit0 -C0814_bit0 -C0815_bit0 -C0816_bit0 -C0817_bit0 -C0818_bit0 -C0819_bit0 -C0820_bit0 -C0821_bit0 -C0822_bit0 -C0823_bit0 -C0824_bit0 -C0825_bit0 -C0826_bit0 -C0827_bit0 -C0828_bit0 -C0829_bit0 -C0830_bit0 -C0831_bit0 -C0832_bit0 -C0833_bit0 -C0834_bit0 -C0835_bit0 -C0836_bit0 -C0837_bit0 -C0838_bit0 -C0839_bit0 -C0840_bit0 -C0841_bit0 -C0842_bit0 -C0843_bit0 -C0844_bit0 -C0845_bit0 -C0846_bit0 -C0847_bit0 -C0848_bit0 -C0849_bit0 -C0850_bit0 -C0851_bit0 -C0852_bit0 -C0853_bit0 -C0854_bit0 -C0855_bit0 -C0856_bit0 -C0857_bit0 -C0858_bit0 -C0859_bit0 -C0860_bit0 -C0861_bit0 -C0862_bit0 -C0863_bit0 -C0864_bit0 -C0865_bit0 -C0866_bit0 -C0867_bit0 -C0868_bit0 -C0869_bit0 -C0870_bit0 -C0871_bit0 -C0872_bit0 -C0873_bit0 -C0874_bit0 -C0875_bit0 -C0876_bit0 C0877_bit0 -C0878_bit0 -C0879_bit0 -C0880_bit0 -C0881_bit0 C0882_bit0 -C0883_bit0 -C0884_bit0 -C0885_bit0 -C0886_bit0 -C0887_bit0 -C0888_bit0 -C0889_bit0 C0890_bit0 -C0891_bit0 -C0892_bit0 -C0893_bit0 -C0894_bit0 -C0895_bit0 -C0896_bit0 -C0897_bit0 -C0898_bit0 -C0899_bit0 -C0900_bit0 -C0901_bit0 -C0902_bit0 -C0903_bit0 -C0904_bit0 -C0905_bit0 -C0906_bit0 -C0907_bit0 -C0908_bit0 -C0909_bit0 -C0910_bit0 -C0911_bit0 -C0912_bit0 -C0913_bit0 -C0914_bit0 -C0915_bit0 -C0916_bit0 -C0917_bit0 -C0918_bit0 -C0919_bit0 -C0920_bit0 -C0921_bit0 -C0922_bit0 -C0923_bit0 -C0924_bit0 -C0925_bit0 -C0926_bit0 -C0927_bit0 -C0928_bit0 -C0929_bit0 -C0930_bit0 -C0931_bit0 -C0932_bit0 -C0933_bit0 -C0934_bit0 -C0935_bit0 -C0936_bit0 -C0937_bit0 -C0938_bit0 -C0939_bit0 -C0940_bit0 -C0941_bit0 -C0942_bit0 -C0943_bit0 -C0944_bit0 -C0945_bit0 -C0946_bit0 -C0947_bit0 -C0948_bit0 -C0949_bit0 -C0950_bit0 -C0951_bit0 -C0952_bit0 -C0953_bit0 C0954_bit0 C0955_bit0 -C0956_bit0 -C0957_bit0 -C0958_bit0 -C0959_bit0 -C0960_bit0 -C0961_bit0 -C0962_bit0 -C0963_bit0 -C0964_bit0 -C0965_bit0 -C0966_bit0 -C0967_bit0 -C0968_bit0 -C0969_bit0 -C0970_bit0 -C0971_bit0 -C0972_bit0 -C0973_bit0 -C0974_bit0 -C0975_bit0 -C0976_bit0 -C0977_bit0 -C0978_bit0 -C0979_bit0 -C0980_bit0 -C0981_bit0 -C0982_bit0 -C0983_bit0 -C0984_bit0 -C0985_bit0 -C0986_bit0 -C0987_bit0 -C0988_bit0 -C0989_bit0 -C0990_bit0 -C0991_bit0 -C0992_bit0 -C0993_bit0 -C0994_bit0 -C0995_bit0 -C0996_bit0 -C0997_bit0 -C0998_bit0 -C0999_bit0 -C1000_bit0 -C1001_bit0 -C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 -C1006_bit0 -C1007_bit0 -C1008_bit0 -C1009_bit0 -C1010_bit0 -C1011_bit0 -C1012_bit0 -C1013_bit0 -C1014_bit0 -C1015_bit0 -C1016_bit0 -C1017_bit0 -C1018_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 -C1022_bit0 -C1023_bit0 -C1024_bit0 -C1025_bit0 -C1026_bit0 -C1027_bit0 -C1028_bit0 -C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 -C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 -C1038_bit0 -C1039_bit0 -C1040_bit0 -C1041_bit0 -C1042_bit0 -C1043_bit0 -C1044_bit0 C1045_bit0 -C1046_bit0 -C1047_bit0 -C1048_bit0 -C1049_bit0 -C1050_bit0 -C1051_bit0 -C1052_bit0 -C1053_bit0 -C1054_bit0 -C1055_bit0 -C1056_bit0 -C1057_bit0 -C1058_bit0 -C1059_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 -C1063_bit0 -C1064_bit0 -C1065_bit0 -C1066_bit0 -C1067_bit0 -C1068_bit0 -C1069_bit0 -C1070_bit0 -C1071_bit0 -C1072_bit0 -C1073_bit0 -C1074_bit0 -C1075_bit0 -C1076_bit0 -C1077_bit0 -C1078_bit0 -C1079_bit0 -C1080_bit0 -C1081_bit0 -C1082_bit0 -C1083_bit0 -C1084_bit0 -C1085_bit0 -C1086_bit0 -C1087_bit0 -C1088_bit0 -C1089_bit0 -C1090_bit0 -C1091_bit0 -C1092_bit0 -C1093_bit0 -C1094_bit0 -C1095_bit0 -C1096_bit0 -C1097_bit0 -C1098_bit0 -C1099_bit0 -C1100_bit0 -C1101_bit0 -C1102_bit0 -C1103_bit0 -C1104_bit0 -C1105_bit0 -C1106_bit0 -C1107_bit0 -C1108_bit0 -C1109_bit0 -C1110_bit0 -C1111_bit0 -C1112_bit0 -C1113_bit0 -C1114_bit0 -C1115_bit0 -C1116_bit0 -C1117_bit0 -C1118_bit0 -C1119_bit0 -C1120_bit0 -C1121_bit0 -C1122_bit0 -C1123_bit0 -C1124_bit0 -C1125_bit0 -C1126_bit0 -C1127_bit0 -C1128_bit0 -C1129_bit0 -C1130_bit0 -C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1135_bit0 -C1136_bit0 -C1137_bit0 -C1138_bit0 -C1139_bit0 -C1140_bit0 -C1141_bit0 -C1142_bit0 -C1143_bit0 -C1144_bit0 -C1145_bit0 -C1146_bit0 -C1147_bit0 -C1148_bit0 -C1149_bit0 -C1150_bit0 -C1151_bit0 -C1152_bit0 -C1153_bit0 -C1154_bit0 -C1155_bit0 -C1156_bit0 -C1157_bit0 -C1158_bit0 -C1159_bit0 -C1160_bit0 C1161_bit0 -C1162_bit0 C1163_bit0 C1164_bit0 -C1165_bit0 -C1166_bit0 -C1167_bit0 -C1168_bit0 -C1169_bit0 -C1170_bit0 -C1171_bit0 -C1172_bit0 -C1173_bit0 -C1174_bit0 -C1175_bit0 -C1176_bit0 -C1177_bit0 -C1178_bit0 -C1179_bit0 -C1180_bit0 -C1181_bit0 -C1182_bit0 -C1183_bit0 -C1184_bit0 -C1185_bit0 -C1186_bit0 -C1187_bit0 -C1188_bit0 -C1189_bit0 -C1190_bit0 -C1191_bit0 -C1192_bit0 -C1193_bit0 -C1194_bit0 -C1195_bit0 -C1196_bit0 -C1197_bit0 -C1198_bit0 -C1199_bit0 -C1200_bit0 -C1201_bit0 -C1202_bit0 -C1203_bit0 -C1204_bit0 -C1205_bit0 -C1206_bit0 -C1207_bit0 -C1208_bit0 -C1209_bit0 -C1210_bit0 -C1211_bit0 -C1212_bit0 -C1213_bit0 -C1214_bit0 -C1215_bit0 -C1216_bit0 -C1217_bit0 -C1218_bit0 -C1219_bit0 -C1220_bit0 -C1221_bit0 -C1222_bit0 -C1223_bit0 -C1224_bit0 -C1225_bit0 -C1226_bit0 -C1227_bit0 -C1228_bit0 -C1229_bit0 -C1230_bit0 -C1231_bit0 -C1232_bit0 -C1233_bit0 -C1234_bit0 -C1235_bit0 -C1236_bit0 -C1237_bit0 -C1238_bit0 -C1239_bit0 -C1240_bit0 -C1241_bit0 -C1242_bit0 -C1243_bit0 -C1244_bit0 -C1245_bit0 -C1246_bit0 -C1247_bit0 -C1248_bit0 -C1249_bit0 -C1250_bit0 -C1251_bit0 -C1252_bit0 -C1253_bit0 -C1254_bit0 -C1255_bit0 -C1256_bit0 -C1257_bit0 -C1258_bit0 -C1259_bit0 -C1260_bit0 -C1261_bit0 -C1262_bit0 -C1263_bit0 -C1264_bit0 -C1265_bit0 -C1266_bit0 -C1267_bit0 -C1268_bit0 -C1269_bit0 -C1270_bit0 -C1271_bit0 -C1272_bit0 -C1273_bit0 -C1274_bit0 -C1275_bit0 -C1276_bit0 -C1277_bit0 -C1278_bit0 -C1279_bit0 -C1280_bit0 -C1281_bit0 -C1282_bit0 -C1283_bit0 -C1284_bit0 -C1285_bit0 -C1286_bit0 -C1287_bit0 -C1288_bit0 -C1289_bit0 -C1290_bit0 -C1291_bit0 -C1292_bit0 -C1293_bit0 -C1294_bit0 -C1295_bit0 -C1296_bit0 -C1297_bit0 -C1298_bit0 -C1299_bit0 -C1300_bit0 -C1301_bit0 -C1302_bit0 -C1303_bit0 -C1304_bit0 -C1305_bit0 -C1306_bit0 -C1307_bit0 -C1308_bit0 -C1309_bit0 -C1310_bit0 -C1311_bit0 -C1312_bit0 -C1313_bit0 -C1314_bit0 -C1315_bit0 -C1316_bit0 -C1317_bit0 -C1318_bit0 -C1319_bit0 -C1320_bit0 -C1321_bit0 -C1322_bit0 -C1323_bit0 -C1324_bit0 -C1325_bit0 -C1326_bit0 -C1327_bit0 -C1328_bit0 -C1329_bit0 -C1330_bit0 -C1331_bit0 -C1332_bit0 -C1333_bit0 -C1334_bit0 -C1335_bit0 -C1336_bit0 -C1337_bit0 -C1338_bit0 -C1339_bit0 -C1340_bit0 -C1341_bit0 -C1342_bit0 -C1343_bit0 -C1344_bit0 -C1345_bit0 -C1346_bit0 -C1347_bit0 -C1348_bit0 -C1349_bit0 -C1350_bit0 -C1351_bit0 -C1352_bit0 -C1353_bit0 -C1354_bit0 -C1355_bit0 -C1356_bit0 -C1357_bit0 -C1358_bit0 -C1359_bit0 -C1360_bit0 -C1361_bit0 -C1362_bit0 -C1363_bit0 -C1364_bit0 -C1365_bit0 -C1366_bit0 -C1367_bit0 -C1368_bit0 -C1369_bit0 -C1370_bit0 -C1371_bit0 -C1372_bit0 -C1373_bit0 -C1374_bit0 -C1375_bit0 -C1376_bit0 -C1377_bit0 -C1378_bit0 -C1379_bit0 -C1380_bit0 -C1381_bit0 -C1382_bit0 -C1383_bit0 -C1384_bit0 -C1385_bit0 -C1386_bit0 -C1387_bit0 -C1388_bit0 -C1389_bit0 -C1390_bit0 -C1391_bit0 -C1392_bit0 -C1393_bit0 -C1394_bit0 -C1395_bit0 -C1396_bit0 -C1397_bit0 -C1398_bit0 -C1399_bit0 -C1400_bit0 C1401_bit0 -C1402_bit0 -C1403_bit0 -C1404_bit0 -C1405_bit0 -C1406_bit0 -C1407_bit0 -C1408_bit0 -C1409_bit0 -C1410_bit0 -C1411_bit0 -C1412_bit0 -C1413_bit0 -C1414_bit0 -C1415_bit0 -C1416_bit0 -C1417_bit0 -C1418_bit0 -C1419_bit0 -C1420_bit0 -C1421_bit0 -C1422_bit0 -C1423_bit0 -C1424_bit0 -C1425_bit0 -C1426_bit0 -C1427_bit0 -C1428_bit0 -C1429_bit0 -C1430_bit0 -C1431_bit0 -C1432_bit0 -C1433_bit0 -C1434_bit0 -C1435_bit0 -C1436_bit0 -C1437_bit0 -C1438_bit0 -C1439_bit0 -C1440_bit0 C1441_bit0 C1442_bit0 -C1443_bit0 -C1444_bit0 C1445_bit0 -C1446_bit0 -C1447_bit0 -C1448_bit0 -C1449_bit0 -C1450_bit0 -C1451_bit0 -C1452_bit0 -C1453_bit0 C1454_bit0 -C1455_bit0 -C1456_bit0 -C1457_bit0 -C1458_bit0 -C1459_bit0 -C1460_bit0 -C1461_bit0 -C1462_bit0 -C1463_bit0 -C1464_bit0 -C1465_bit0 -C1466_bit0 -C1467_bit0 -C1468_bit0 -C1469_bit0 -C1470_bit0 -C1471_bit0 C1472_bit0 C1473_bit0 -C1474_bit0 -C1475_bit0 -C1476_bit0 -C1477_bit0 -C1478_bit0 -C1479_bit0 -C1480_bit0 -C1481_bit0 -C1482_bit0 -C1483_bit0 -C1484_bit0 -C1485_bit0 -C1486_bit0 -C1487_bit0 -C1488_bit0 -C1489_bit0 -C1490_bit0 -C1491_bit0 -C1492_bit0 C1493_bit0 -C1494_bit0 -C1495_bit0 -C1496_bit0 -C1497_bit0 -C1498_bit0 -C1499_bit0 -C1500_bit0 -C1501_bit0 -C1502_bit0 -C1503_bit0 -C1504_bit0 C1505_bit0 -C1506_bit0 -C1507_bit0 -C1508_bit0 -C1509_bit0 -C1510_bit0 -C1511_bit0 -C1512_bit0 -C1513_bit0 -C1514_bit0 -C1515_bit0 -C1516_bit0 C1517_bit0 -C1518_bit0 -C1519_bit0 -C1520_bit0 -C1521_bit0 -C1522_bit0 -C1523_bit0 -C1524_bit0 -C1525_bit0 -C1526_bit0 -C1527_bit0 -C1528_bit0 -C1529_bit0 C1530_bit0 -C1531_bit0 -C1532_bit0 C1533_bit0 C1534_bit0 -C1535_bit0 -C1536_bit0 -C1537_bit0 -C1538_bit0 -C1539_bit0 -C1540_bit0 -C1541_bit0 -C1542_bit0 -C1543_bit0 -C1544_bit0 -C1545_bit0 -C1546_bit0 -C1547_bit0 -C1548_bit0 -C1549_bit0 C1550_bit0 -C1551_bit0 -C1552_bit0 -C1553_bit0 -C1554_bit0 -C1555_bit0 -C1556_bit0 -C1557_bit0 -C1558_bit0 -C1559_bit0 -C1560_bit0 -C1561_bit0 C1562_bit0 -C1563_bit0 -C1564_bit0 -C1565_bit0 C1566_bit0 C1567_bit0 -C1568_bit0 -C1569_bit0 C1570_bit0 -C1571_bit0 -C1572_bit0 -C1573_bit0 C1574_bit0 -C1575_bit0 -C1576_bit0 -C1577_bit0 -C1578_bit0 -C1579_bit0 -C1580_bit0 -C1581_bit0 -C1582_bit0 -C1583_bit0 -C1584_bit0 -C1585_bit0 -C1586_bit0 -C1587_bit0 -C1588_bit0 -C1589_bit0 -C1590_bit0 -C1591_bit0 -C1592_bit0 -C1593_bit0 -C1594_bit0 -C1595_bit0 -C1596_bit0 -C1597_bit0 -C1598_bit0 -C1599_bit0 C1600_bit0 -C1601_bit0 -C1602_bit0 -C1603_bit0 -C1604_bit0 -C1605_bit0 -C1606_bit0 -C1607_bit0 -C1608_bit0 -C1609_bit0 C1610_bit0 -C1611_bit0 -C1612_bit0 -C1613_bit0 -C1614_bit0 -C1615_bit0 -C1616_bit0 -C1617_bit0 -C1618_bit0 -C1619_bit0 -C1620_bit0 -C1621_bit0 -C1622_bit0 -C1623_bit0 -C1624_bit0 -C1625_bit0 -C1626_bit0 C1627_bit0 -C1628_bit0 C1629_bit0 -C1630_bit0 C1631_bit0 -C1632_bit0 -C1633_bit0 -C1634_bit0 -C1635_bit0 -C1636_bit0 -C1637_bit0 -C1638_bit0 -C1639_bit0 -C1640_bit0 C1641_bit0 -C1642_bit0 -C1643_bit0 -C1644_bit0 C1645_bit0 -C1646_bit0 -C1647_bit0 -C1648_bit0 C1649_bit0 -C1650_bit0 -C1651_bit0 C1652_bit0 -C1653_bit0 -C1654_bit0 C1655_bit0 C1656_bit0 -C1657_bit0 -C1658_bit0 -C1659_bit0 C1660_bit0 -C1661_bit0 -C1662_bit0 -C1663_bit0 C1664_bit0 -C1665_bit0 -C1666_bit0 -C1667_bit0 -C1668_bit0 -C1669_bit0 -C1670_bit0 -C1671_bit0 -C1672_bit0 -C1673_bit0 -C1674_bit0 -C1675_bit0 -C1676_bit0 -C1677_bit0 -C1678_bit0 -C1679_bit0 -C1680_bit0 -C1681_bit0 -C1682_bit0 -C1683_bit0 -C1684_bit0 -C1685_bit0 -C1686_bit0 -C1687_bit0 -C1688_bit0 C1689_bit0 -C1690_bit0 -C1691_bit0 -C1692_bit0 C1693_bit0 -C1694_bit0 -C1695_bit0 -C1696_bit0 C1697_bit0 -C1698_bit0 -C1699_bit0 -C1700_bit0 C1701_bit0 -C1702_bit0 -C1703_bit0 C1704_bit0 -C1705_bit0 -C1706_bit0 -C1707_bit0 -C1708_bit0 -C1709_bit0 -C1710_bit0 -C1711_bit0 -C1712_bit0 -C1713_bit0 -C1714_bit0 -C1715_bit0 -C1716_bit0 -C1717_bit0 -C1718_bit0 -C1719_bit0 -C1720_bit0 -C1721_bit0 -C1722_bit0 -C1723_bit0 -C1724_bit0 -C1725_bit0 -C1726_bit0 C1727_bit0 -C1728_bit0 -C1729_bit0 -C1730_bit0 C1731_bit0 -C1732_bit0 -C1733_bit0 -C1734_bit0 C1735_bit0 -C1736_bit0 -C1737_bit0 -C1738_bit0 -C1739_bit0 -C1740_bit0 -C1741_bit0 -C1742_bit0 -C1743_bit0 -C1744_bit0 -C1745_bit0 -C1746_bit0 -C1747_bit0 -C1748_bit0 -C1749_bit0 -C1750_bit0 C1751_bit0 -C1752_bit0 -C1753_bit0 -C1754_bit0 -C1755_bit0 -C1756_bit0 -C1757_bit0 -C1758_bit0 -C1759_bit0 -C1760_bit0 -C1761_bit0 -C1762_bit0 -C1763_bit0 -C1764_bit0 -C1765_bit0 -C1766_bit0 -C1767_bit0 C1768_bit0 -C1769_bit0 -C1770_bit0 -C1771_bit0 -C1772_bit0 -C1773_bit0 -C1774_bit0 C1775_bit0 -C1776_bit0 -C1777_bit0 -C1778_bit0 -C1779_bit0 -C1780_bit0 -C1781_bit0 -C1782_bit0 -C1783_bit0 -C1784_bit0 -C1785_bit0 -C1786_bit0 -C1787_bit0 -C1788_bit0 -C1789_bit0 -C1790_bit0 -C1791_bit0 C1792_bit0 -C1793_bit0 -C1794_bit0 -C1795_bit0 -C1796_bit0 -C1797_bit0 -C1798_bit0 C1799_bit0 -C1800_bit0 -C1801_bit0 -C1802_bit0 -C1803_bit0 -C1804_bit0 -C1805_bit0 -C1806_bit0 -C1807_bit0 -C1808_bit0 -C1809_bit0 -C1810_bit0 -C1811_bit0 -C1812_bit0 -C1813_bit0 -C1814_bit0 -C1815_bit0 -C1816_bit0 -C1817_bit0 -C1818_bit0 -C1819_bit0 C1820_bit0 -C1821_bit0 -C1822_bit0 -C1823_bit0 C1824_bit0
c _______________________________________________________________________________
c 
c restarts              : 62
c conflicts             : 32452          (306 /sec)
c decisions             : 156833         (1478 /sec)
c propagations          : 25455428       (239816 /sec)
c inspects              : 71430414       (672946 /sec)
c CPU time              : 106.146 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.58 0.78 0.84 2/55 18820
Raw data (stat): 18820 (runsolver) R 18819 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540197776 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.64 0.79 0.84 2/55 18820
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 5772 0 0 0 980 19 0 0 25 0 1 0 540197776 20865024 4312 4294967295 134512640 134672761 3221224544 3221222720 134604069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5094 4312 603 41 0 5053 0
vsize: 20376
[startup+20.0017 s]
Raw data (loadavg): 0.70 0.79 0.84 2/55 18820
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 5937 0 0 0 1977 22 0 0 25 0 1 0 540197776 20971520 4338 4294967295 134512640 134672761 3221224544 3221222992 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5120 4338 603 41 0 5079 0
vsize: 20480
[startup+30.0019 s]
Raw data (loadavg): 0.74 0.80 0.84 2/55 18820
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 7269 0 0 0 2972 27 0 0 25 0 1 0 540197776 21524480 4449 4294967295 134512640 134672761 3221224544 3221222960 134608993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5255 4449 603 41 0 5214 0
vsize: 21020
[startup+40.0024 s]
Raw data (loadavg): 0.78 0.80 0.84 2/55 18820
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 8549 0 0 0 3964 34 0 0 25 0 1 0 540197776 23334912 4872 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5697 4872 603 41 0 5656 0
vsize: 22788
[startup+50.0021 s]
Raw data (loadavg): 0.81 0.81 0.84 2/55 18820
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 9075 0 0 0 4963 36 0 0 25 0 1 0 540197776 23846912 4968 4294967295 134512640 134672761 3221224544 3221223744 134610683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 4968 603 41 0 5781 0
vsize: 23288
[startup+60.0031 s]
Raw data (loadavg): 0.84 0.82 0.85 2/55 18822
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 10237 0 0 0 5954 44 0 0 25 0 1 0 540197776 26116096 5117 4294967295 134512640 134672761 3221224544 3221222992 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6376 5117 603 41 0 6335 0
vsize: 25504
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.84 0.85 2/55 18822
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 11347 0 0 0 6948 50 0 0 25 0 1 0 540197776 24854528 4843 4294967295 134512640 134672761 3221224544 3221223036 134541792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6068 4843 603 41 0 6027 0
vsize: 24272
[startup+80.0113 s]
Raw data (loadavg): 0.95 0.84 0.85 2/55 18822
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 12771 0 0 0 7944 55 0 0 25 0 1 0 540197776 24895488 4853 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6078 4853 603 41 0 6037 0
vsize: 24312
[startup+90.0119 s]
Raw data (loadavg): 0.96 0.85 0.85 2/55 18822
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 12799 0 0 0 8944 55 0 0 25 0 1 0 540197776 25026560 4881 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6110 4881 603 41 0 6069 0
vsize: 24440
[startup+100.013 s]
Raw data (loadavg): 0.97 0.85 0.85 2/55 18822
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 12870 0 0 0 9944 56 0 0 25 0 1 0 540197776 25489408 4952 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6223 4952 603 41 0 6182 0
vsize: 24892
[startup+106.771 s]
Raw data (loadavg): 0.97 0.86 0.86 1/54 18822
Raw data (stat): 18820 (minisat+) R 18819 20838 20837 0 -1 0 12870 0 0 0 9944 56 0 0 25 0 1 0 540197776 25489408 4952 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6223 4952 603 41 0 6182 0
vsize: 0

Child status: 30
Real time (s): 106.77
CPU time (s): 106.745
CPU user time (s): 106.165
CPU system time (s): 0.579911
CPU usage (%): 99.9761
Max. virtual memory (Kb): 25504
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	19
#### END VERIFIER DATA ####