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 20592

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 21:29:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14648 boxname=wulflinc26 idbench=1127 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3fce91583b30a82646d8d8e778b97a89  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-neos1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-neos1.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-neos1.opb
IDLAUNCH: 14648
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        377584 kB
Buffers:         34312 kB
Cached:         594620 kB
SwapCached:         68 kB
Active:         175488 kB
Inactive:       456316 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        377332 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6880 kB
Slab:            19348 kB
Committed_AS:    63720 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 21:49:52 (client local time) WITH STATUS 10 IN 1200.33 SECONDS
stats: 14648 7 1200.33 10
#### 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]---> Adder-cost: 61   maxlim: 15   bits: 5/4
c ---[5116]---> Adder-cost: 44   maxlim: 11   bits: 5/4
c ---[5114]---> Adder-cost: 44   maxlim: 11   bits: 5/4
c ---[5112]---> Adder-cost: 61   maxlim: 15   bits: 5/4
c ---[5110]---> Adder-cost: 61   maxlim: 15   bits: 5/4
c ---[5108]---> Adder-cost: 61   maxlim: 15   bits: 5/4
c ---[5106]---> Adder-cost: 44   maxlim: 11   bits: 5/4
c ---[5104]---> Adder-cost: 44   maxlim: 11   bits: 5/4
c ---[5102]---> Adder-cost: 61   maxlim: 15   bits: 5/4
c ---[5100]---> Adder-cost: 61   maxlim: 15   bits: 5/4
c ---[5098]---> Adder-cost: 62   maxlim: 17   bits: 6/5
c ---[5096]---> Adder-cost: 44   maxlim: 13   bits: 5/4
c ---[5094]---> Adder-cost: 44   maxlim: 13   bits: 5/4
c ---[5092]---> Adder-cost: 44   maxlim: 13   bits: 5/4
c ---[5090]---> Adder-cost: 62   maxlim: 17   bits: 6/5
c ---[5088]---> Adder-cost: 62   maxlim: 17   bits: 6/5
c ---[5086]---> Adder-cost: 44   maxlim: 13   bits: 5/4
c ---[5084]---> Adder-cost: 44   maxlim: 13   bits: 5/4
c ---[5082]---> Adder-cost: 44   maxlim: 13   bits: 5/4
c ---[5080]---> Adder-cost: 62   maxlim: 17   bits: 6/5
c ---[5078]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5076]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5074]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5072]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5070]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[5068]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5066]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5064]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[5062]---> Adder-cost: 60   maxlim: 16   bits: 6/5
c ---[5060]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5058]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5056]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5054]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5052]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5050]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[5048]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5046]---> Adder-cost: 60   maxlim: 16   bits: 6/5
c ---[5044]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5042]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5040]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5038]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[5036]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5034]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5032]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5030]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5028]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5026]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5024]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5022]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[5020]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5018]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5016]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5014]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5012]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5010]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[5008]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[5006]---> Adder-cost: 40   maxlim: 12   bits: 5/4
c ---[5004]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[5002]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[5000]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4998]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4996]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4994]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4992]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4990]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[4988]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4986]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4984]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[4982]---> Adder-cost: 60   maxlim: 16   bits: 6/5
c ---[4980]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4978]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4976]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4974]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4972]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4970]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[4968]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4966]---> Adder-cost: 60   maxlim: 16   bits: 6/5
c ---[4964]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4962]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4960]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4958]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[4956]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4954]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4952]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4950]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4948]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4946]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4944]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4942]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[4940]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4938]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4936]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4934]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4932]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4930]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4928]---> Adder-cost: 42   maxlim: 12   bits: 5/4
c ---[4926]---> Adder-cost: 40   maxlim: 12   bits: 5/4
c ---[4924]---> Adder-cost: 58   maxlim: 16   bits: 6/5
c ---[4922]---> Adder-cost: 44   maxlim: 12   bits: 5/4
c ---[4920]---> Adder-cost: 62   maxlim: 16   bits: 6/5
c ---[4919]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4918]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4917]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4916]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4915]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4914]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4913]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4912]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4911]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4910]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4909]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4908]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4907]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4906]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4905]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4904]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4903]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4902]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4901]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4900]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4899]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4898]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4897]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4896]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4895]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4894]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4893]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4892]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4891]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4890]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4889]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4888]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4887]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4886]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4885]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4884]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4883]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4882]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4881]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4880]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4879]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4878]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4877]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4876]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4875]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4874]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4873]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4872]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4871]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4870]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4869]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4868]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4867]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4866]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4865]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4864]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4863]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4862]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4861]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4860]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4859]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4858]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4857]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4856]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4855]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4854]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4853]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4852]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4851]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4850]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4849]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4848]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4847]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4846]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4845]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4844]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4843]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4842]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4841]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4840]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4839]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4838]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4837]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4836]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4835]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4834]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4833]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4832]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4831]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4830]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4829]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4828]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4827]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4826]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4825]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4824]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4823]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4822]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4821]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4820]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4819]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4818]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4817]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4816]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4815]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4814]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4813]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4812]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4811]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4810]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4809]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4808]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4807]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4806]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4805]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4804]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4803]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4802]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4801]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4800]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4799]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4798]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4797]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4796]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4795]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4794]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4793]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4792]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4791]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4790]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4789]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4788]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4787]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4786]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4785]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4784]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4783]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4782]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4781]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4780]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4779]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4778]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4777]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4776]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4775]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[4774]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4773]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4772]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4771]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4770]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4769]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4768]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4767]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4766]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4765]---> Adder-cost: 23   maxlim: 14   bits: 5/4
c ---[4764]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4763]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4762]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4761]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4760]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4759]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4758]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4757]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4756]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4755]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4754]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4753]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4752]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4751]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4750]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4749]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4748]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4747]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4746]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4745]---> Adder-cost: 27   maxlim: 14   bits: 5/4
c ---[4744]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4743]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4742]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4741]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4740]---> Adder-cost: 0   maxlim: 14   bits: 5/4
c ---[4739]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4738]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4737]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4736]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4735]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4734]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4733]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4732]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4731]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4730]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4729]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4728]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4727]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4726]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4725]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4724]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4723]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4722]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4721]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4720]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4719]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4718]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4717]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4716]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4715]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4714]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4713]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4712]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4711]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4710]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4709]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4708]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4707]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4706]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4705]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4704]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4703]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4702]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4701]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4700]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4699]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4698]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4697]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4696]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4695]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4694]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4693]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4692]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4691]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4690]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4689]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4688]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4687]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4686]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4685]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4684]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4683]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4682]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4681]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4680]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4679]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4678]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4677]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4676]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4675]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4674]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4673]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4672]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4671]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4670]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4669]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4668]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4667]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4666]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4665]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4664]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4663]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4662]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4661]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4660]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4659]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4658]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4657]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4656]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4655]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4654]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4653]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4652]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4651]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4650]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4649]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4648]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4647]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4646]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4645]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4644]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4643]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4642]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4641]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4640]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4639]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4638]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4637]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4636]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4635]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4634]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4633]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4632]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4631]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4630]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4629]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4628]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4627]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4626]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4625]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4624]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4623]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4622]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4621]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4620]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4619]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4618]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4617]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4616]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4615]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4614]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4613]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4612]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4611]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4610]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4609]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4608]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4607]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4606]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4605]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4604]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4603]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4602]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4601]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4600]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4599]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4598]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4597]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4596]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4451]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4450]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4449]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4448]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4447]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4446]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4445]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4444]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4443]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4442]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4441]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4440]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4439]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4438]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4437]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4436]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4435]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4434]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4433]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4432]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4431]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4430]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4429]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4428]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4427]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4426]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4425]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4424]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4423]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4422]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4421]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4420]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4419]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4418]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4417]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4416]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4415]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4414]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4413]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4412]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4411]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4410]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4409]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4408]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4407]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4406]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4405]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4404]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4403]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4402]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4401]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4400]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4399]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4398]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4397]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4396]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4395]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4394]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4393]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4392]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4391]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4390]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4389]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4388]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4387]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4386]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4385]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4384]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4383]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4382]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4381]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4380]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4379]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4378]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4377]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4376]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4375]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4374]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4373]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4372]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4371]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4370]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4369]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4368]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4367]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4366]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4365]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4364]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4363]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4362]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4361]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4360]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4359]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4358]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4357]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4356]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4355]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4354]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4353]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4352]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4351]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4350]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4349]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4348]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4347]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4346]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4345]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4344]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4343]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4342]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4341]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4340]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4339]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4338]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4337]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4336]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4335]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4334]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4333]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4332]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4331]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4330]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4329]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4328]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4327]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4326]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4325]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4324]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4323]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4322]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4321]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4320]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4319]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4318]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4317]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4316]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4315]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4314]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4313]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4312]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4311]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4310]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4309]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4308]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4307]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4306]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4305]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4304]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4303]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4302]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4301]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4300]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4299]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4298]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4297]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4296]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4295]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4294]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4293]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4292]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4291]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4290]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4289]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4288]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4287]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4286]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4285]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4284]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4283]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4282]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4281]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4280]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4279]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4278]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4277]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4276]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4275]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4274]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4273]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4272]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4271]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4270]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4269]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4268]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4267]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4266]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4265]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4264]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4263]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4262]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4261]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4260]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4259]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4258]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4257]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4256]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4255]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4254]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4253]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4252]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4251]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4250]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4249]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4248]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4247]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4246]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4245]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4244]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4243]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4242]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4241]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4240]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4239]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4238]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4237]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4236]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4235]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4234]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4233]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4232]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4231]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4230]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4229]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4228]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4227]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4226]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4225]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4224]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4223]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4222]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4221]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4220]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4219]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4218]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4217]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4216]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4215]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4214]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4213]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4212]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4211]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4210]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4209]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4208]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4207]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4206]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4205]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4204]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4203]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4202]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4201]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4200]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4199]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4198]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4197]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4196]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4195]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4194]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4193]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4192]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4191]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4190]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4189]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4188]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4187]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4186]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4185]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4184]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4183]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4182]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4181]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4180]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4179]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4178]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4177]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4176]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4175]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4174]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4173]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4172]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4171]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4170]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4169]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4168]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4167]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4166]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4165]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4164]---> Adder-cost: 10   maxlim: 5   bits: 4/3
c ---[4163]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4162]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4161]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4160]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4159]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4158]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4157]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4156]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4155]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4154]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4153]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4152]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4151]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4150]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4149]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4148]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4147]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4146]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4145]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4144]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4143]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4142]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4141]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4140]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4139]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4138]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4137]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4136]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4135]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4134]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4133]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4132]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4131]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4130]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4129]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4128]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4127]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4126]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4125]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4124]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4123]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4122]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4121]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4120]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4119]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4118]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4117]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4116]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4115]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4114]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4113]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4112]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4111]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4110]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4109]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4108]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4107]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4106]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4105]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4104]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4103]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4102]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4101]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4100]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4099]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4098]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4097]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4096]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4095]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4094]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4093]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4092]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4091]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4090]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4089]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4088]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4087]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4086]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4085]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4084]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4083]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4082]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4081]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4080]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4079]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4078]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4077]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4076]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4075]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4074]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4073]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4072]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4071]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4070]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4069]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4068]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4067]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4066]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4065]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4064]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4063]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4062]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4061]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4060]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4059]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4058]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4057]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4056]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4055]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4054]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4053]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4052]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4051]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4050]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4049]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4048]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4047]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4046]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4045]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4044]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4043]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4042]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4041]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4040]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4039]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4038]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4037]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4036]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4035]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4034]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4033]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4032]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4031]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4030]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4029]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4028]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4027]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4026]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4025]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4024]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4023]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4022]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4021]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[4020]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[3875]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3874]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3873]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3872]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3871]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3870]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3869]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3868]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3867]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3866]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3865]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3864]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3863]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3862]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3861]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3860]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3859]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3858]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3857]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3856]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3855]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3854]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3853]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3852]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3851]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3850]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3849]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3848]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3847]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3846]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3845]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3844]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3843]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3842]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3841]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[3840]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   82484   281624 |   27494       0        0     nan |  0.000 % |
c |       100 |   82470   281580 |   30243      98      428     4.4 | 14.611 % |
c |       250 |   82461   281549 |   33267     245     1243     5.1 | 14.617 % |
c |       475 |   82434   281466 |   36594     466     2293     4.9 | 14.640 % |
c |       812 |   82347   281180 |   40253     788     4151     5.3 | 14.719 % |
c |      1318 |   82300   281022 |   44279    1283     6985     5.4 | 14.759 % |
c |      2077 |   82198   280678 |   48707    2021    10713     5.3 | 14.833 % |
c |      3216 |   82090   280332 |   53578    3141    16546     5.3 | 14.935 % |
c |      4925 |   81453   278210 |   58935    4594    24609     5.4 | 15.464 % |
c |      7487 |   81029   276771 |   64829    6933    44249     6.4 | 15.766 % |
c |     11331 |   80279   274239 |   71312   10356    77536     7.5 | 16.380 % |
c |     17097 |   79422   271353 |   78443   15345   141085     9.2 | 17.085 % |
c |     25746 |   78911   269627 |   86287   23512   326575    13.9 | 17.477 % |
c |     38720 |   77547   265037 |   94916   31457   365492    11.6 | 18.568 % |
c |     58182 |   76173   260387 |  104408   48667   678521    13.9 | 19.671 % |
c |     87374 |   73084   249833 |  114849   74494  1145636    15.4 | 21.872 % |
c ==============================================================================
c [1mFound solution: 67[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 548   maxlim: 221   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115584 |   74315   254654 |   24771   99175  1545992    15.6 | 21.872 % |
c |    115684 |   74315   254654 |   27248   27787   301718    10.9 | 23.057 % |
c |    115835 |   74310   254638 |   29972   27936   303966    10.9 | 23.063 % |
c |    116061 |   74310   254638 |   32970   28162   306619    10.9 | 23.063 % |
c |    116398 |   74303   254615 |   36267   28497   312779    11.0 | 23.068 % |
c |    116904 |   74204   254268 |   39893   28999   318579    11.0 | 23.101 % |
c |    117665 |   74197   254245 |   43883   29757   329295    11.1 | 23.107 % |
c |    118809 |   74181   254191 |   48271   30895   348392    11.3 | 23.118 % |
c |    120517 |   74167   254145 |   53098   32594   379047    11.6 | 23.129 % |
c |    123079 |   73993   253544 |   58408   35111   427746    12.2 | 23.217 % |
c |    126923 |   73840   253005 |   64249   38851   489568    12.6 | 23.283 % |
c |    132694 |   73742   252670 |   70674   44602   608042    13.6 | 23.344 % |
c |    141343 |   73623   252253 |   77742   53199   782194    14.7 | 23.393 % |
c ==============================================================================
c [1mFound solution: 65[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 223   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    143785 |   73540   251977 |   24513   55627   836019    15.0 | 23.393 % |
c |    143885 |   73540   251977 |   26964   27914   329296    11.8 | 23.464 % |
c |    144035 |   73540   251977 |   29660   28064   331111    11.8 | 23.464 % |
c |    144262 |   73540   251977 |   32626   28291   335243    11.8 | 23.464 % |
c |    144599 |   73540   251977 |   35889   28628   340328    11.9 | 23.464 % |
c |    145105 |   73540   251977 |   39478   29134   349682    12.0 | 23.464 % |
c |    145864 |   73422   251555 |   43426   29865   365128    12.2 | 23.502 % |
c |    147004 |   73416   251535 |   47768   31003   383229    12.4 | 23.508 % |
c |    148712 |   73402   251489 |   52545   32704   410485    12.6 | 23.519 % |
c |    151274 |   73395   251466 |   57800   35265   479844    13.6 | 23.524 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 225   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    152876 |   73391   251460 |   24463   36858   511248    13.9 | 23.524 % |
c |    152976 |   73391   251460 |   26909   18529   186379    10.1 | 23.534 % |
c |    153128 |   73391   251460 |   29600   18681   188325    10.1 | 23.534 % |
c |    153353 |   73391   251460 |   32560   18906   190912    10.1 | 23.534 % |
c |    153691 |   73391   251460 |   35816   19244   195202    10.1 | 23.534 % |
c |    154197 |   73382   251429 |   39397   19746   202824    10.3 | 23.539 % |
c |    154957 |   73382   251429 |   43337   20506   219371    10.7 | 23.539 % |
c |    156098 |   73375   251406 |   47671   21643   234726    10.8 | 23.545 % |
c |    157806 |   73164   250657 |   52438   23314   261097    11.2 | 23.622 % |
c |    160373 |   73164   250657 |   57682   25881   351237    13.6 | 23.622 % |
c |    164217 |   73157   250634 |   63450   29720   459528    15.5 | 23.628 % |
c |    169983 |   73066   250326 |   69795   35472   649221    18.3 | 23.694 % |
c ==============================================================================
c [1mFound solution: 61[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 227   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175852 |   72872   249669 |   24290   41306   799969    19.4 | 23.694 % |
c |    175954 |   72872   249669 |   26719   20755   333740    16.1 | 23.858 % |
c |    176104 |   72872   249669 |   29390   20905   335995    16.1 | 23.858 % |
c |    176329 |   72872   249669 |   32329   21130   338989    16.0 | 23.858 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 230   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    176458 |   72878   249700 |   24292   21259   340646    16.0 | 23.858 % |
c |    176560 |   72878   249700 |   26721   21361   341582    16.0 | 23.865 % |
c |    176710 |   72878   249700 |   29393   21511   344373    16.0 | 23.865 % |
c |    176938 |   72878   249700 |   32332   21739   348021    16.0 | 23.865 % |
c |    177276 |   72878   249700 |   35565   22077   352623    16.0 | 23.865 % |
c |    177784 |   72833   249543 |   39122   22580   359756    15.9 | 23.887 % |
c |    178543 |   72784   249366 |   43034   23332   370609    15.9 | 23.909 % |
c |    179683 |   72695   249049 |   47338   24453   387839    15.9 | 23.942 % |
c |    181391 |   72641   248857 |   52072   26145   416201    15.9 | 23.959 % |
c |    183953 |   72595   248702 |   57279   28681   471802    16.4 | 23.997 % |
c |    187797 |   72595   248702 |   63007   32525   604108    18.6 | 23.997 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 233   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188266 |   72597   248718 |   24199   32994   612416    18.6 | 23.997 % |
c |    188366 |   72597   248718 |   26618   16597   217105    13.1 | 24.006 % |
c |    188518 |   72597   248718 |   29280   16749   219477    13.1 | 24.006 % |
c |    188745 |   72597   248718 |   32208   16976   222356    13.1 | 24.006 % |
c |    189082 |   72568   248621 |   35429   17306   225834    13.0 | 24.055 % |
c |    189588 |   72568   248621 |   38972   17812   235045    13.2 | 24.055 % |
c |    190347 |   72568   248621 |   42870   18571   250735    13.5 | 24.055 % |
c |    191486 |   72568   248621 |   47157   19710   284032    14.4 | 24.055 % |
c |    193197 |   72568   248621 |   51872   21421   332075    15.5 | 24.055 % |
c |    195760 |   72421   248106 |   57059   23960   379039    15.8 | 24.105 % |
c |    199604 |   72340   247826 |   62765   27794   489349    17.6 | 24.138 % |
c |    205374 |   72324   247772 |   69042   33560   662380    19.7 | 24.149 % |
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 235   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    209401 |   72289   247656 |   24096   37580   762349    20.3 | 24.149 % |
c |    209501 |   72289   247656 |   26505   18890   275870    14.6 | 24.164 % |
c |    209651 |   72289   247656 |   29156   19040   278597    14.6 | 24.164 % |
c |    209876 |   72289   247656 |   32071   19265   283056    14.7 | 24.164 % |
c |    210214 |   72289   247656 |   35278   19603   287731    14.7 | 24.164 % |
c |    210721 |   72283   247639 |   38806   20109   294212    14.6 | 24.169 % |
c |    211480 |   72185   247303 |   42687   20863   309799    14.8 | 24.230 % |
c |    212620 |   72185   247303 |   46956   22003   347213    15.8 | 24.230 % |
c |    214328 |   72185   247303 |   51651   23711   395655    16.7 | 24.230 % |
c |    216890 |   72185   247303 |   56817   26273   486505    18.5 | 24.230 % |
c |    220734 |   72185   247303 |   62498   30117   645526    21.4 | 24.230 % |
c |    226500 |   72086   246954 |   68748   35872   857887    23.9 | 24.269 % |
c ==============================================================================
c [1mFound solution: 50[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 238   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    234255 |   72068   246903 |   24022   43616  1246458    28.6 | 24.269 % |
c |    234355 |   72068   246903 |   26424   21908   570429    26.0 | 24.291 % |
c |    234505 |   72068   246903 |   29066   22058   571786    25.9 | 24.291 % |
c |    234730 |   72068   246903 |   31973   22283   576298    25.9 | 24.291 % |
c |    235067 |   72068   246903 |   35170   22620   581611    25.7 | 24.291 % |
c |    235573 |   72068   246903 |   38687   23126   591120    25.6 | 24.291 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 251   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    235825 |   72072   246926 |   24024   23378   595611    25.5 | 24.291 % |
c |    235926 |   72072   246926 |   26426   23479   597308    25.4 | 24.302 % |
c |    236076 |   72072   246926 |   29069   23629   600275    25.4 | 24.302 % |
c |    236301 |   72072   246926 |   31975   23854   603396    25.3 | 24.302 % |
c |    236640 |   72072   246926 |   35173   24193   610819    25.2 | 24.302 % |
c |    237146 |   72072   246926 |   38690   24699   617622    25.0 | 24.302 % |
c |    237905 |   72072   246926 |   42559   25458   628079    24.7 | 24.302 % |
c |    239044 |   72072   246926 |   46815   26597   662762    24.9 | 24.302 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 255   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    240112 |   72020   246683 |   24006   27557   690288    25.0 | 24.302 % |
c |    240212 |   72020   246683 |   26406   27657   691360    25.0 | 24.352 % |
c |    240363 |   72020   246683 |   29047   27808   695926    25.0 | 24.352 % |
c |    240590 |   72020   246683 |   31951   28035   700978    25.0 | 24.352 % |
c |    240927 |   72020   246683 |   35147   28372   710766    25.1 | 24.352 % |
c |    241433 |   72020   246683 |   38661   28878   738001    25.6 | 24.352 % |
c |    242192 |   72013   246660 |   42528   29636   762027    25.7 | 24.357 % |
c |    243334 |   71983   246554 |   46780   30774   806159    26.2 | 24.368 % |
c |    245043 |   71983   246554 |   51458   32483   904348    27.8 | 24.368 % |
c |    247607 |   71983   246554 |   56604   35047  1005080    28.7 | 24.368 % |
c |    251452 |   71983   246554 |   62265   38892  1165754    30.0 | 24.368 % |
c |    257221 |   71968   246503 |   68491   44657  1530749    34.3 | 24.379 % |
c |    265870 |   71953   246454 |   75341   53301  2242091    42.1 | 24.390 % |
c |    278844 |   71913   246312 |   82875   66269  3178617    48.0 | 24.412 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 259   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    283453 |   71915   246319 |   23971   70878  3422527    48.3 | 24.412 % |
c |    283553 |   71915   246319 |   26368   24880   900543    36.2 | 24.415 % |
c |    283703 |   71915   246319 |   29004   25030   903157    36.1 | 24.415 % |
c |    283928 |   71915   246319 |   31905   25255   907727    35.9 | 24.415 % |
c |    284266 |   71915   246319 |   35095   25593   912136    35.6 | 24.415 % |
c |    284775 |   71915   246319 |   38605   26102   936172    35.9 | 24.415 % |
c |    285534 |   71907   246293 |   42466   26860   950123    35.4 | 24.420 % |
c |    286673 |   71901   246276 |   46712   27998   997922    35.6 | 24.426 % |
c |    288381 |   71901   246276 |   51383   29706  1059580    35.7 | 24.426 % |
c |    290943 |   71814   245976 |   56522   32259  1134883    35.2 | 24.454 % |
c |    294789 |   71781   245859 |   62174   36103  1394020    38.6 | 24.465 % |
c |    300555 |   71773   245834 |   68392   41868  1670673    39.9 | 24.476 % |
c |    309204 |   71773   245834 |   75231   50517  2332888    46.2 | 24.476 % |
c |    322179 |   71767   245817 |   82754   63491  3186929    50.2 | 24.481 % |
c |    341642 |   71767   245817 |   91029   82954  4463944    53.8 | 24.481 % |
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 260   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    352700 |   71742   245732 |   23914   94009  5274093    56.1 | 24.481 % |
c |    352800 |   71742   245732 |   26305   26046   979038    37.6 | 24.491 % |
c |    352951 |   71742   245732 |   28935   26197   980788    37.4 | 24.491 % |
c |    353176 |   71736   245715 |   31829   26420   983114    37.2 | 24.496 % |
c |    353513 |   71736   245715 |   35012   26757   993375    37.1 | 24.496 % |
c |    354019 |   71736   245715 |   38513   27263  1027685    37.7 | 24.496 % |
c |    354784 |   71736   245715 |   42365   28028  1063219    37.9 | 24.496 % |
c |    355923 |   71736   245715 |   46601   29167  1122961    38.5 | 24.496 % |
c |    357632 |   71729   245692 |   51261   30873  1213219    39.3 | 24.502 % |
c |    360194 |   71642   245380 |   56387   33428  1389566    41.6 | 24.535 % |
c |    364043 |   71642   245380 |   62026   37277  1632797    43.8 | 24.535 % |
c |    369811 |   71635   245357 |   68229   43044  2011144    46.7 | 24.540 % |
c |    378462 |   71612   245281 |   75052   51690  2556868    49.5 | 24.562 % |
c |    391436 |   71605   245258 |   82557   64663  3304291    51.1 | 24.568 % |
c |    410897 |   71559   245092 |   90813   84099  4619518    54.9 | 24.590 % |
c |    440090 |   71559   245092 |   99894   36463  2139695    58.7 | 24.590 % |
c |    483879 |   71550   245063 |  109884   80251  4764235    59.4 | 24.601 % |
c |    549564 |   71372   244457 |  120872   53467  2638306    49.3 | 24.711 % |
c |    648091 |   71155   243687 |  132959   51893  3092722    59.6 | 24.816 % |
c 
c *** TERMINATED ***
s SATISFIABLE
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_bit#### 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.71 0.90 0.89 2/54 10464
Raw data (stat): 10464 (runsolver) R 10463 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548334884 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99967 s]
Raw data (loadavg): 0.75 0.90 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 2237 0 0 0 994 4 0 0 25 0 1 0 548334884 11800576 2208 4294967295 134512640 134672761 3221224544 3221223712 134564752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2881 2208 603 41 0 2840 0
vsize: 11524
[startup+20.0004 s]
Raw data (loadavg): 0.79 0.90 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 2619 0 0 0 1992 6 0 0 25 0 1 0 548334884 13393920 2590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2590 603 41 0 3229 0
vsize: 13080
[startup+30.0023 s]
Raw data (loadavg): 0.82 0.91 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 2753 0 0 0 2992 6 0 0 25 0 1 0 548334884 13799424 2724 4294967295 134512640 134672761 3221224544 3221223696 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3369 2724 603 41 0 3328 0
vsize: 13476
[startup+40.0027 s]
Raw data (loadavg): 0.85 0.91 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 3013 0 0 0 3990 7 0 0 25 0 1 0 548334884 14995456 2984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3661 2984 603 41 0 3620 0
vsize: 14644
[startup+50.0201 s]
Raw data (loadavg): 0.87 0.91 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 3220 0 0 0 4991 8 0 0 25 0 1 0 548334884 15798272 3191 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3857 3191 603 41 0 3816 0
vsize: 15428
[startup+60.0201 s]
Raw data (loadavg): 0.89 0.91 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 3364 0 0 0 5989 8 0 0 25 0 1 0 548334884 16470016 3335 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4021 3335 603 41 0 3980 0
vsize: 16084
[startup+70.0207 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 3554 0 0 0 6988 9 0 0 25 0 1 0 548334884 17137664 3525 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4184 3525 603 41 0 4143 0
vsize: 16736
[startup+80.0248 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 3741 0 0 0 7988 10 0 0 25 0 1 0 548334884 18198528 3712 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4443 3712 603 41 0 4402 0
vsize: 17772
[startup+90.0253 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 3857 0 0 0 8988 10 0 0 25 0 1 0 548334884 18595840 3828 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4540 3828 603 41 0 4499 0
vsize: 18160
[startup+100.025 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 3993 0 0 0 9986 11 0 0 25 0 1 0 548334884 19132416 3964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4671 3964 603 41 0 4630 0
vsize: 18684
[startup+110.025 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4110 0 0 0 10986 12 0 0 25 0 1 0 548334884 19673088 4081 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4803 4081 603 41 0 4762 0
vsize: 19212
[startup+120.025 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4253 0 0 0 11985 13 0 0 25 0 1 0 548334884 20209664 4224 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4224 603 41 0 4893 0
vsize: 19736
[startup+130.025 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4420 0 0 0 12985 13 0 0 25 0 1 0 548334884 20881408 4391 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5098 4391 603 41 0 5057 0
vsize: 20392
[startup+140.025 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4562 0 0 0 13984 14 0 0 25 0 1 0 548334884 21417984 4533 4294967295 134512640 134672761 3221224544 3221223680 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5229 4533 603 41 0 5188 0
vsize: 20916
[startup+150.025 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4669 0 0 0 14984 14 0 0 25 0 1 0 548334884 21815296 4640 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5326 4640 603 41 0 5285 0
vsize: 21304
[startup+160.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4669 0 0 0 15984 14 0 0 25 0 1 0 548334884 21815296 4640 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5326 4640 603 41 0 5285 0
vsize: 21304
[startup+170.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4669 0 0 0 16984 14 0 0 25 0 1 0 548334884 21815296 4640 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5326 4640 603 41 0 5285 0
vsize: 21304
[startup+180.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 17984 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+190.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 18985 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+200.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 19985 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+210.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 20985 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+220.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 21985 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+230.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 22985 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+240.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 23985 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+250.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 24985 15 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+260.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 25985 16 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+270.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4687 0 0 0 26985 16 0 0 25 0 1 0 548334884 21958656 4658 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4658 603 41 0 5320 0
vsize: 21444
[startup+280.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 4888 0 0 0 27985 16 0 0 25 0 1 0 548334884 22757376 4859 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5556 4859 603 41 0 5515 0
vsize: 22224
[startup+290.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 5343 0 0 0 28984 17 0 0 25 0 1 0 548334884 24637440 5314 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6015 5314 603 41 0 5974 0
vsize: 24060
[startup+300.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 5755 0 0 0 29983 19 0 0 25 0 1 0 548334884 26378240 5726 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6440 5726 603 41 0 6399 0
vsize: 25760
[startup+310.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6290 0 0 0 30981 21 0 0 25 0 1 0 548334884 28528640 6261 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6965 6261 603 41 0 6924 0
vsize: 27860
[startup+320.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6645 0 0 0 31980 22 0 0 25 0 1 0 548334884 29995008 6616 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7323 6616 603 41 0 7282 0
vsize: 29292
[startup+330.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6810 0 0 0 32979 22 0 0 25 0 1 0 548334884 30666752 6781 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7487 6781 603 41 0 7446 0
vsize: 29948
[startup+340.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6810 0 0 0 33979 22 0 0 25 0 1 0 548334884 30666752 6781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7487 6781 603 41 0 7446 0
vsize: 29948
[startup+350.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6810 0 0 0 34979 22 0 0 25 0 1 0 548334884 30666752 6781 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7487 6781 603 41 0 7446 0
vsize: 29948
[startup+360.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6810 0 0 0 35979 23 0 0 25 0 1 0 548334884 30666752 6781 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7487 6781 603 41 0 7446 0
vsize: 29948
[startup+370.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6810 0 0 0 36980 23 0 0 25 0 1 0 548334884 30666752 6781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7487 6781 603 41 0 7446 0
vsize: 29948
[startup+380.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 6960 0 0 0 37979 23 0 0 25 0 1 0 548334884 31199232 6931 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7617 6931 603 41 0 7576 0
vsize: 30468
[startup+390.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 7440 0 0 0 38978 25 0 0 25 0 1 0 548334884 33214464 7411 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8109 7411 603 41 0 8068 0
vsize: 32436
[startup+400.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 7860 0 0 0 39976 26 0 0 25 0 1 0 548334884 34959360 7831 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8535 7831 603 41 0 8494 0
vsize: 34140
[startup+410.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8250 0 0 0 40975 28 0 0 25 0 1 0 548334884 36597760 8221 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8935 8221 603 41 0 8894 0
vsize: 35740
[startup+420.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8642 0 0 0 41973 30 0 0 25 0 1 0 548334884 38199296 8613 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9326 8613 603 41 0 9285 0
vsize: 37304
[startup+430.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8962 0 0 0 42972 31 0 0 25 0 1 0 548334884 39546880 8933 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9655 8933 603 41 0 9614 0
vsize: 38620
[startup+440.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8992 0 0 0 43972 31 0 0 25 0 1 0 548334884 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8963 603 41 0 9646 0
vsize: 38748
[startup+450.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8992 0 0 0 44972 32 0 0 25 0 1 0 548334884 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8963 603 41 0 9646 0
vsize: 38748
[startup+460.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8992 0 0 0 45972 32 0 0 25 0 1 0 548334884 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8963 603 41 0 9646 0
vsize: 38748
[startup+470.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8992 0 0 0 46972 32 0 0 25 0 1 0 548334884 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8963 603 41 0 9646 0
vsize: 38748
[startup+480.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8992 0 0 0 47972 32 0 0 25 0 1 0 548334884 39677952 8963 4294967295 134512640 134672761 3221224544 3221223728 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8963 603 41 0 9646 0
vsize: 38748
[startup+490.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 48973 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+500.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 49973 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+510.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 50973 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+520.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 51973 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+530.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 52973 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+540.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 53973 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+550.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 54973 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+560.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 8993 0 0 0 55974 32 0 0 25 0 1 0 548334884 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9687 8964 603 41 0 9646 0
vsize: 38748
[startup+570.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9193 0 0 0 56973 32 0 0 25 0 1 0 548334884 40480768 9164 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9883 9164 603 41 0 9842 0
vsize: 39532
[startup+580.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9535 0 0 0 57973 33 0 0 25 0 1 0 548334884 41947136 9506 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10241 9506 603 41 0 10200 0
vsize: 40964
[startup+590.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 58973 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+600.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 59973 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+610.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 60973 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+620.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 61973 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+630.152 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 62985 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+640.152 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 63985 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+650.161 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 64986 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+660.16 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 65986 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+670.16 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 66986 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+680.16 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 67987 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+690.168 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9745 0 0 0 68988 34 0 0 25 0 1 0 548334884 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+700.168 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9746 0 0 0 69988 34 0 0 25 0 1 0 548334884 42754048 9717 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9717 603 41 0 10397 0
vsize: 41752
[startup+710.168 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9747 0 0 0 70988 34 0 0 25 0 1 0 548334884 42754048 9718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10438 9718 603 41 0 10397 0
vsize: 41752
[startup+720.169 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9772 0 0 0 71988 34 0 0 25 0 1 0 548334884 42946560 9743 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10485 9743 603 41 0 10444 0
vsize: 41940
[startup+730.168 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9773 0 0 0 72988 34 0 0 25 0 1 0 548334884 42946560 9744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10485 9744 603 41 0 10444 0
vsize: 41940
[startup+740.169 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9778 0 0 0 73988 34 0 0 25 0 1 0 548334884 42946560 9749 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10485 9749 603 41 0 10444 0
vsize: 41940
[startup+750.17 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9811 0 0 0 74988 34 0 0 25 0 1 0 548334884 43110400 9782 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10525 9782 603 41 0 10484 0
vsize: 42100
[startup+760.169 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 9870 0 0 0 75988 34 0 0 25 0 1 0 548334884 43241472 9841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10557 9841 603 41 0 10516 0
vsize: 42228
[startup+770.169 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 10125 0 0 0 76987 36 0 0 25 0 1 0 548334884 44314624 10096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10819 10096 603 41 0 10778 0
vsize: 43276
[startup+780.169 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 10393 0 0 0 77986 36 0 0 25 0 1 0 548334884 45477888 10364 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11103 10364 603 41 0 11062 0
vsize: 44412
[startup+790.169 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 10669 0 0 0 78986 37 0 0 25 0 1 0 548334884 46690304 10640 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11399 10640 603 41 0 11358 0
vsize: 45596
[startup+800.169 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 10935 0 0 0 79985 38 0 0 25 0 1 0 548334884 47669248 10906 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11638 10906 603 41 0 11597 0
vsize: 46552
[startup+810.169 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11133 0 0 0 80984 39 0 0 25 0 1 0 548334884 48484352 11104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11837 11104 603 41 0 11796 0
vsize: 47348
[startup+820.169 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11438 0 0 0 81983 40 0 0 25 0 1 0 548334884 49745920 11409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12145 11409 603 41 0 12104 0
vsize: 48580
[startup+830.169 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 82983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+840.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 83983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+850.169 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 84983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+860.169 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 85983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+870.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 86983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+880.169 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 87983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+890.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 88983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+900.171 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 89983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+910.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 90983 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+920.171 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11678 0 0 0 91984 41 0 0 25 0 1 0 548334884 50937856 11649 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+930.171 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11680 0 0 0 92984 41 0 0 25 0 1 0 548334884 50937856 11651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11651 603 41 0 12395 0
vsize: 49744
[startup+940.171 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11681 0 0 0 93984 41 0 0 25 0 1 0 548334884 50937856 11652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11652 603 41 0 12395 0
vsize: 49744
[startup+950.171 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11681 0 0 0 94984 41 0 0 25 0 1 0 548334884 50937856 11652 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11652 603 41 0 12395 0
vsize: 49744
[startup+960.171 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11681 0 0 0 95984 41 0 0 25 0 1 0 548334884 50937856 11652 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11652 603 41 0 12395 0
vsize: 49744
[startup+970.172 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11682 0 0 0 96984 41 0 0 25 0 1 0 548334884 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+980.172 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11682 0 0 0 97984 41 0 0 25 0 1 0 548334884 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+990.172 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11682 0 0 0 98984 41 0 0 25 0 1 0 548334884 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1000.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11682 0 0 0 99985 41 0 0 25 0 1 0 548334884 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1010.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11682 0 0 0 100985 41 0 0 25 0 1 0 548334884 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1020.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11682 0 0 0 101985 42 0 0 25 0 1 0 548334884 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1030.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11682 0 0 0 102985 42 0 0 25 0 1 0 548334884 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1040.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11759 0 0 0 103985 42 0 0 25 0 1 0 548334884 51204096 11730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12501 11730 603 41 0 12460 0
vsize: 50004
[startup+1050.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 11995 0 0 0 104984 42 0 0 25 0 1 0 548334884 52142080 11966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12730 11966 603 41 0 12689 0
vsize: 50920
[startup+1060.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12207 0 0 0 105984 43 0 0 25 0 1 0 548334884 53104640 12178 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12965 12178 603 41 0 12924 0
vsize: 51860
[startup+1070.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12388 0 0 0 106983 44 0 0 25 0 1 0 548334884 53772288 12359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13128 12359 603 41 0 13087 0
vsize: 52512
[startup+1080.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12568 0 0 0 107982 45 0 0 25 0 1 0 548334884 54439936 12539 4294967295 134512640 134672761 3221224544 3221223728 134559604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13291 12539 603 41 0 13250 0
vsize: 53164
[startup+1090.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12743 0 0 0 108982 45 0 0 25 0 1 0 548334884 55246848 12714 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13488 12714 603 41 0 13447 0
vsize: 53952
[startup+1100.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 109982 45 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1110.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 110982 45 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1120.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 111982 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1130.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 112983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1140.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 113983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1150.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 114983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1160.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 115983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223648 134560177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1170.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 116983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1180.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 117983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1190.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 118983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10464
Raw data (stat): 10464 (minisat+) R 10463 22612 22611 0 -1 0 12771 0 0 0 119983 46 0 0 25 0 1 0 548334884 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 10464
Raw data (stat): 10464 (minisat+) Z 10463 22612 22611 0 -1 12 12774 0 0 0 119983 49 0 0 25 0 1 0 548334884 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.21
CPU time (s): 1200.33
CPU user time (s): 1199.84
CPU system time (s): 0.492925
CPU usage (%): 100.01
Max. virtual memory (Kb): 54080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####