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 32463

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-05-27 10:15:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23868 boxname=wulflinc1 idbench=1512 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3fce91583b30a82646d8d8e778b97a89  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-neos1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-neos1.opb
IDLAUNCH: 23868
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        863700 kB
Buffers:          2084 kB
Cached:         145220 kB
SwapCached:        732 kB
Active:          17052 kB
Inactive:       132524 kB
HighTotal:      131008 kB
HighFree:        13104 kB
LowTotal:       903652 kB
LowFree:        850596 kB
SwapTotal:     2097136 kB
SwapFree:      2095340 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            15436 kB
Committed_AS:    92720 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 10:24:46 (client local time) WITH STATUS 30 IN 544.399 SECONDS
stats: 23868 0 544.399 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]---> BDD-cost:  285
c ---[5116]---> BDD-cost:  165
c ---[5114]---> BDD-cost:  165
c ---[5112]---> BDD-cost:  285
c ---[5110]---> BDD-cost:  285
c ---[5108]---> BDD-cost:  285
c ---[5106]---> BDD-cost:  165
c ---[5104]---> BDD-cost:  165
c ---[5102]---> BDD-cost:  285
c ---[5100]---> BDD-cost:  285
c ---[5098]---> BDD-cost:  285
c ---[5096]---> BDD-cost:  165
c ---[5094]---> BDD-cost:  165
c ---[5092]---> BDD-cost:  165
c ---[5090]---> BDD-cost:  285
c ---[5088]---> BDD-cost:  285
c ---[5086]---> BDD-cost:  165
c ---[5084]---> BDD-cost:  165
c ---[5082]---> BDD-cost:  165
c ---[5080]---> BDD-cost:  285
c ---[5078]---> BDD-cost:  154
c ---[5076]---> BDD-cost:  286
c ---[5074]---> BDD-cost:  286
c ---[5072]---> BDD-cost:  166
c ---[5070]---> BDD-cost:  166
c ---[5068]---> BDD-cost:  286
c ---[5066]---> BDD-cost:  286
c ---[5064]---> BDD-cost:  166
c ---[5062]---> BDD-cost:  286
c ---[5060]---> BDD-cost:  154
c ---[5058]---> BDD-cost:  286
c ---[5056]---> BDD-cost:  286
c ---[5054]---> BDD-cost:  286
c ---[5052]---> BDD-cost:  286
c ---[5050]---> BDD-cost:  166
c ---[5048]---> BDD-cost:  286
c ---[5046]---> BDD-cost:  274
c ---[5044]---> BDD-cost:  286
c ---[5042]---> BDD-cost:  286
c ---[5040]---> BDD-cost:  166
c ---[5038]---> BDD-cost:  166
c ---[5036]---> BDD-cost:  286
c ---[5034]---> BDD-cost:  286
c ---[5032]---> BDD-cost:  286
c ---[5030]---> BDD-cost:  286
c ---[5028]---> BDD-cost:  154
c ---[5026]---> BDD-cost:  286
c ---[5024]---> BDD-cost:  166
c ---[5022]---> BDD-cost:  166
c ---[5020]---> BDD-cost:  286
c ---[5018]---> BDD-cost:  286
c ---[5016]---> BDD-cost:  286
c ---[5014]---> BDD-cost:  286
c ---[5012]---> BDD-cost:  154
c ---[5010]---> BDD-cost:  286
c ---[5008]---> BDD-cost:  166
c ---[5006]---> BDD-cost:  166
c ---[5004]---> BDD-cost:  286
c ---[5002]---> BDD-cost:  166
c ---[5000]---> BDD-cost:  286
c ---[4998]---> BDD-cost:  154
c ---[4996]---> BDD-cost:  286
c ---[4994]---> BDD-cost:  286
c ---[4992]---> BDD-cost:  166
c ---[4990]---> BDD-cost:  166
c ---[4988]---> BDD-cost:  286
c ---[4986]---> BDD-cost:  286
c ---[4984]---> BDD-cost:  166
c ---[4982]---> BDD-cost:  286
c ---[4980]---> BDD-cost:  154
c ---[4978]---> BDD-cost:  286
c ---[4976]---> BDD-cost:  286
c ---[4974]---> BDD-cost:  286
c ---[4972]---> BDD-cost:  286
c ---[4970]---> BDD-cost:  166
c ---[4968]---> BDD-cost:  286
c ---[4966]---> BDD-cost:  274
c ---[4964]---> BDD-cost:  286
c ---[4962]---> BDD-cost:  286
c ---[4960]---> BDD-cost:  166
c ---[4958]---> BDD-cost:  166
c ---[4956]---> BDD-cost:  286
c ---[4954]---> BDD-cost:  286
c ---[4952]---> BDD-cost:  286
c ---[4950]---> BDD-cost:  286
c ---[4948]---> BDD-cost:  154
c ---[4946]---> BDD-cost:  286
c ---[4944]---> BDD-cost:  166
c ---[4942]---> BDD-cost:  166
c ---[4940]---> BDD-cost:  286
c ---[4938]---> BDD-cost:  286
c ---[4936]---> BDD-cost:  286
c ---[4934]---> BDD-cost:  286
c ---[4932]---> BDD-cost:  154
c ---[4930]---> BDD-cost:  286
c ---[4928]---> BDD-cost:  166
c ---[4926]---> BDD-cost:  166
c ---[4924]---> BDD-cost:  286
c ---[4922]---> BDD-cost:  166
c ---[4920]---> BDD-cost:  286
c ---[4919]---> BDD-cost:   25
c ---[4918]---> BDD-cost:   25
c ---[4917]---> BDD-cost:   25
c ---[4916]---> BDD-cost:   25
c ---[4915]---> BDD-cost:   25
c ---[4914]---> BDD-cost:   25
c ---[4913]---> BDD-cost:   25
c ---[4912]---> BDD-cost:   25
c ---[4911]---> BDD-cost:   25
c ---[4910]---> BDD-cost:   25
c ---[4909]---> BDD-cost:   25
c ---[4908]---> BDD-cost:   25
c ---[4907]---> BDD-cost:   25
c ---[4906]---> BDD-cost:   25
c ---[4905]---> BDD-cost:   25
c ---[4904]---> BDD-cost:   25
c ---[4903]---> BDD-cost:   25
c ---[4902]---> BDD-cost:   25
c ---[4901]---> BDD-cost:   25
c ---[4900]---> BDD-cost:   25
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:   25
c ---[4878]---> BDD-cost:   25
c ---[4877]---> BDD-cost:   25
c ---[4876]---> BDD-cost:   25
c ---[4875]---> BDD-cost:   25
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:   29
c ---[4868]---> BDD-cost:   29
c ---[4867]---> BDD-cost:   29
c ---[4866]---> BDD-cost:   29
c ---[4865]---> BDD-cost:   29
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:   25
c ---[4858]---> BDD-cost:   25
c ---[4857]---> BDD-cost:   25
c ---[4856]---> BDD-cost:   25
c ---[4855]---> BDD-cost:   25
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:   29
c ---[4848]---> BDD-cost:   29
c ---[4847]---> BDD-cost:   29
c ---[4846]---> BDD-cost:   29
c ---[4845]---> BDD-cost:   29
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:   29
c ---[4838]---> BDD-cost:   29
c ---[4837]---> BDD-cost:   29
c ---[4836]---> BDD-cost:   29
c ---[4835]---> BDD-cost:   29
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:   29
c ---[4828]---> BDD-cost:   29
c ---[4827]---> BDD-cost:   29
c ---[4826]---> BDD-cost:   29
c ---[4825]---> BDD-cost:   29
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:   25
c ---[4818]---> BDD-cost:   25
c ---[4817]---> BDD-cost:   25
c ---[4816]---> BDD-cost:   25
c ---[4815]---> BDD-cost:   25
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:   25
c ---[4808]---> BDD-cost:   25
c ---[4807]---> BDD-cost:   25
c ---[4806]---> BDD-cost:   25
c ---[4805]---> BDD-cost:   25
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:   25
c ---[4798]---> BDD-cost:   25
c ---[4797]---> BDD-cost:   25
c ---[4796]---> BDD-cost:   25
c ---[4795]---> BDD-cost:   25
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:   29
c ---[4788]---> BDD-cost:   29
c ---[4787]---> BDD-cost:   29
c ---[4786]---> BDD-cost:   29
c ---[4785]---> BDD-cost:   29
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:   29
c ---[4778]---> BDD-cost:   29
c ---[4777]---> BDD-cost:   29
c ---[4776]---> BDD-cost:   29
c ---[4775]---> BDD-cost:   29
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:   29
c ---[4768]---> BDD-cost:   29
c ---[4767]---> BDD-cost:   29
c ---[4766]---> BDD-cost:   29
c ---[4765]---> BDD-cost:   29
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:   29
c ---[4758]---> BDD-cost:   29
c ---[4757]---> BDD-cost:   29
c ---[4756]---> BDD-cost:   29
c ---[4755]---> BDD-cost:   29
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:   29
c ---[4748]---> BDD-cost:   29
c ---[4747]---> BDD-cost:   29
c ---[4746]---> BDD-cost:   29
c ---[4745]---> BDD-cost:   29
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   83342   240304 |   27780       0        0     nan |  0.000 % |
c |       101 |   83342   240304 |   30558     101     1238    12.3 |  2.645 % |
c |       253 |   83310   240222 |   33613     250     2291     9.2 |  2.687 % |
c |       478 |   83198   239919 |   36975     466     3688     7.9 |  2.816 % |
c |       815 |   83061   239546 |   40672     786     5827     7.4 |  2.988 % |
c |      1321 |   82862   238989 |   44739    1264     9647     7.6 |  3.228 % |
c |      2080 |   82637   238410 |   49213    1993    14803     7.4 |  3.528 % |
c |      3219 |   82293   237522 |   54135    3078    22602     7.3 |  3.987 % |
c |      4928 |   81990   236725 |   59548    4703    38207     8.1 |  4.386 % |
c |      7491 |   80964   233866 |   65503    7050    57456     8.1 |  5.583 % |
c |     11335 |   79804   230622 |   72054   10650    88610     8.3 |  6.935 % |
c |     17102 |   78111   225854 |   79259   16095   145825     9.1 |  8.860 % |
c ==============================================================================
c [1mFound solution: 109[0m
c ---[   0]---> Sorter-cost:10236     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20394 |   88831   250539 |   29610   19215   178026     9.3 |  8.860 % |
c |     20495 |   88778   250398 |   32571   19282   178634     9.3 |  8.127 % |
c |     20645 |   88765   250359 |   35828   19412   179474     9.2 |  8.140 % |
c |     20871 |   88765   250359 |   39410   19638   181217     9.2 |  8.140 % |
c |     21208 |   88694   250149 |   43352   19954   183808     9.2 |  8.177 % |
c |     21714 |   88562   249753 |   47687   20455   189983     9.3 |  8.292 % |
c |     22473 |   88338   249119 |   52455   21187   198906     9.4 |  8.484 % |
c |     23612 |   88177   248662 |   57701   22301   210740     9.4 |  8.636 % |
c ==============================================================================
c [1mFound solution: 89[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25126 |   87623   247055 |   29207   23720   228308     9.6 |  8.636 % |
c |     25226 |   87590   246956 |   32127   23819   229286     9.6 |  9.346 % |
c |     25378 |   87587   246947 |   35340   23965   230567     9.6 |  9.348 % |
c |     25603 |   87546   246844 |   38874   24171   232423     9.6 |  9.393 % |
c |     25941 |   87543   246835 |   42761   24504   235856     9.6 |  9.396 % |
c |     26447 |   87498   246742 |   47038   25000   241580     9.7 |  9.453 % |
c |     27206 |   87368   246392 |   51741   25701   248162     9.7 |  9.584 % |
c |     28345 |   86957   245295 |   56916   26780   259204     9.7 | 10.006 % |
c ==============================================================================
c [1mFound solution: 85[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29674 |   86718   244616 |   28906   28069   273211     9.7 | 10.006 % |
c |     29776 |   86640   244400 |   31796   28169   273975     9.7 | 10.330 % |
c |     29929 |   86640   244400 |   34976   28322   275865     9.7 | 10.330 % |
c |     30154 |   86590   244264 |   38473   28543   277901     9.7 | 10.379 % |
c |     30491 |   86581   244237 |   42321   28871   280582     9.7 | 10.387 % |
c |     30997 |   86444   243834 |   46553   29359   288268     9.8 | 10.476 % |
c |     31758 |   86345   243559 |   51208   30106   295167     9.8 | 10.570 % |
c |     32897 |   86328   243508 |   56329   31221   312296    10.0 | 10.586 % |
c ==============================================================================
c [1mFound solution: 71[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33640 |   86330   243477 |   28776   31946   320573    10.0 | 10.586 % |
c |     33741 |   86300   243387 |   31653   32041   321364    10.0 | 10.718 % |
c |     33891 |   86294   243369 |   34818   32183   322611    10.0 | 10.723 % |
c |     34117 |   86115   242894 |   38300   32397   324492    10.0 | 10.905 % |
c |     34454 |   86048   242715 |   42130   32695   327302    10.0 | 10.973 % |
c |     34961 |   85836   242153 |   46344   33185   332725    10.0 | 11.190 % |
c |     35722 |   85665   241658 |   50978   33940   340153    10.0 | 11.347 % |
c |     36861 |   85133   240100 |   56076   35005   351277    10.0 | 11.756 % |
c ==============================================================================
c [1mFound solution: 57[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37144 |   85253   240396 |   28417   35276   354076    10.0 | 11.756 % |
c |     37244 |   85253   240396 |   31258   17738   151106     8.5 | 11.744 % |
c |     37395 |   85253   240396 |   34384   17889   153054     8.6 | 11.744 % |
c |     37621 |   85245   240380 |   37823   18112   155653     8.6 | 11.755 % |
c |     37958 |   85240   240365 |   41605   18448   158956     8.6 | 11.760 % |
c |     38464 |   85058   239885 |   45765   18944   164922     8.7 | 11.945 % |
c |     39224 |   84918   239483 |   50342   19691   172983     8.8 | 12.075 % |
c |     40363 |   84585   238544 |   55376   20775   183873     8.9 | 12.330 % |
c |     42071 |   84192   237433 |   60914   22435   204677     9.1 | 12.669 % |
c ==============================================================================
c [1mFound solution: 51[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42925 |   83942   236719 |   27980   23233   212956     9.2 | 12.669 % |
c |     43025 |   83942   236719 |   30778   23333   213923     9.2 | 12.939 % |
c ==============================================================================
c [1mFound solution: 45[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43125 |   84005   236886 |   28001   23433   214929     9.2 | 12.939 % |
c |     43225 |   84005   236886 |   30801   23533   216480     9.2 | 12.928 % |
c |     43375 |   83973   236792 |   33881   23680   218692     9.2 | 12.957 % |
c |     43600 |   83913   236612 |   37269   23902   223549     9.4 | 13.009 % |
c |     43939 |   83826   236369 |   40996   24225   227380     9.4 | 13.092 % |
c |     44445 |   83580   235650 |   45095   24679   233630     9.5 | 13.310 % |
c |     45208 |   83547   235569 |   49605   25400   242888     9.6 | 13.347 % |
c ==============================================================================
c [1mFound solution: 37[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45477 |   83592   235697 |   27864   25665   246581     9.6 | 13.347 % |
c |     45577 |   83592   235697 |   30650   25765   248249     9.6 | 13.365 % |
c |     45728 |   83592   235697 |   33715   25916   250945     9.7 | 13.365 % |
c |     45953 |   83557   235592 |   37086   26135   254313     9.7 | 13.397 % |
c |     46291 |   83527   235508 |   40795   26467   261577     9.9 | 13.407 % |
c ==============================================================================
c [1mFound solution: 34[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46708 |   83528   235504 |   27842   26849   268825    10.0 | 13.407 % |
c |     46812 |   83528   235504 |   30626   26953   269736    10.0 | 13.439 % |
c |     46962 |   83511   235465 |   33688   27097   273996    10.1 | 13.457 % |
c |     47189 |   83505   235447 |   37057   27319   276986    10.1 | 13.462 % |
c |     47527 |   83505   235447 |   40763   27657   287478    10.4 | 13.462 % |
c ==============================================================================
c [1mFound solution: 33[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47894 |   83524   235502 |   27841   28024   298072    10.6 | 13.462 % |
c |     47994 |   83524   235502 |   30625   28124   299491    10.6 | 13.463 % |
c |     48146 |   83524   235502 |   33687   28276   304248    10.8 | 13.463 % |
c |     48371 |   83524   235502 |   37056   28501   308541    10.8 | 13.463 % |
c |     48710 |   83418   235208 |   40762   28828   313909    10.9 | 13.567 % |
c |     49219 |   83406   235172 |   44838   29333   326182    11.1 | 13.577 % |
c ==============================================================================
c [1mFound solution: 30[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49808 |   83397   235130 |   27799   29811   335925    11.3 | 13.577 % |
c |     49908 |   83397   235130 |   30578   29911   337239    11.3 | 13.618 % |
c |     50058 |   83397   235130 |   33636   30061   339972    11.3 | 13.618 % |
c |     50283 |   83397   235130 |   37000   30286   345007    11.4 | 13.617 % |
c |     50620 |   83394   235121 |   40700   30620   353927    11.6 | 13.620 % |
c |     51126 |   83083   234230 |   44770   31106   366793    11.8 | 13.859 % |
c |     51885 |   82825   233490 |   49247   31841   390661    12.3 | 14.090 % |
c |     53025 |   82762   233301 |   54172   32978   430412    13.1 | 14.144 % |
c |     54733 |   82744   233247 |   59589   34685   485676    14.0 | 14.160 % |
c |     57296 |   82678   233061 |   65548   37243   571923    15.4 | 14.206 % |
c |     61142 |   82590   232815 |   72103   41061   720728    17.6 | 14.292 % |
c ==============================================================================
c [1mFound solution: 29[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65025 |   82540   232689 |   27513   44934   868083    19.3 | 14.292 % |
c |     65125 |   82455   232434 |   30264   20360   469438    23.1 | 14.436 % |
c |     65276 |   82455   232434 |   33290   20511   475056    23.2 | 14.436 % |
c |     65501 |   82455   232434 |   36619   20736   481863    23.2 | 14.436 % |
c |     65838 |   82455   232434 |   40281   21073   493084    23.4 | 14.436 % |
c |     66344 |   82455   232434 |   44309   21579   508900    23.6 | 14.436 % |
c |     67103 |   82423   232338 |   48740   22332   538485    24.1 | 14.464 % |
c |     68242 |   82347   232139 |   53615   23460   575334    24.5 | 14.532 % |
c ==============================================================================
c [1mFound solution: 28[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68345 |   82239   231863 |   27413   23532   576685    24.5 | 14.532 % |
c |     68445 |   82239   231863 |   30154   23632   579737    24.5 | 14.720 % |
c |     68596 |   82227   231827 |   33169   23778   584290    24.6 | 14.731 % |
c |     68825 |   82227   231827 |   36486   24007   591705    24.6 | 14.731 % |
c |     69163 |   82227   231827 |   40135   24345   602777    24.8 | 14.731 % |
c ==============================================================================
c [1mFound solution: 22[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69351 |   82237   231828 |   27412   23589   553656    23.5 | 14.731 % |
c |     69453 |   82237   231828 |   30153   23691   556080    23.5 | 14.765 % |
c |     69604 |   82237   231828 |   33168   23842   560162    23.5 | 14.765 % |
c |     69829 |   82237   231828 |   36485   24067   565618    23.5 | 14.765 % |
c |     70167 |   82237   231828 |   40133   24405   575927    23.6 | 14.765 % |
c |     70674 |   82237   231828 |   44147   24912   589848    23.7 | 14.765 % |
c |     71433 |   82237   231828 |   48562   25671   609387    23.7 | 14.765 % |
c |     72573 |   82237   231828 |   53418   26811   640075    23.9 | 14.765 % |
c |     74281 |   82219   231774 |   58760   28518   691206    24.2 | 14.780 % |
c |     76844 |   82219   231774 |   64636   31081   768061    24.7 | 14.780 % |
c |     80688 |   82198   231711 |   71099   34918   880310    25.2 | 14.798 % |
c |     86454 |   82125   231496 |   78209   40675  1036248    25.5 | 14.863 % |
c ==============================================================================
c [1mFound solution: 21[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91410 |   82109   231451 |   27369   45627  1183620    25.9 | 14.863 % |
c |     91511 |   82109   231451 |   30105   21543   399817    18.6 | 14.893 % |
c |     91661 |   82109   231451 |   33116   21693   404161    18.6 | 14.893 % |
c |     91886 |   82109   231451 |   36428   21918   410628    18.7 | 14.893 % |
c |     92223 |   82109   231451 |   40070   22255   417708    18.8 | 14.893 % |
c |     92729 |   82109   231451 |   44078   22761   430323    18.9 | 14.893 % |
c |     93490 |   82092   231400 |   48485   23521   450093    19.1 | 14.908 % |
c |     94631 |   82092   231400 |   53334   24662   477288    19.4 | 14.908 % |
c |     96341 |   82092   231400 |   58667   26372   512709    19.4 | 14.908 % |
c |     98903 |   82062   231310 |   64534   28932   565599    19.5 | 14.934 % |
c |    102747 |   82044   231256 |   70988   32772   657579    20.1 | 14.950 % |
c |    108516 |   82021   231187 |   78086   38540   796334    20.7 | 14.971 % |
c ==============================================================================
c [1mFound solution: 20[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115833 |   81884   230825 |   27294   45726   973104    21.3 | 14.971 % |
c |    115933 |   81884   230825 |   30023   21480   357501    16.6 | 15.172 % |
c |    116084 |   81884   230825 |   33025   21631   360611    16.7 | 15.172 % |
c |    116309 |   81884   230825 |   36328   21856   364398    16.7 | 15.172 % |
c |    116648 |   81884   230825 |   39961   22195   370862    16.7 | 15.172 % |
c |    117155 |   81881   230816 |   43957   22701   381418    16.8 | 15.175 % |
c |    117915 |   81881   230816 |   48352   23461   395772    16.9 | 15.175 % |
c |    119055 |   81881   230816 |   53188   24601   420881    17.1 | 15.175 % |
c |    120763 |   81862   230761 |   58507   26307   454579    17.3 | 15.177 % |
c |    123326 |   81862   230761 |   64357   28870   505645    17.5 | 15.177 % |
c ==============================================================================
c [1mFound solution: 19[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    126861 |   81876   230796 |   27292   32405   574143    17.7 | 15.177 % |
c |    126963 |   81876   230796 |   30021   32507   576203    17.7 | 15.176 % |
c |    127113 |   81876   230796 |   33023   32657   578881    17.7 | 15.176 % |
c |    127338 |   81876   230796 |   36325   32882   582134    17.7 | 15.176 % |
c |    127676 |   81876   230796 |   39958   33220   588614    17.7 | 15.176 % |
c |    128184 |   81876   230796 |   43954   33728   597547    17.7 | 15.176 % |
c |    128944 |   81876   230796 |   48349   34488   613888    17.8 | 15.176 % |
c |    130084 |   81876   230796 |   53184   35628   632908    17.8 | 15.176 % |
c |    131792 |   81876   230796 |   58502   37336   666473    17.9 | 15.176 % |
c |    134354 |   81876   230796 |   64353   39898   711536    17.8 | 15.176 % |
c |    138198 |   79835   224817 |   70788   18736   232813    12.4 | 16.788 % |
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              : 147
c conflicts             : 141547         (260 /sec)
c decisions             : 624346         (1147 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 544.176 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/55 4469
Raw data (stat): 4469 (runsolver) R 4468 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 740288360 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99964 s]
Raw data (loadavg): 0.92 0.95 0.90 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0005 s]
Raw data (loadavg): 0.93 0.95 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0013 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0013 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+544.342 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4473
Raw data (stat): 4469 (minisat+_script) S 4468 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740288360 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 544.342
CPU time (s): 544.399
CPU user time (s): 544.201
CPU system time (s): 0.197969
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	19
#### END VERIFIER DATA ####