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-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-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.05884
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 13433

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-20 21:04:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14651 boxname=wulflinc11 idbench=1127 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3fce91583b30a82646d8d8e778b97a89  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-neos1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-neos1.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-neos1.opb
IDLAUNCH: 14651
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        552804 kB
Buffers:         42448 kB
Cached:         410668 kB
SwapCached:       4932 kB
Active:         212572 kB
Inactive:       248360 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        552552 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            15228 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 21:06:37 (client local time) WITH STATUS 30 IN 107.546 SECONDS
stats: 14651 0 107.546 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5120 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[5118]---> Sorter-cost:  383     Base:
c ---[5116]---> Sorter-cost:  265     Base:
c ---[5114]---> Sorter-cost:  265     Base:
c ---[5112]---> Sorter-cost:  383     Base:
c ---[5110]---> Sorter-cost:  383     Base:
c ---[5108]---> Sorter-cost:  383     Base:
c ---[5106]---> Sorter-cost:  265     Base:
c ---[5104]---> Sorter-cost:  265     Base:
c ---[5102]---> Sorter-cost:  383     Base:
c ---[5100]---> Sorter-cost:  383     Base:
c ---[5098]---> Sorter-cost:  383     Base:
c ---[5096]---> Sorter-cost:  265     Base:
c ---[5094]---> Sorter-cost:  265     Base:
c ---[5092]---> Sorter-cost:  265     Base:
c ---[5090]---> Sorter-cost:  345     Base:
c ---[5088]---> Sorter-cost:  383     Base:
c ---[5086]---> Sorter-cost:  265     Base:
c ---[5084]---> Sorter-cost:  265     Base:
c ---[5082]---> Sorter-cost:  265     Base:
c ---[5080]---> Sorter-cost:  345     Base:
c ---[5078]---> Sorter-cost:  245     Base:
c ---[5076]---> Sorter-cost:  325     Base:
c ---[5074]---> Sorter-cost:  325     Base:
c ---[5072]---> Sorter-cost:  207     Base:
c ---[5070]---> Sorter-cost:  189     Base:
c ---[5068]---> Sorter-cost:  269     Base:
c ---[5066]---> Sorter-cost:  269     Base:
c ---[5064]---> Sorter-cost:  151     Base:
c ---[5062]---> Sorter-cost:  363     Base:
c ---[5060]---> Sorter-cost:  207     Base:
c ---[5058]---> Sorter-cost:  325     Base:
c ---[5056]---> Sorter-cost:  287     Base:
c ---[5054]---> Sorter-cost:  307     Base:
c ---[5052]---> Sorter-cost:  307     Base:
c ---[5050]---> Sorter-cost:  189     Base:
c ---[5048]---> Sorter-cost:  231     Base:
c ---[5046]---> Sorter-cost:  363     Base:
c ---[5044]---> Sorter-cost:  325     Base:
c ---[5042]---> Sorter-cost:  325     Base:
c ---[5040]---> Sorter-cost:  169     Base:
c ---[5038]---> Sorter-cost:  227     Base:
c ---[5036]---> Sorter-cost:  307     Base:
c ---[5034]---> Sorter-cost:  269     Base:
c ---[5032]---> Sorter-cost:  231     Base:
c ---[5030]---> Sorter-cost:  363     Base:
c ---[5028]---> Sorter-cost:  207     Base:
c ---[5026]---> Sorter-cost:  325     Base:
c ---[5024]---> Sorter-cost:  169     Base:
c ---[5022]---> Sorter-cost:  227     Base:
c ---[5020]---> Sorter-cost:  307     Base:
c ---[5018]---> Sorter-cost:  269     Base:
c ---[5016]---> Sorter-cost:  231     Base:
c ---[5014]---> Sorter-cost:  363     Base:
c ---[5012]---> Sorter-cost:  207     Base:
c ---[5010]---> Sorter-cost:  325     Base:
c ---[5008]---> Sorter-cost:  207     Base:
c ---[5006]---> Sorter-cost:  189     Base:
c ---[5004]---> Sorter-cost:  307     Base:
c ---[5002]---> Sorter-cost:  189     Base:
c ---[5000]---> Sorter-cost:  231     Base:
c ---[4998]---> Sorter-cost:  245     Base:
c ---[4996]---> Sorter-cost:  325     Base:
c ---[4994]---> Sorter-cost:  325     Base:
c ---[4992]---> Sorter-cost:  207     Base:
c ---[4990]---> Sorter-cost:  189     Base:
c ---[4988]---> Sorter-cost:  269     Base:
c ---[4986]---> Sorter-cost:  269     Base:
c ---[4984]---> Sorter-cost:  151     Base:
c ---[4982]---> Sorter-cost:  363     Base:
c ---[4980]---> Sorter-cost:  207     Base:
c ---[4978]---> Sorter-cost:  325     Base:
c ---[4976]---> Sorter-cost:  287     Base:
c ---[4974]---> Sorter-cost:  307     Base:
c ---[4972]---> Sorter-cost:  307     Base:
c ---[4970]---> Sorter-cost:  189     Base:
c ---[4968]---> Sorter-cost:  231     Base:
c ---[4966]---> Sorter-cost:  363     Base:
c ---[4964]---> Sorter-cost:  325     Base:
c ---[4962]---> Sorter-cost:  325     Base:
c ---[4960]---> Sorter-cost:  169     Base:
c ---[4958]---> Sorter-cost:  227     Base:
c ---[4956]---> Sorter-cost:  307     Base:
c ---[4954]---> Sorter-cost:  269     Base:
c ---[4952]---> Sorter-cost:  231     Base:
c ---[4950]---> Sorter-cost:  363     Base:
c ---[4948]---> Sorter-cost:  207     Base:
c ---[4946]---> Sorter-cost:  325     Base:
c ---[4944]---> Sorter-cost:  169     Base:
c ---[4942]---> Sorter-cost:  227     Base:
c ---[4940]---> Sorter-cost:  307     Base:
c ---[4938]---> Sorter-cost:  269     Base:
c ---[4936]---> Sorter-cost:  231     Base:
c ---[4934]---> Sorter-cost:  363     Base:
c ---[4932]---> Sorter-cost:  207     Base:
c ---[4930]---> Sorter-cost:  325     Base:
c ---[4928]---> Sorter-cost:  207     Base:
c ---[4926]---> Sorter-cost:  189     Base:
c ---[4924]---> Sorter-cost:  307     Base:
c ---[4922]---> Sorter-cost:  189     Base:
c ---[4920]---> Sorter-cost:  231     Base:
c ---[4919]---> BDD-cost:   27
c ---[4918]---> BDD-cost:   27
c ---[4917]---> BDD-cost:   27
c ---[4916]---> BDD-cost:   27
c ---[4915]---> BDD-cost:   27
c ---[4914]---> BDD-cost:   27
c ---[4913]---> BDD-cost:   27
c ---[4912]---> BDD-cost:   27
c ---[4911]---> BDD-cost:   27
c ---[4910]---> BDD-cost:   27
c ---[4909]---> BDD-cost:   27
c ---[4908]---> BDD-cost:   27
c ---[4907]---> BDD-cost:   27
c ---[4906]---> BDD-cost:   27
c ---[4905]---> BDD-cost:   27
c ---[4904]---> BDD-cost:   27
c ---[4903]---> BDD-cost:   27
c ---[4902]---> BDD-cost:   27
c ---[4901]---> BDD-cost:   27
c ---[4900]---> BDD-cost:   27
c ---[4899]---> BDD-cost:    0
c ---[4898]---> BDD-cost:    0
c ---[4897]---> BDD-cost:    0
c ---[4896]---> BDD-cost:    0
c ---[4895]---> BDD-cost:    0
c ---[4894]---> BDD-cost:    0
c ---[4893]---> BDD-cost:    0
c ---[4892]---> BDD-cost:    0
c ---[4891]---> BDD-cost:    0
c ---[4890]---> BDD-cost:    0
c ---[4889]---> BDD-cost:    0
c ---[4888]---> BDD-cost:    0
c ---[4887]---> BDD-cost:    0
c ---[4886]---> BDD-cost:    0
c ---[4885]---> BDD-cost:    0
c ---[4884]---> BDD-cost:    0
c ---[4883]---> BDD-cost:    0
c ---[4882]---> BDD-cost:    0
c ---[4881]---> BDD-cost:    0
c ---[4880]---> BDD-cost:    0
c ---[4879]---> BDD-cost:   27
c ---[4878]---> BDD-cost:   27
c ---[4877]---> BDD-cost:   27
c ---[4876]---> BDD-cost:   27
c ---[4875]---> BDD-cost:   27
c ---[4874]---> BDD-cost:    0
c ---[4873]---> BDD-cost:    0
c ---[4872]---> BDD-cost:    0
c ---[4871]---> BDD-cost:    0
c ---[4870]---> BDD-cost:    0
c ---[4869]---> BDD-cost:   27
c ---[4868]---> BDD-cost:   27
c ---[4867]---> BDD-cost:   27
c ---[4866]---> BDD-cost:   27
c ---[4865]---> BDD-cost:   27
c ---[4864]---> BDD-cost:    0
c ---[4863]---> BDD-cost:    0
c ---[4862]---> BDD-cost:    0
c ---[4861]---> BDD-cost:    0
c ---[4860]---> BDD-cost:    0
c ---[4859]---> BDD-cost:   27
c ---[4858]---> BDD-cost:   27
c ---[4857]---> BDD-cost:   27
c ---[4856]---> BDD-cost:   27
c ---[4855]---> BDD-cost:   27
c ---[4854]---> BDD-cost:    0
c ---[4853]---> BDD-cost:    0
c ---[4852]---> BDD-cost:    0
c ---[4851]---> BDD-cost:    0
c ---[4850]---> BDD-cost:    0
c ---[4849]---> BDD-cost:   27
c ---[4848]---> BDD-cost:   27
c ---[4847]---> BDD-cost:   27
c ---[4846]---> BDD-cost:   27
c ---[4845]---> BDD-cost:   27
c ---[4844]---> BDD-cost:    0
c ---[4843]---> BDD-cost:    0
c ---[4842]---> BDD-cost:    0
c ---[4841]---> BDD-cost:    0
c ---[4840]---> BDD-cost:    0
c ---[4839]---> BDD-cost:   27
c ---[4838]---> BDD-cost:   27
c ---[4837]---> BDD-cost:   27
c ---[4836]---> BDD-cost:   27
c ---[4835]---> BDD-cost:   27
c ---[4834]---> BDD-cost:    0
c ---[4833]---> BDD-cost:    0
c ---[4832]---> BDD-cost:    0
c ---[4831]---> BDD-cost:    0
c ---[4830]---> BDD-cost:    0
c ---[4829]---> BDD-cost:   27
c ---[4828]---> BDD-cost:   27
c ---[4827]---> BDD-cost:   27
c ---[4826]---> BDD-cost:   27
c ---[4825]---> BDD-cost:   27
c ---[4824]---> BDD-cost:    0
c ---[4823]---> BDD-cost:    0
c ---[4822]---> BDD-cost:    0
c ---[4821]---> BDD-cost:    0
c ---[4820]---> BDD-cost:    0
c ---[4819]---> BDD-cost:   27
c ---[4818]---> BDD-cost:   27
c ---[4817]---> BDD-cost:   27
c ---[4816]---> BDD-cost:   27
c ---[4815]---> BDD-cost:   27
c ---[4814]---> BDD-cost:    0
c ---[4813]---> BDD-cost:    0
c ---[4812]---> BDD-cost:    0
c ---[4811]---> BDD-cost:    0
c ---[4810]---> BDD-cost:    0
c ---[4809]---> BDD-cost:   27
c ---[4808]---> BDD-cost:   27
c ---[4807]---> BDD-cost:   27
c ---[4806]---> BDD-cost:   27
c ---[4805]---> BDD-cost:   27
c ---[4804]---> BDD-cost:    0
c ---[4803]---> BDD-cost:    0
c ---[4802]---> BDD-cost:    0
c ---[4801]---> BDD-cost:    0
c ---[4800]---> BDD-cost:    0
c ---[4799]---> BDD-cost:   27
c ---[4798]---> BDD-cost:   27
c ---[4797]---> BDD-cost:   27
c ---[4796]---> BDD-cost:   27
c ---[4795]---> BDD-cost:   27
c ---[4794]---> BDD-cost:    0
c ---[4793]---> BDD-cost:    0
c ---[4792]---> BDD-cost:    0
c ---[4791]---> BDD-cost:    0
c ---[4790]---> BDD-cost:    0
c ---[4789]---> BDD-cost:   27
c ---[4788]---> BDD-cost:   27
c ---[4787]---> BDD-cost:   27
c ---[4786]---> BDD-cost:   27
c ---[4785]---> BDD-cost:   27
c ---[4784]---> BDD-cost:    0
c ---[4783]---> BDD-cost:    0
c ---[4782]---> BDD-cost:    0
c ---[4781]---> BDD-cost:    0
c ---[4780]---> BDD-cost:    0
c ---[4779]---> BDD-cost:   27
c ---[4778]---> BDD-cost:   27
c ---[4777]---> BDD-cost:   27
c ---[4776]---> BDD-cost:   27
c ---[4775]---> BDD-cost:   27
c ---[4774]---> BDD-cost:    0
c ---[4773]---> BDD-cost:    0
c ---[4772]---> BDD-cost:    0
c ---[4771]---> BDD-cost:    0
c ---[4770]---> BDD-cost:    0
c ---[4769]---> BDD-cost:   27
c ---[4768]---> BDD-cost:   27
c ---[4767]---> BDD-cost:   27
c ---[4766]---> BDD-cost:   27
c ---[4765]---> BDD-cost:   27
c ---[4764]---> BDD-cost:    0
c ---[4763]---> BDD-cost:    0
c ---[4762]---> BDD-cost:    0
c ---[4761]---> BDD-cost:    0
c ---[4760]---> BDD-cost:    0
c ---[4759]---> BDD-cost:   27
c ---[4758]---> BDD-cost:   27
c ---[4757]---> BDD-cost:   27
c ---[4756]---> BDD-cost:   27
c ---[4755]---> BDD-cost:   27
c ---[4754]---> BDD-cost:    0
c ---[4753]---> BDD-cost:    0
c ---[4752]---> BDD-cost:    0
c ---[4751]---> BDD-cost:    0
c ---[4750]---> BDD-cost:    0
c ---[4749]---> BDD-cost:   27
c ---[4748]---> BDD-cost:   27
c ---[4747]---> BDD-cost:   27
c ---[4746]---> BDD-cost:   27
c ---[4745]---> BDD-cost:   27
c ---[4744]---> BDD-cost:    0
c ---[4743]---> BDD-cost:    0
c ---[4742]---> BDD-cost:    0
c ---[4741]---> BDD-cost:    0
c ---[4740]---> BDD-cost:    0
c ---[4739]---> BDD-cost:    5
c ---[4738]---> BDD-cost:    5
c ---[4737]---> BDD-cost:    5
c ---[4736]---> BDD-cost:    5
c ---[4735]---> BDD-cost:    5
c ---[4734]---> BDD-cost:    5
c ---[4733]---> BDD-cost:    5
c ---[4732]---> BDD-cost:    5
c ---[4731]---> BDD-cost:    5
c ---[4730]---> BDD-cost:    5
c ---[4729]---> BDD-cost:    5
c ---[4728]---> BDD-cost:    5
c ---[4727]---> BDD-cost:    5
c ---[4726]---> BDD-cost:    5
c ---[4725]---> BDD-cost:    5
c ---[4724]---> BDD-cost:    5
c ---[4723]---> BDD-cost:    5
c ---[4722]---> BDD-cost:    5
c ---[4721]---> BDD-cost:    5
c ---[4720]---> BDD-cost:    5
c ---[4719]---> BDD-cost:    5
c ---[4718]---> BDD-cost:    5
c ---[4717]---> BDD-cost:    5
c ---[4716]---> BDD-cost:    5
c ---[4715]---> BDD-cost:    5
c ---[4714]---> BDD-cost:    5
c ---[4713]---> BDD-cost:    5
c ---[4712]---> BDD-cost:    5
c ---[4711]---> BDD-cost:    5
c ---[4710]---> BDD-cost:    5
c ---[4709]---> BDD-cost:    5
c ---[4708]---> BDD-cost:    5
c ---[4707]---> BDD-cost:    5
c ---[4706]---> BDD-cost:    5
c ---[4705]---> BDD-cost:    5
c ---[4704]---> BDD-cost:    5
c ---[4703]---> BDD-cost:    5
c ---[4702]---> BDD-cost:    5
c ---[4701]---> BDD-cost:    5
c ---[4700]---> BDD-cost:    5
c ---[4699]---> BDD-cost:    5
c ---[4698]---> BDD-cost:    5
c ---[4697]---> BDD-cost:    5
c ---[4696]---> BDD-cost:    5
c ---[4695]---> BDD-cost:    5
c ---[4694]---> BDD-cost:    5
c ---[4693]---> BDD-cost:    5
c ---[4692]---> BDD-cost:    5
c ---[4691]---> BDD-cost:    5
c ---[4690]---> BDD-cost:    5
c ---[4689]---> BDD-cost:    5
c ---[4688]---> BDD-cost:    5
c ---[4687]---> BDD-cost:    5
c ---[4686]---> BDD-cost:    5
c ---[4685]---> BDD-cost:    5
c ---[4684]---> BDD-cost:    5
c ---[4683]---> BDD-cost:    5
c ---[4682]---> BDD-cost:    5
c ---[4681]---> BDD-cost:    5
c ---[4680]---> BDD-cost:    5
c ---[4679]---> BDD-cost:    5
c ---[4678]---> BDD-cost:    5
c ---[4677]---> BDD-cost:    5
c ---[4676]---> BDD-cost:    5
c ---[4675]---> BDD-cost:    5
c ---[4674]---> BDD-cost:    5
c ---[4673]---> BDD-cost:    5
c ---[4672]---> BDD-cost:    5
c ---[4671]---> BDD-cost:    5
c ---[4670]---> BDD-cost:    5
c ---[4669]---> BDD-cost:    5
c ---[4668]---> BDD-cost:    5
c ---[4667]---> BDD-cost:    5
c ---[4666]---> BDD-cost:    5
c ---[4665]---> BDD-cost:    5
c ---[4664]---> BDD-cost:    5
c ---[4663]---> BDD-cost:    5
c ---[4662]---> BDD-cost:    5
c ---[4661]---> BDD-cost:    5
c ---[4660]---> BDD-cost:    5
c ---[4659]---> BDD-cost:    5
c ---[4658]---> BDD-cost:    5
c ---[4657]---> BDD-cost:    5
c ---[4656]---> BDD-cost:    5
c ---[4655]---> BDD-cost:    5
c ---[4654]---> BDD-cost:    5
c ---[4653]---> BDD-cost:    5
c ---[4652]---> BDD-cost:    5
c ---[4651]---> BDD-cost:    5
c ---[4650]---> BDD-cost:    5
c ---[4649]---> BDD-cost:    5
c ---[4648]---> BDD-cost:    5
c ---[4647]---> BDD-cost:    5
c ---[4646]---> BDD-cost:    5
c ---[4645]---> BDD-cost:    5
c ---[4644]---> BDD-cost:    5
c ---[4643]---> BDD-cost:    5
c ---[4642]---> BDD-cost:    5
c ---[4641]---> BDD-cost:    5
c ---[4640]---> BDD-cost:    5
c ---[4639]---> BDD-cost:    5
c ---[4638]---> BDD-cost:    5
c ---[4637]---> BDD-cost:    5
c ---[4636]---> BDD-cost:    5
c ---[4635]---> BDD-cost:    5
c ---[4634]---> BDD-cost:    5
c ---[4633]---> BDD-cost:    5
c ---[4632]---> BDD-cost:    5
c ---[4631]---> BDD-cost:    5
c ---[4630]---> BDD-cost:    5
c ---[4629]---> BDD-cost:    5
c ---[4628]---> BDD-cost:    5
c ---[4627]---> BDD-cost:    5
c ---[4626]---> BDD-cost:    5
c ---[4625]---> BDD-cost:    5
c ---[4624]---> BDD-cost:    5
c ---[4623]---> BDD-cost:    5
c ---[4622]---> BDD-cost:    5
c ---[4621]---> BDD-cost:    5
c ---[4620]---> BDD-cost:    5
c ---[4619]---> BDD-cost:    5
c ---[4618]---> BDD-cost:    5
c ---[4617]---> BDD-cost:    5
c ---[4616]---> BDD-cost:    5
c ---[4615]---> BDD-cost:    5
c ---[4614]---> BDD-cost:    5
c ---[4613]---> BDD-cost:    5
c ---[4612]---> BDD-cost:    5
c ---[4611]---> BDD-cost:    5
c ---[4610]---> BDD-cost:    5
c ---[4609]---> BDD-cost:    5
c ---[4608]---> BDD-cost:    5
c ---[4607]---> BDD-cost:    5
c ---[4606]---> BDD-cost:    5
c ---[4605]---> BDD-cost:    5
c ---[4604]---> BDD-cost:    5
c ---[4603]---> BDD-cost:    5
c ---[4602]---> BDD-cost:    5
c ---[4601]---> BDD-cost:    5
c ---[4600]---> BDD-cost:    5
c ---[4599]---> BDD-cost:    5
c ---[4598]---> BDD-cost:    5
c ---[4597]---> BDD-cost:    5
c ---[4596]---> BDD-cost:    5
c ---[4451]---> BDD-cost:    2
c ---[4450]---> BDD-cost:    2
c ---[4449]---> BDD-cost:    2
c ---[4448]---> BDD-cost:    2
c ---[4447]---> BDD-cost:    2
c ---[4446]---> BDD-cost:    2
c ---[4445]---> BDD-cost:    2
c ---[4444]---> BDD-cost:    2
c ---[4443]---> BDD-cost:    2
c ---[4442]---> BDD-cost:    2
c ---[4441]---> BDD-cost:    2
c ---[4440]---> BDD-cost:    2
c ---[4439]---> BDD-cost:    2
c ---[4438]---> BDD-cost:    2
c ---[4437]---> BDD-cost:    2
c ---[4436]---> BDD-cost:    2
c ---[4435]---> BDD-cost:    2
c ---[4434]---> BDD-cost:    2
c ---[4433]---> BDD-cost:    2
c ---[4432]---> BDD-cost:    2
c ---[4431]---> BDD-cost:    2
c ---[4430]---> BDD-cost:    2
c ---[4429]---> BDD-cost:    2
c ---[4428]---> BDD-cost:    2
c ---[4427]---> BDD-cost:    2
c ---[4426]---> BDD-cost:    2
c ---[4425]---> BDD-cost:    2
c ---[4424]---> BDD-cost:    2
c ---[4423]---> BDD-cost:    2
c ---[4422]---> BDD-cost:    2
c ---[4421]---> BDD-cost:    2
c ---[4420]---> BDD-cost:    2
c ---[4419]---> BDD-cost:    2
c ---[4418]---> BDD-cost:    2
c ---[4417]---> BDD-cost:    2
c ---[4416]---> BDD-cost:    2
c ---[4415]---> BDD-cost:    2
c ---[4414]---> BDD-cost:    2
c ---[4413]---> BDD-cost:    2
c ---[4412]---> BDD-cost:    2
c ---[4411]---> BDD-cost:    2
c ---[4410]---> BDD-cost:    2
c ---[4409]---> BDD-cost:    2
c ---[4408]---> BDD-cost:    2
c ---[4407]---> BDD-cost:    2
c ---[4406]---> BDD-cost:    2
c ---[4405]---> BDD-cost:    2
c ---[4404]---> BDD-cost:    2
c ---[4403]---> BDD-cost:    2
c ---[4402]---> BDD-cost:    2
c ---[4401]---> BDD-cost:    2
c ---[4400]---> BDD-cost:    2
c ---[4399]---> BDD-cost:    2
c ---[4398]---> BDD-cost:    2
c ---[4397]---> BDD-cost:    2
c ---[4396]---> BDD-cost:    2
c ---[4395]---> BDD-cost:    2
c ---[4394]---> BDD-cost:    2
c ---[4393]---> BDD-cost:    2
c ---[4392]---> BDD-cost:    2
c ---[4391]---> BDD-cost:    2
c ---[4390]---> BDD-cost:    2
c ---[4389]---> BDD-cost:    2
c ---[4388]---> BDD-cost:    2
c ---[4387]---> BDD-cost:    2
c ---[4386]---> BDD-cost:    2
c ---[4385]---> BDD-cost:    2
c ---[4384]---> BDD-cost:    2
c ---[4383]---> BDD-cost:    2
c ---[4382]---> BDD-cost:    2
c ---[4381]---> BDD-cost:    2
c ---[4380]---> BDD-cost:    2
c ---[4379]---> BDD-cost:    2
c ---[4378]---> BDD-cost:    2
c ---[4377]---> BDD-cost:    2
c ---[4376]---> BDD-cost:    2
c ---[4375]---> BDD-cost:    2
c ---[4374]---> BDD-cost:    2
c ---[4373]---> BDD-cost:    2
c ---[4372]---> BDD-cost:    2
c ---[4371]---> BDD-cost:    2
c ---[4370]---> BDD-cost:    2
c ---[4369]---> BDD-cost:    2
c ---[4368]---> BDD-cost:    2
c ---[4367]---> BDD-cost:    2
c ---[4366]---> BDD-cost:    2
c ---[4365]---> BDD-cost:    2
c ---[4364]---> BDD-cost:    2
c ---[4363]---> BDD-cost:    2
c ---[4362]---> BDD-cost:    2
c ---[4361]---> BDD-cost:    2
c ---[4360]---> BDD-cost:    2
c ---[4359]---> BDD-cost:    2
c ---[4358]---> BDD-cost:    2
c ---[4357]---> BDD-cost:    2
c ---[4356]---> BDD-cost:    2
c ---[4355]---> BDD-cost:    2
c ---[4354]---> BDD-cost:    2
c ---[4353]---> BDD-cost:    2
c ---[4352]---> BDD-cost:    2
c ---[4351]---> BDD-cost:    2
c ---[4350]---> BDD-cost:    2
c ---[4349]---> BDD-cost:    2
c ---[4348]---> BDD-cost:    2
c ---[4347]---> BDD-cost:    2
c ---[4346]---> BDD-cost:    2
c ---[4345]---> BDD-cost:    2
c ---[4344]---> BDD-cost:    2
c ---[4343]---> BDD-cost:    2
c ---[4342]---> BDD-cost:    2
c ---[4341]---> BDD-cost:    2
c ---[4340]---> BDD-cost:    2
c ---[4339]---> BDD-cost:    2
c ---[4338]---> BDD-cost:    2
c ---[4337]---> BDD-cost:    2
c ---[4336]---> BDD-cost:    2
c ---[4335]---> BDD-cost:    2
c ---[4334]---> BDD-cost:    2
c ---[4333]---> BDD-cost:    2
c ---[4332]---> BDD-cost:    2
c ---[4331]---> BDD-cost:    2
c ---[4330]---> BDD-cost:    2
c ---[4329]---> BDD-cost:    2
c ---[4328]---> BDD-cost:    2
c ---[4327]---> BDD-cost:    2
c ---[4326]---> BDD-cost:    2
c ---[4325]---> BDD-cost:    2
c ---[4324]---> BDD-cost:    2
c ---[4323]---> BDD-cost:    2
c ---[4322]---> BDD-cost:    2
c ---[4321]---> BDD-cost:    2
c ---[4320]---> BDD-cost:    2
c ---[4319]---> BDD-cost:    2
c ---[4318]---> BDD-cost:    2
c ---[4317]---> BDD-cost:    2
c ---[4316]---> BDD-cost:    2
c ---[4315]---> BDD-cost:    2
c ---[4314]---> BDD-cost:    2
c ---[4313]---> BDD-cost:    2
c ---[4312]---> BDD-cost:    2
c ---[4311]---> BDD-cost:    2
c ---[4310]---> BDD-cost:    2
c ---[4309]---> BDD-cost:    2
c ---[4308]---> BDD-cost:    2
c ---[4307]---> BDD-cost:    3
c ---[4306]---> BDD-cost:    3
c ---[4305]---> BDD-cost:    3
c ---[4304]---> BDD-cost:    3
c ---[4303]---> BDD-cost:    3
c ---[4302]---> BDD-cost:    3
c ---[4301]---> BDD-cost:    3
c ---[4300]---> BDD-cost:    3
c ---[4299]---> BDD-cost:    3
c ---[4298]---> BDD-cost:    3
c ---[4297]---> BDD-cost:    3
c ---[4296]---> BDD-cost:    3
c ---[4295]---> BDD-cost:    3
c ---[4294]---> BDD-cost:    3
c ---[4293]---> BDD-cost:    3
c ---[4292]---> BDD-cost:    3
c ---[4291]---> BDD-cost:    3
c ---[4290]---> BDD-cost:    3
c ---[4289]---> BDD-cost:    3
c ---[4288]---> BDD-cost:    3
c ---[4287]---> BDD-cost:    3
c ---[4286]---> BDD-cost:    3
c ---[4285]---> BDD-cost:    3
c ---[4284]---> BDD-cost:    3
c ---[4283]---> BDD-cost:    3
c ---[4282]---> BDD-cost:    3
c ---[4281]---> BDD-cost:    3
c ---[4280]---> BDD-cost:    3
c ---[4279]---> BDD-cost:    3
c ---[4278]---> BDD-cost:    3
c ---[4277]---> BDD-cost:    3
c ---[4276]---> BDD-cost:    3
c ---[4275]---> BDD-cost:    3
c ---[4274]---> BDD-cost:    3
c ---[4273]---> BDD-cost:    3
c ---[4272]---> BDD-cost:    3
c ---[4271]---> BDD-cost:    3
c ---[4270]---> BDD-cost:    3
c ---[4269]---> BDD-cost:    3
c ---[4268]---> BDD-cost:    3
c ---[4267]---> BDD-cost:    3
c ---[4266]---> BDD-cost:    3
c ---[4265]---> BDD-cost:    3
c ---[4264]---> BDD-cost:    3
c ---[4263]---> BDD-cost:    3
c ---[4262]---> BDD-cost:    3
c ---[4261]---> BDD-cost:    3
c ---[4260]---> BDD-cost:    3
c ---[4259]---> BDD-cost:    3
c ---[4258]---> BDD-cost:    3
c ---[4257]---> BDD-cost:    3
c ---[4256]---> BDD-cost:    3
c ---[4255]---> BDD-cost:    3
c ---[4254]---> BDD-cost:    3
c ---[4253]---> BDD-cost:    3
c ---[4252]---> BDD-cost:    3
c ---[4251]---> BDD-cost:    3
c ---[4250]---> BDD-cost:    3
c ---[4249]---> BDD-cost:    3
c ---[4248]---> BDD-cost:    3
c ---[4247]---> BDD-cost:    3
c ---[4246]---> BDD-cost:    3
c ---[4245]---> BDD-cost:    3
c ---[4244]---> BDD-cost:    3
c ---[4243]---> BDD-cost:    3
c ---[4242]---> BDD-cost:    3
c ---[4241]---> BDD-cost:    3
c ---[4240]---> BDD-cost:    3
c ---[4239]---> BDD-cost:    3
c ---[4238]---> BDD-cost:    3
c ---[4237]---> BDD-cost:    3
c ---[4236]---> BDD-cost:    3
c ---[4235]---> BDD-cost:    3
c ---[4234]---> BDD-cost:    3
c ---[4233]---> BDD-cost:    3
c ---[4232]---> BDD-cost:    3
c ---[4231]---> BDD-cost:    3
c ---[4230]---> BDD-cost:    3
c ---[4229]---> BDD-cost:    3
c ---[4228]---> BDD-cost:    3
c ---[4227]---> BDD-cost:    3
c ---[4226]---> BDD-cost:    3
c ---[4225]---> BDD-cost:    3
c ---[4224]---> BDD-cost:    3
c ---[4223]---> BDD-cost:    3
c ---[4222]---> BDD-cost:    3
c ---[4221]---> BDD-cost:    3
c ---[4220]---> BDD-cost:    3
c ---[4219]---> BDD-cost:    3
c ---[4218]---> BDD-cost:    3
c ---[4217]---> BDD-cost:    3
c ---[4216]---> BDD-cost:    3
c ---[4215]---> BDD-cost:    3
c ---[4214]---> BDD-cost:    3
c ---[4213]---> BDD-cost:    3
c ---[4212]---> BDD-cost:    3
c ---[4211]---> BDD-cost:    3
c ---[4210]---> BDD-cost:    3
c ---[4209]---> BDD-cost:    3
c ---[4208]---> BDD-cost:    3
c ---[4207]---> BDD-cost:    3
c ---[4206]---> BDD-cost:    3
c ---[4205]---> BDD-cost:    3
c ---[4204]---> BDD-cost:    3
c ---[4203]---> BDD-cost:    3
c ---[4202]---> BDD-cost:    3
c ---[4201]---> BDD-cost:    3
c ---[4200]---> BDD-cost:    3
c ---[4199]---> BDD-cost:    3
c ---[4198]---> BDD-cost:    3
c ---[4197]---> BDD-cost:    3
c ---[4196]---> BDD-cost:    3
c ---[4195]---> BDD-cost:    3
c ---[4194]---> BDD-cost:    3
c ---[4193]---> BDD-cost:    3
c ---[4192]---> BDD-cost:    3
c ---[4191]---> BDD-cost:    3
c ---[4190]---> BDD-cost:    3
c ---[4189]---> BDD-cost:    3
c ---[4188]---> BDD-cost:    3
c ---[4187]---> BDD-cost:    3
c ---[4186]---> BDD-cost:    3
c ---[4185]---> BDD-cost:    3
c ---[4184]---> BDD-cost:    3
c ---[4183]---> BDD-cost:    3
c ---[4182]---> BDD-cost:    3
c ---[4181]---> BDD-cost:    3
c ---[4180]---> BDD-cost:    3
c ---[4179]---> BDD-cost:    3
c ---[4178]---> BDD-cost:    3
c ---[4177]---> BDD-cost:    3
c ---[4176]---> BDD-cost:    3
c ---[4175]---> BDD-cost:    3
c ---[4174]---> BDD-cost:    3
c ---[4173]---> BDD-cost:    3
c ---[4172]---> BDD-cost:    3
c ---[4171]---> BDD-cost:    3
c ---[4170]---> BDD-cost:    3
c ---[4169]---> BDD-cost:    3
c ---[4168]---> BDD-cost:    3
c ---[4167]---> BDD-cost:    3
c ---[4166]---> BDD-cost:    3
c ---[4165]---> BDD-cost:    3
c ---[4164]---> BDD-cost:    3
c ---[4163]---> BDD-cost:    4
c ---[4162]---> BDD-cost:    4
c ---[4161]---> BDD-cost:    4
c ---[4160]---> BDD-cost:    4
c ---[4159]---> BDD-cost:    4
c ---[4158]---> BDD-cost:    4
c ---[4157]---> BDD-cost:    4
c ---[4156]---> BDD-cost:    4
c ---[4155]---> BDD-cost:    4
c ---[4154]---> BDD-cost:    4
c ---[4153]---> BDD-cost:    4
c ---[4152]---> BDD-cost:    4
c ---[4151]---> BDD-cost:    4
c ---[4150]---> BDD-cost:    4
c ---[4149]---> BDD-cost:    4
c ---[4148]---> BDD-cost:    4
c ---[4147]---> BDD-cost:    4
c ---[4146]---> BDD-cost:    4
c ---[4145]---> BDD-cost:    4
c ---[4144]---> BDD-cost:    4
c ---[4143]---> BDD-cost:    4
c ---[4142]---> BDD-cost:    4
c ---[4141]---> BDD-cost:    4
c ---[4140]---> BDD-cost:    4
c ---[4139]---> BDD-cost:    4
c ---[4138]---> BDD-cost:    4
c ---[4137]---> BDD-cost:    4
c ---[4136]---> BDD-cost:    4
c ---[4135]---> BDD-cost:    4
c ---[4134]---> BDD-cost:    4
c ---[4133]---> BDD-cost:    4
c ---[4132]---> BDD-cost:    4
c ---[4131]---> BDD-cost:    4
c ---[4130]---> BDD-cost:    4
c ---[4129]---> BDD-cost:    4
c ---[4128]---> BDD-cost:    4
c ---[4127]---> BDD-cost:    4
c ---[4126]---> BDD-cost:    4
c ---[4125]---> BDD-cost:    4
c ---[4124]---> BDD-cost:    4
c ---[4123]---> BDD-cost:    4
c ---[4122]---> BDD-cost:    4
c ---[4121]---> BDD-cost:    4
c ---[4120]---> BDD-cost:    4
c ---[4119]---> BDD-cost:    4
c ---[4118]---> BDD-cost:    4
c ---[4117]---> BDD-cost:    4
c ---[4116]---> BDD-cost:    4
c ---[4115]---> BDD-cost:    4
c ---[4114]---> BDD-cost:    4
c ---[4113]---> BDD-cost:    4
c ---[4112]---> BDD-cost:    4
c ---[4111]---> BDD-cost:    4
c ---[4110]---> BDD-cost:    4
c ---[4109]---> BDD-cost:    4
c ---[4108]---> BDD-cost:    4
c ---[4107]---> BDD-cost:    4
c ---[4106]---> BDD-cost:    4
c ---[4105]---> BDD-cost:    4
c ---[4104]---> BDD-cost:    4
c ---[4103]---> BDD-cost:    4
c ---[4102]---> BDD-cost:    4
c ---[4101]---> BDD-cost:    4
c ---[4100]---> BDD-cost:    4
c ---[4099]---> BDD-cost:    4
c ---[4098]---> BDD-cost:    4
c ---[4097]---> BDD-cost:    4
c ---[4096]---> BDD-cost:    4
c ---[4095]---> BDD-cost:    4
c ---[4094]---> BDD-cost:    4
c ---[4093]---> BDD-cost:    4
c ---[4092]---> BDD-cost:    4
c ---[4091]---> BDD-cost:    4
c ---[4090]---> BDD-cost:    4
c ---[4089]---> BDD-cost:    4
c ---[4088]---> BDD-cost:    4
c ---[4087]---> BDD-cost:    4
c ---[4086]---> BDD-cost:    4
c ---[4085]---> BDD-cost:    4
c ---[4084]---> BDD-cost:    4
c ---[4083]---> BDD-cost:    4
c ---[4082]---> BDD-cost:    4
c ---[4081]---> BDD-cost:    4
c ---[4080]---> BDD-cost:    4
c ---[4079]---> BDD-cost:    4
c ---[4078]---> BDD-cost:    4
c ---[4077]---> BDD-cost:    4
c ---[4076]---> BDD-cost:    4
c ---[4075]---> BDD-cost:    4
c ---[4074]---> BDD-cost:    4
c ---[4073]---> BDD-cost:    4
c ---[4072]---> BDD-cost:    4
c ---[4071]---> BDD-cost:    4
c ---[4070]---> BDD-cost:    4
c ---[4069]---> BDD-cost:    4
c ---[4068]---> BDD-cost:    4
c ---[4067]---> BDD-cost:    4
c ---[4066]---> BDD-cost:    4
c ---[4065]---> BDD-cost:    4
c ---[4064]---> BDD-cost:    4
c ---[4063]---> BDD-cost:    4
c ---[4062]---> BDD-cost:    4
c ---[4061]---> BDD-cost:    4
c ---[4060]---> BDD-cost:    4
c ---[4059]---> BDD-cost:    4
c ---[4058]---> BDD-cost:    4
c ---[4057]---> BDD-cost:    4
c ---[4056]---> BDD-cost:    4
c ---[4055]---> BDD-cost:    4
c ---[4054]---> BDD-cost:    4
c ---[4053]---> BDD-cost:    4
c ---[4052]---> BDD-cost:    4
c ---[4051]---> BDD-cost:    4
c ---[4050]---> BDD-cost:    4
c ---[4049]---> BDD-cost:    4
c ---[4048]---> BDD-cost:    4
c ---[4047]---> BDD-cost:    4
c ---[4046]---> BDD-cost:    4
c ---[4045]---> BDD-cost:    4
c ---[4044]---> BDD-cost:    4
c ---[4043]---> BDD-cost:    4
c ---[4042]---> BDD-cost:    4
c ---[4041]---> BDD-cost:    4
c ---[4040]---> BDD-cost:    4
c ---[4039]---> BDD-cost:    4
c ---[4038]---> BDD-cost:    4
c ---[4037]---> BDD-cost:    4
c ---[4036]---> BDD-cost:    4
c ---[4035]---> BDD-cost:    4
c ---[4034]---> BDD-cost:    4
c ---[4033]---> BDD-cost:    4
c ---[4032]---> BDD-cost:    4
c ---[4031]---> BDD-cost:    4
c ---[4030]---> BDD-cost:    4
c ---[4029]---> BDD-cost:    4
c ---[4028]---> BDD-cost:    4
c ---[4027]---> BDD-cost:    4
c ---[4026]---> BDD-cost:    4
c ---[4025]---> BDD-cost:    4
c ---[4024]---> BDD-cost:    4
c ---[4023]---> BDD-cost:    4
c ---[4022]---> BDD-cost:    4
c ---[4021]---> BDD-cost:    4
c ---[4020]---> BDD-cost:    4
c ---[3875]---> BDD-cost:   19
c ---[3874]---> BDD-cost:   19
c ---[3873]---> BDD-cost:   19
c ---[3872]---> BDD-cost:   19
c ---[3871]---> BDD-cost:   19
c ---[3870]---> BDD-cost:   19
c ---[3869]---> BDD-cost:   19
c ---[3868]---> BDD-cost:   19
c ---[3867]---> BDD-cost:   19
c ---[3866]---> BDD-cost:   19
c ---[3865]---> BDD-cost:   19
c ---[3864]---> BDD-cost:   19
c ---[3863]---> BDD-cost:   19
c ---[3862]---> BDD-cost:   19
c ---[3861]---> BDD-cost:   19
c ---[3860]---> BDD-cost:   19
c ---[3859]---> BDD-cost:   19
c ---[3858]---> BDD-cost:   19
c ---[3857]---> BDD-cost:   19
c ---[3856]---> BDD-cost:   19
c ---[3855]---> BDD-cost:   19
c ---[3854]---> BDD-cost:   19
c ---[3853]---> BDD-cost:   19
c ---[3852]---> BDD-cost:   19
c ---[3851]---> BDD-cost:   19
c ---[3850]---> BDD-cost:   19
c ---[3849]---> BDD-cost:   19
c ---[3848]---> BDD-cost:   19
c ---[3847]---> BDD-cost:   19
c ---[3846]---> BDD-cost:   19
c ---[3845]---> BDD-cost:   19
c ---[3844]---> BDD-cost:   19
c ---[3843]---> BDD-cost:   19
c ---[3842]---> BDD-cost:   19
c ---[3841]---> BDD-cost:   19
c ---[3840]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   73710   183706 |   24570       0        0     nan |  0.000 % |
c |       100 |   73332   182790 |   27027      35      169     4.8 |  5.350 % |
c |       250 |   72898   181768 |   29729     129      744     5.8 |  5.816 % |
c |       475 |   72084   179794 |   32702     225     1238     5.5 |  6.683 % |
c |       812 |   70907   177098 |   35972     434     2588     6.0 |  8.034 % |
c |      1319 |   69013   172726 |   39570     751     4550     6.1 | 10.221 % |
c |      2079 |   65326   164162 |   43527    1145     6667     5.8 | 14.550 % |
c |      3218 |   61065   154206 |   47879    1850    10309     5.6 | 19.648 % |
c |      4926 |   52426   133922 |   52667    2870    15923     5.5 | 30.420 % |
c |      7488 |   42640   110990 |   57934    4450    25108     5.6 | 42.877 % |
c ==============================================================================
c [1mFound solution: 67[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10236     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7656 |   65107   163588 |   21702    4547    25690     5.6 | 42.877 % |
c |      7756 |   64409   161947 |   23872    4601    25994     5.6 | 33.702 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7856 |   64030   161036 |   21343    4657    26297     5.6 | 33.702 % |
c |      7956 |   63628   160071 |   23477    4710    26659     5.7 | 34.512 % |
c |      8109 |   63381   159509 |   25825    4853    27404     5.6 | 34.741 % |
c |      8335 |   63320   159363 |   28407    5075    29568     5.8 | 34.802 % |
c |      8673 |   63320   159363 |   31248    5413    34227     6.3 | 34.802 % |
c |      9179 |   63228   159153 |   34373    5917    39615     6.7 | 34.886 % |
c |      9938 |   62690   157844 |   37810    6625    45034     6.8 | 35.389 % |
c |     11077 |   61547   155133 |   41591    7640    51435     6.7 | 36.543 % |
c |     12785 |   58794   148731 |   45750    8958    59984     6.7 | 39.290 % |
c |     15350 |   57023   144453 |   50325   11254    83472     7.4 | 41.025 % |
c |     19194 |   56100   142241 |   55358   14874   131342     8.8 | 41.956 % |
c ==============================================================================
c [1mFound solution: 65[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19840 |   55871   141691 |   18623   15495   136001     8.8 | 41.956 % |
c |     19941 |   55856   141646 |   20485   15590   136894     8.8 | 42.252 % |
c |     20091 |   55821   141564 |   22533   15736   137948     8.8 | 42.284 % |
c |     20316 |   55821   141564 |   24787   15961   140077     8.8 | 42.284 % |
c |     20653 |   55798   141513 |   27265   16294   142761     8.8 | 42.303 % |
c |     21159 |   55654   141163 |   29992   16784   151770     9.0 | 42.458 % |
c |     21919 |   55607   141055 |   32991   17537   163532     9.3 | 42.506 % |
c |     23060 |   55472   140747 |   36290   18619   183078     9.8 | 42.639 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23359 |   55240   140215 |   18413   18491   167058     9.0 | 42.639 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23414 |   55285   140331 |   18428   18546   167415     9.0 | 42.639 % |
c |     23514 |   55285   140331 |   20270   18646   169151     9.1 | 42.856 % |
c |     23664 |   55203   140128 |   22297   18783   170299     9.1 | 42.946 % |
c |     23889 |   55203   140128 |   24527   19008   176113     9.3 | 42.946 % |
c |     24226 |   55050   139772 |   26980   19326   178783     9.3 | 43.098 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24536 |   55077   139856 |   18359   19599   182380     9.3 | 43.098 % |
c |     24636 |   55020   139718 |   20194   19691   183095     9.3 | 43.237 % |
c |     24787 |   55020   139718 |   22214   19842   184176     9.3 | 43.237 % |
c |     25012 |   54943   139542 |   24435   20023   185413     9.3 | 43.311 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25285 |   54892   139420 |   18297   20250   187022     9.2 | 43.311 % |
c |     25386 |   54860   139343 |   20126   20339   187675     9.2 | 43.392 % |
c |     25536 |   54856   139334 |   22139   20485   188727     9.2 | 43.395 % |
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25562 |   54910   139472 |   18303   20511   189047     9.2 | 43.395 % |
c |     25662 |   54851   139321 |   20133   20605   189985     9.2 | 43.438 % |
c |     25813 |   54851   139321 |   22146   20756   190983     9.2 | 43.438 % |
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25998 |   54692   138950 |   18230   20613   180832     8.8 | 43.438 % |
c |     26098 |   54692   138950 |   20053   20713   181904     8.8 | 43.592 % |
c |     26250 |   54692   138950 |   22058   20865   183660     8.8 | 43.592 % |
c |     26475 |   54692   138950 |   24264   21090   185748     8.8 | 43.592 % |
c ==============================================================================
c [1mFound solution: 51[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26507 |   54735   139060 |   18245   21122   185987     8.8 | 43.592 % |
c |     26608 |   54735   139060 |   20069   21223   186912     8.8 | 43.577 % |
c |     26758 |   54735   139060 |   22076   21373   192762     9.0 | 43.577 % |
c |     26985 |   54657   138876 |   24284   21541   194539     9.0 | 43.661 % |
c ==============================================================================
c [1mFound solution: 46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27151 |   54653   138873 |   18217   21623   193380     8.9 | 43.661 % |
c |     27251 |   54628   138815 |   20038   21716   194695     9.0 | 43.736 % |
c ==============================================================================
c [1mFound solution: 45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27377 |   54671   138924 |   18223   21842   196533     9.0 | 43.736 % |
c |     27478 |   54671   138924 |   20045   21943   197469     9.0 | 43.728 % |
c |     27628 |   54667   138914 |   22049   22092   198901     9.0 | 43.731 % |
c |     27855 |   54667   138914 |   24254   22319   202381     9.1 | 43.731 % |
c ==============================================================================
c [1mFound solution: 44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27914 |   54459   138414 |   18153   22339   201624     9.0 | 43.731 % |
c |     28014 |   54420   138312 |   19968   22431   202883     9.0 | 43.985 % |
c |     28165 |   54412   138292 |   21965   22580   204442     9.1 | 43.991 % |
c |     28391 |   54377   138211 |   24161   22802   206693     9.1 | 44.033 % |
c ==============================================================================
c [1mFound solution: 43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28472 |   54412   138300 |   18137   22883   207208     9.1 | 44.033 % |
c ==============================================================================
c [1mFound solution: 42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28511 |   54341   138122 |   18113   22920   207630     9.1 | 44.033 % |
c |     28611 |   54231   137845 |   19924   23006   208957     9.1 | 44.207 % |
c |     28761 |   54222   137823 |   21916   23153   210966     9.1 | 44.220 % |
c ==============================================================================
c [1mFound solution: 41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28885 |   54228   137842 |   18076   23270   212436     9.1 | 44.220 % |
c |     28985 |   54228   137842 |   19883   23370   213483     9.1 | 44.246 % |
c |     29137 |   54228   137842 |   21871   23522   214726     9.1 | 44.246 % |
c |     29362 |   54205   137785 |   24059   23741   216921     9.1 | 44.271 % |
c ==============================================================================
c [1mFound solution: 40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29442 |   53881   137029 |   17960   23343   206316     8.8 | 44.271 % |
c |     29542 |   53881   137029 |   19756   23443   209979     9.0 | 44.589 % |
c |     29693 |   53881   137029 |   21731   23594   211927     9.0 | 44.589 % |
c |     29918 |   53827   136898 |   23904   23807   215183     9.0 | 44.650 % |
c |     30258 |   53823   136888 |   26295   24146   219787     9.1 | 44.653 % |
c ==============================================================================
c [1mFound solution: 39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30354 |   53845   136945 |   17948   24240   220431     9.1 | 44.653 % |
c |     30454 |   53845   136945 |   19742   24340   223088     9.2 | 44.654 % |
c |     30605 |   53845   136945 |   21717   24491   225166     9.2 | 44.654 % |
c ==============================================================================
c [1mFound solution: 38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30822 |   53808   136850 |   17936   24698   226964     9.2 | 44.654 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30840 |   53848   136950 |   17949   24716   227108     9.2 | 44.654 % |
c |     30944 |   53848   136950 |   19743   24820   228856     9.2 | 44.681 % |
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30982 |   53729   136662 |   17909   24777   226435     9.1 | 44.681 % |
c |     31082 |   53662   136506 |   19699   24874   227946     9.2 | 44.876 % |
c ==============================================================================
c [1mFound solution: 35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31100 |   53695   136589 |   17898   24892   228166     9.2 | 44.876 % |
c ==============================================================================
c [1mFound solution: 34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31162 |   53642   136448 |   17880   24842   223218     9.0 | 44.876 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31240 |   53681   136545 |   17893   24920   224472     9.0 | 44.876 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31258 |   51317   131058 |   17105   22095   169132     7.7 | 44.876 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31310 |   51300   131010 |   17100   22139   169504     7.7 | 44.876 % |
c |     31412 |   51279   130958 |   18810   22238   171492     7.7 | 47.391 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31470 |   51311   131037 |   17103   22296   172683     7.7 | 47.391 % |
c |     31571 |   51311   131037 |   18813   22397   175874     7.9 | 47.378 % |
c |     31722 |   51311   131037 |   20694   22548   178573     7.9 | 47.378 % |
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31942 |   51162   130681 |   17054   22706   180944     8.0 | 47.378 % |
c |     32044 |   51162   130681 |   18759   22808   183058     8.0 | 47.534 % |
c |     32194 |   51157   130666 |   20635   22956   185716     8.1 | 47.537 % |
c |     32419 |   51157   130666 |   22698   23181   188775     8.1 | 47.537 % |
c |     32756 |   51146   130643 |   24968   23502   192930     8.2 | 47.550 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33003 |   51174   130712 |   17058   23749   195879     8.2 | 47.550 % |
c |     33103 |   51174   130712 |   18763   23849   197513     8.3 | 47.538 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33138 |   51130   130598 |   17043   23833   196338     8.2 | 47.538 % |
c |     33238 |   51130   130598 |   18747   23933   198470     8.3 | 47.589 % |
c |     33388 |   51130   130598 |   20622   24083   201800     8.4 | 47.589 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33501 |   51154   130658 |   17051   24146   203397     8.4 | 47.589 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33535 |   50624   129413 |   16874   23898   199086     8.3 | 47.589 % |
c |     33635 |   50624   129413 |   18561   23998   200714     8.4 | 48.160 % |
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33647 |   50649   129475 |   16883   24010   200879     8.4 | 48.160 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33737 |   50608   129368 |   16869   24090   202027     8.4 | 48.160 % |
c |     33837 |   50608   129368 |   18555   24190   203474     8.4 | 48.201 % |
c |     33987 |   50608   129368 |   20411   24340   205871     8.5 | 48.201 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34091 |   50626   129412 |   16875   24443   207831     8.5 | 48.201 % |
c |     34191 |   50626   129412 |   18562   24543   209407     8.5 | 48.198 % |
c |     34341 |   50622   129402 |   20418   24692   211810     8.6 | 48.201 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34378 |   50369   128787 |   16789   24454   205302     8.4 | 48.201 % |
c |     34478 |   50369   128787 |   18467   24554   206640     8.4 | 48.482 % |
c |     34628 |   50364   128772 |   20314   24703   208852     8.5 | 48.485 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34694 |   50385   128823 |   16795   24769   209794     8.5 | 48.485 % |
c |     34795 |   50351   128737 |   18474   24866   210864     8.5 | 48.519 % |
c |     34946 |   50351   128737 |   20321   25017   212978     8.5 | 48.519 % |
c |     35171 |   50351   128737 |   22354   25242   216169     8.6 | 48.519 % |
c |     35508 |   50341   128707 |   24589   25577   220541     8.6 | 48.525 % |
c |     36014 |   49733   127266 |   27048   25684   220632     8.6 | 49.189 % |
c |     36773 |   49733   127266 |   29753   26443   231395     8.8 | 49.189 % |
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              : 125
c conflicts             : 37874          (353 /sec)
c decisions             : 186356         (1735 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 107.383 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.62 0.90 0.87 2/54 22278
Raw data (stat): 22278 (runsolver) R 22277 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481314787 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.67 0.90 0.87 2/54 22278
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 2432 0 0 0 992 6 0 0 25 0 1 0 481314787 11882496 2357 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2901 2357 603 41 0 2860 0
vsize: 11604
[startup+20.0003 s]
Raw data (loadavg): 0.72 0.90 0.87 2/54 22278
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 2437 0 0 0 1992 6 0 0 25 0 1 0 481314787 12029952 2362 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2362 603 41 0 2896 0
vsize: 11748
[startup+30.0006 s]
Raw data (loadavg): 0.77 0.90 0.87 2/54 22278
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 2449 0 0 0 2992 6 0 0 25 0 1 0 481314787 12029952 2374 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2374 603 41 0 2896 0
vsize: 11748
[startup+40.0005 s]
Raw data (loadavg): 0.80 0.91 0.87 2/54 22278
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3134 0 0 0 3989 9 0 0 25 0 1 0 481314787 14585856 2976 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3561 2976 603 41 0 3520 0
vsize: 14244
[startup+50.0014 s]
Raw data (loadavg): 0.83 0.91 0.87 2/54 22278
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3204 0 0 0 4989 9 0 0 25 0 1 0 481314787 14856192 3046 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3627 3046 603 41 0 3586 0
vsize: 14508
[startup+60.0011 s]
Raw data (loadavg): 0.86 0.91 0.87 2/54 22280
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3338 0 0 0 5987 10 0 0 25 0 1 0 481314787 15413248 3180 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3763 3180 603 41 0 3722 0
vsize: 15052
[startup+70.0009 s]
Raw data (loadavg): 0.88 0.91 0.87 2/54 22280
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3379 0 0 0 6986 11 0 0 25 0 1 0 481314787 15523840 3221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3790 3221 603 41 0 3749 0
vsize: 15160
[startup+80.0019 s]
Raw data (loadavg): 0.90 0.92 0.87 2/54 22280
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3441 0 0 0 7986 12 0 0 25 0 1 0 481314787 15761408 3283 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3848 3283 603 41 0 3807 0
vsize: 15392
[startup+90.0013 s]
Raw data (loadavg): 0.91 0.92 0.88 2/54 22280
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3446 0 0 0 8986 12 0 0 25 0 1 0 481314787 15761408 3288 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3848 3288 603 41 0 3807 0
vsize: 15392
[startup+100.001 s]
Raw data (loadavg): 0.93 0.92 0.88 2/54 22280
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3461 0 0 0 9985 13 0 0 25 0 1 0 481314787 15880192 3303 4294967295 134512640 134672761 3221224544 3221223680 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3877 3303 603 41 0 3836 0
vsize: 15508
[startup+107.571 s]
Raw data (loadavg): 0.94 0.92 0.88 1/53 22280
Raw data (stat): 22278 (minisat+) R 22277 32461 32460 0 -1 0 3461 0 0 0 9985 13 0 0 25 0 1 0 481314787 15880192 3303 4294967295 134512640 134672761 3221224544 3221223680 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3877 3303 603 41 0 3836 0
vsize: 0

Child status: 30
Real time (s): 107.571
CPU time (s): 107.546
CPU user time (s): 107.403
CPU system time (s): 0.142978
CPU usage (%): 99.9768
Max. virtual memory (Kb): 15508
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	19
#### END VERIFIER DATA ####