PB'05 competition: run trace

Some explanations

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        432232 kB
Buffers:         33960 kB
Cached:         534900 kB
SwapCached:        164 kB
Active:         276820 kB
Inactive:       294492 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        431980 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6088 kB
Slab:            25512 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:51:57 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 19653 7 1200.23 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.85 0.99 0.94 2/54 12958
Raw data (stat): 12958 (runsolver) R 12957 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540786126 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+10.0001 s]
Raw data (loadavg): 0.87 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 2237 0 0 0 993 6 0 0 25 0 1 0 540786126 11800576 2208 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.0063 s]
Raw data (loadavg): 0.89 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 2625 0 0 0 1993 6 0 0 25 0 1 0 540786126 13393920 2596 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2596 603 41 0 3229 0
vsize: 13080
[startup+30.0065 s]
Raw data (loadavg): 0.91 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 2753 0 0 0 2992 7 0 0 25 0 1 0 540786126 13799424 2724 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3369 2724 603 41 0 3328 0
vsize: 13476
[startup+40.0072 s]
Raw data (loadavg): 0.92 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 3016 0 0 0 3991 8 0 0 25 0 1 0 540786126 14995456 2987 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3661 2987 603 41 0 3620 0
vsize: 14644
[startup+50.0082 s]
Raw data (loadavg): 0.93 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 3227 0 0 0 4991 9 0 0 25 0 1 0 540786126 15798272 3198 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3857 3198 603 41 0 3816 0
vsize: 15428
[startup+60.0076 s]
Raw data (loadavg): 0.94 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 3370 0 0 0 5990 10 0 0 25 0 1 0 540786126 16470016 3341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4021 3341 603 41 0 3980 0
vsize: 16084
[startup+70.0081 s]
Raw data (loadavg): 0.95 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 3557 0 0 0 6989 11 0 0 25 0 1 0 540786126 17137664 3528 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4184 3528 603 41 0 4143 0
vsize: 16736
[startup+80.0094 s]
Raw data (loadavg): 0.96 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 3748 0 0 0 7989 11 0 0 25 0 1 0 540786126 18198528 3719 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4443 3719 603 41 0 4402 0
vsize: 17772
[startup+90.0095 s]
Raw data (loadavg): 0.96 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 3862 0 0 0 8989 12 0 0 25 0 1 0 540786126 18595840 3833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4540 3833 603 41 0 4499 0
vsize: 18160
[startup+100.009 s]
Raw data (loadavg): 0.97 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 3998 0 0 0 9988 12 0 0 25 0 1 0 540786126 19132416 3969 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4671 3969 603 41 0 4630 0
vsize: 18684
[startup+110.009 s]
Raw data (loadavg): 0.97 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4112 0 0 0 10987 13 0 0 25 0 1 0 540786126 19673088 4083 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4803 4083 603 41 0 4762 0
vsize: 19212
[startup+120.01 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4260 0 0 0 11987 13 0 0 25 0 1 0 540786126 20209664 4231 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4231 603 41 0 4893 0
vsize: 19736
[startup+130.009 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4425 0 0 0 12986 14 0 0 25 0 1 0 540786126 20881408 4396 4294967295 134512640 134672761 3221224544 3221223680 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5098 4396 603 41 0 5057 0
vsize: 20392
[startup+140.01 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4569 0 0 0 13986 14 0 0 25 0 1 0 540786126 21417984 4540 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5229 4540 603 41 0 5188 0
vsize: 20916
[startup+150.01 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4669 0 0 0 14986 15 0 0 25 0 1 0 540786126 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+160.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4669 0 0 0 15986 15 0 0 25 0 1 0 540786126 21815296 4640 4294967295 134512640 134672761 3221224544 3221223680 134565096 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): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4669 0 0 0 16988 15 0 0 25 0 1 0 540786126 21815296 4640 4294967295 134512640 134672761 3221224544 3221223712 134560864 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): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 17988 15 0 0 25 0 1 0 540786126 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560920 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): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 18988 15 0 0 25 0 1 0 540786126 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+200.026 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 19988 15 0 0 25 0 1 0 540786126 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): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 20988 15 0 0 25 0 1 0 540786126 21958656 4658 4294967295 134512640 134672761 3221224544 3221223680 134560697 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): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 21988 15 0 0 25 0 1 0 540786126 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+230.025 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 22989 15 0 0 25 0 1 0 540786126 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+240.026 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 23989 15 0 0 25 0 1 0 540786126 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.028 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 24989 15 0 0 25 0 1 0 540786126 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+260.031 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 25990 15 0 0 25 0 1 0 540786126 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.032 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4687 0 0 0 26990 15 0 0 25 0 1 0 540786126 21958656 4658 4294967295 134512640 134672761 3221224544 3221223712 134561215 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.032 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 4912 0 0 0 27989 16 0 0 25 0 1 0 540786126 22892544 4883 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5589 4883 603 41 0 5548 0
vsize: 22356
[startup+290.032 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 5369 0 0 0 28988 17 0 0 25 0 1 0 540786126 24772608 5340 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6048 5340 603 41 0 6007 0
vsize: 24192
[startup+300.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 5773 0 0 0 29987 19 0 0 25 0 1 0 540786126 26378240 5744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6440 5744 603 41 0 6399 0
vsize: 25760
[startup+310.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6316 0 0 0 30985 21 0 0 25 0 1 0 540786126 28659712 6287 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6997 6287 603 41 0 6956 0
vsize: 27988
[startup+320.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6656 0 0 0 31983 22 0 0 25 0 1 0 540786126 29995008 6627 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7323 6627 603 41 0 7282 0
vsize: 29292
[startup+330.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6810 0 0 0 32983 23 0 0 25 0 1 0 540786126 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+340.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6810 0 0 0 33983 23 0 0 25 0 1 0 540786126 30666752 6781 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6810 0 0 0 34983 23 0 0 25 0 1 0 540786126 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+360.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6810 0 0 0 35984 23 0 0 25 0 1 0 540786126 30666752 6781 4294967295 134512640 134672761 3221224544 3221223648 134560293 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6810 0 0 0 36984 23 0 0 25 0 1 0 540786126 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.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 6987 0 0 0 37983 24 0 0 25 0 1 0 540786126 31334400 6958 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7650 6958 603 41 0 7609 0
vsize: 30600
[startup+390.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 7463 0 0 0 38982 25 0 0 25 0 1 0 540786126 33345536 7434 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8141 7434 603 41 0 8100 0
vsize: 32564
[startup+400.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 7883 0 0 0 39981 26 0 0 25 0 1 0 540786126 35090432 7854 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8567 7854 603 41 0 8526 0
vsize: 34268
[startup+410.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8267 0 0 0 40980 27 0 0 25 0 1 0 540786126 36597760 8238 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8935 8238 603 41 0 8894 0
vsize: 35740
[startup+420.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8654 0 0 0 41980 28 0 0 25 0 1 0 540786126 38199296 8625 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9326 8625 603 41 0 9285 0
vsize: 37304
[startup+430.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8978 0 0 0 42979 29 0 0 25 0 1 0 540786126 39546880 8949 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9655 8949 603 41 0 9614 0
vsize: 38620
[startup+440.035 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8992 0 0 0 43979 29 0 0 25 0 1 0 540786126 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8992 0 0 0 44979 29 0 0 25 0 1 0 540786126 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8992 0 0 0 45979 29 0 0 25 0 1 0 540786126 39677952 8963 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.035 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8992 0 0 0 46980 29 0 0 25 0 1 0 540786126 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8992 0 0 0 47980 29 0 0 25 0 1 0 540786126 39677952 8963 4294967295 134512640 134672761 3221224544 3221223712 134560920 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.035 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 48980 29 0 0 25 0 1 0 540786126 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.035 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 49980 29 0 0 25 0 1 0 540786126 39677952 8964 4294967295 134512640 134672761 3221224544 3221223728 134559405 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 50980 29 0 0 25 0 1 0 540786126 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 51980 29 0 0 25 0 1 0 540786126 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+530.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 52981 29 0 0 25 0 1 0 540786126 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 53981 29 0 0 25 0 1 0 540786126 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 54981 29 0 0 25 0 1 0 540786126 39677952 8964 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 8993 0 0 0 55981 29 0 0 25 0 1 0 540786126 39677952 8964 4294967295 134512640 134672761 3221224544 3221223728 134558662 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9210 0 0 0 56980 30 0 0 25 0 1 0 540786126 40480768 9181 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9883 9181 603 41 0 9842 0
vsize: 39532
[startup+580.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9556 0 0 0 57980 31 0 0 25 0 1 0 540786126 41947136 9527 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10241 9527 603 41 0 10200 0
vsize: 40964
[startup+590.035 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 58979 32 0 0 25 0 1 0 540786126 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.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 59979 32 0 0 25 0 1 0 540786126 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+610.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 60979 32 0 0 25 0 1 0 540786126 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+620.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 61980 32 0 0 25 0 1 0 540786126 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+630.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 62979 32 0 0 25 0 1 0 540786126 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+640.038 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 63979 32 0 0 25 0 1 0 540786126 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+650.046 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 64980 32 0 0 25 0 1 0 540786126 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+660.049 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 65980 32 0 0 25 0 1 0 540786126 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+670.049 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 66980 33 0 0 25 0 1 0 540786126 42754048 9716 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+680.05 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 67980 33 0 0 25 0 1 0 540786126 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+690.05 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9745 0 0 0 68980 33 0 0 25 0 1 0 540786126 42754048 9716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9716 603 41 0 10397 0
vsize: 41752
[startup+700.051 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9746 0 0 0 69979 34 0 0 25 0 1 0 540786126 42754048 9717 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9717 603 41 0 10397 0
vsize: 41752
[startup+710.051 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9748 0 0 0 70979 34 0 0 25 0 1 0 540786126 42754048 9719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10438 9719 603 41 0 10397 0
vsize: 41752
[startup+720.052 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9772 0 0 0 71979 35 0 0 25 0 1 0 540786126 42946560 9743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10485 9743 603 41 0 10444 0
vsize: 41940
[startup+730.053 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9773 0 0 0 72979 35 0 0 25 0 1 0 540786126 42946560 9744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10485 9744 603 41 0 10444 0
vsize: 41940
[startup+740.053 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9778 0 0 0 73978 35 0 0 25 0 1 0 540786126 42946560 9749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10485 9749 603 41 0 10444 0
vsize: 41940
[startup+750.054 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9816 0 0 0 74978 36 0 0 25 0 1 0 540786126 43110400 9787 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10525 9787 603 41 0 10484 0
vsize: 42100
[startup+760.054 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 9926 0 0 0 75978 36 0 0 25 0 1 0 540786126 43511808 9897 4294967295 134512640 134672761 3221224544 3221223724 1075351041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10623 9897 603 41 0 10582 0
vsize: 42492
[startup+770.054 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 10187 0 0 0 76977 36 0 0 25 0 1 0 540786126 44584960 10158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10885 10158 603 41 0 10844 0
vsize: 43540
[startup+780.055 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 10465 0 0 0 77976 38 0 0 25 0 1 0 540786126 45883392 10436 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11202 10436 603 41 0 11161 0
vsize: 44808
[startup+790.056 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 10757 0 0 0 78976 38 0 0 25 0 1 0 540786126 46956544 10728 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11464 10728 603 41 0 11423 0
vsize: 45856
[startup+800.056 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 10990 0 0 0 79975 40 0 0 25 0 1 0 540786126 47939584 10961 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 10961 603 41 0 11663 0
vsize: 46816
[startup+810.056 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11198 0 0 0 80974 41 0 0 25 0 1 0 540786126 48812032 11169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11917 11169 603 41 0 11876 0
vsize: 47668
[startup+820.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11525 0 0 0 81973 42 0 0 25 0 1 0 540786126 50274304 11496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12274 11496 603 41 0 12233 0
vsize: 49096
[startup+830.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 82972 42 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+840.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 83972 43 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+850.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 84972 43 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+860.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 85971 43 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+870.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 86971 43 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+880.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 87971 44 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+890.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 88971 44 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.059 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 89971 44 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+910.059 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11678 0 0 0 90970 44 0 0 25 0 1 0 540786126 50937856 11649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+920.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11679 0 0 0 91970 45 0 0 25 0 1 0 540786126 50937856 11650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11650 603 41 0 12395 0
vsize: 49744
[startup+930.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11681 0 0 0 92970 45 0 0 25 0 1 0 540786126 50937856 11652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11652 603 41 0 12395 0
vsize: 49744
[startup+940.063 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11681 0 0 0 93970 45 0 0 25 0 1 0 540786126 50937856 11652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11652 603 41 0 12395 0
vsize: 49744
[startup+950.064 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11681 0 0 0 94970 46 0 0 25 0 1 0 540786126 50937856 11652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11652 603 41 0 12395 0
vsize: 49744
[startup+960.064 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 95970 46 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+970.065 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 96969 46 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+980.066 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 97969 47 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+990.066 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 98969 47 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 99969 47 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 100969 47 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 101969 48 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11682 0 0 0 102969 48 0 0 25 0 1 0 540786126 50937856 11653 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12436 11653 603 41 0 12395 0
vsize: 49744
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 11871 0 0 0 103968 49 0 0 25 0 1 0 540786126 51740672 11842 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12632 11842 603 41 0 12591 0
vsize: 50528
[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12104 0 0 0 104967 49 0 0 25 0 1 0 540786126 52699136 12075 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12866 12075 603 41 0 12825 0
vsize: 51464
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12303 0 0 0 105967 50 0 0 25 0 1 0 540786126 53374976 12274 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13031 12274 603 41 0 12990 0
vsize: 52124
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12474 0 0 0 106966 51 0 0 25 0 1 0 540786126 54169600 12445 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13225 12445 603 41 0 13184 0
vsize: 52900
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12664 0 0 0 107966 52 0 0 25 0 1 0 540786126 54841344 12635 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13389 12635 603 41 0 13348 0
vsize: 53556
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 108965 53 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 109964 53 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 110964 53 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 111964 53 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 112965 53 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 113965 54 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 114965 54 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 115964 54 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 116964 54 0 0 25 0 1 0 540786126 55377920 12742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13520 12742 603 41 0 13479 0
vsize: 54080
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 117964 55 0 0 25 0 1 0 540786126 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.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 118964 55 0 0 25 0 1 0 540786126 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.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 12958
Raw data (stat): 12958 (minisat+) R 12957 10614 10613 0 -1 0 12771 0 0 0 119965 55 0 0 25 0 1 0 540786126 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 12958
Raw data (stat): 12958 (minisat+) Z 12957 10614 10613 0 -1 12 12774 0 0 0 119965 57 0 0 25 0 1 0 540786126 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.11
CPU time (s): 1200.23
CPU user time (s): 1199.65
CPU system time (s): 0.578911
CPU usage (%): 100.01
Max. virtual memory (Kb): 54080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####