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/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-9,16-19.opb
MD5SUM	a788dbf2f72289ace41b812e06d88575
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	10
Number of bits of the biggest number in a constraint	4
Biggest sum of numbers in a constraint	101
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	362.64
Number of variables	4626
Total number of constraints	35373
Number of constraints which are clauses	29724
Number of constraints which are cardinality constraints (but not clauses)	5571
Number of constraints which are nor clauses,nor cardinality constraints	78
Minimum length of a constraint	1
Maximum length of a constraint	29
Trace number 5284

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-13 23:16:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3748 boxname=wulflinc4 idbench=364 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a788dbf2f72289ace41b812e06d88575  /oldhome/oroussel/tmp/wulflinc4/normalized-ppp:1-9,16-19.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-ppp:1-9,16-19.opb /oldhome/oroussel/tmp/wulflinc4/normalized-ppp:1-9,16-19.opb
IDLAUNCH: 3748
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        906712 kB
Buffers:         34748 kB
Cached:          73440 kB
SwapCached:          0 kB
Active:          54320 kB
Inactive:        56788 kB
HighTotal:      131008 kB
HighFree:        53760 kB
LowTotal:       903652 kB
LowFree:        852952 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11440 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:36:50 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 3748 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30921 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30920]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30919]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30918]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30917]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30916]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30915]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30914]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30913]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30912]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30911]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30910]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30909]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30908]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30907]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30906]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30905]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30904]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30903]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30902]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30901]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30900]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30899]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30898]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30897]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30896]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30895]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30894]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30893]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30892]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30891]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30890]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[30889]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[30888]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[30887]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[30886]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[30885]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[30884]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30883]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30882]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30881]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30880]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30879]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30878]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30877]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30876]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30875]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30874]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30873]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30872]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30871]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30870]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30869]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30868]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30867]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[30866]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30865]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30864]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30863]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30862]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30861]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30860]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30859]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30858]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30857]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30856]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30855]---> Adder-cost: 64   maxlim: 80   bits: 7/7
c ---[30854]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30853]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30852]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30851]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30850]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30849]---> Adder-cost: 62   maxlim: 77   bits: 7/7
c ---[30848]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30847]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30846]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30845]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30844]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30843]---> Adder-cost: 50   maxlim: 64   bits: 7/7
c ---[30841]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30839]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30837]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30835]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30833]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30831]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30829]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30827]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30825]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30823]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30821]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30819]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30817]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30815]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30813]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30811]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30809]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30807]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30805]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30803]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30801]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30799]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30797]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30795]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30793]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30791]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30789]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30787]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30785]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30783]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30781]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30779]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30777]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30775]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30773]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30771]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30769]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30767]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30765]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30763]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30761]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30759]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30757]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[30755]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[30753]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[30751]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[30749]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[30747]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[30745]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30743]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30741]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30739]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30737]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30735]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30733]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30731]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30729]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30727]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30725]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30723]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30721]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30719]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30717]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30715]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30713]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30711]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30709]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30707]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30705]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30703]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30701]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30699]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[30697]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30695]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30693]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30691]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30689]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30687]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30685]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30683]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30681]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30679]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30677]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30675]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30673]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30671]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30669]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30667]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30665]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30663]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30661]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30659]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30657]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30655]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30653]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30651]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30649]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30647]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30645]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30643]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30641]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30639]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30637]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30635]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30633]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30631]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30629]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30627]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30625]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30623]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30621]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30619]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30617]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30615]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30613]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30611]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30609]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30607]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30605]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30603]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30601]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30599]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30597]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30595]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30593]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30591]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30589]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30587]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30585]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30583]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30581]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30579]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30577]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30575]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30573]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30571]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30569]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30567]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30565]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30563]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30561]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30559]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30557]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30555]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30553]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30551]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30549]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30547]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30545]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30543]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30541]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30539]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30537]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30535]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30533]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30531]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30529]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30527]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30525]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30523]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30521]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30519]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30517]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30515]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30513]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30511]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30509]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30507]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30505]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30503]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30501]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30499]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30497]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30495]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[30494]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30493]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30492]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30491]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30490]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30489]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30488]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30487]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30486]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30485]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30484]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30483]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30482]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30481]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30480]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30479]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30478]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30477]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30476]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30475]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30474]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30473]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30472]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30471]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30470]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30469]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30468]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30467]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30466]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30465]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30464]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30463]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30462]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30461]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30460]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30459]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30458]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30457]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30456]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30455]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30454]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30453]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30452]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30451]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30450]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30449]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30448]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30447]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30446]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30445]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30444]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30443]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30442]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30441]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30440]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30439]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30438]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30437]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30436]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30435]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30434]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30433]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30432]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30431]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30430]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30429]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30428]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30427]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30426]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30425]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30424]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30423]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30422]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30421]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30420]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30419]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30418]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30417]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30416]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30415]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30414]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30413]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30412]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30411]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30410]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30409]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30408]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30407]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30406]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30403]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30402]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30401]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30400]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30399]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30398]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30396]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30395]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30394]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30393]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30392]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30391]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30390]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30389]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30388]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30387]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30386]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30385]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30384]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30383]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30382]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30381]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30380]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30379]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30378]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30377]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30376]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30375]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30374]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30373]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30372]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30371]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30370]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30369]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30368]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30367]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30366]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30365]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30364]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30363]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30362]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30361]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30355]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30354]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30353]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30352]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30351]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30350]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30349]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30348]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30347]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30346]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30345]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30344]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30343]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30342]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30341]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30340]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30339]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30338]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30337]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30336]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30335]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30334]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30333]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30332]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30331]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30330]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30329]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30328]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30327]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30326]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30325]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30324]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30323]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30322]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30321]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30320]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30319]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30318]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30317]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30316]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30315]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30314]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30313]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30312]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30311]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30310]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30309]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30308]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30307]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30306]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30305]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30304]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30303]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30302]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30301]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30300]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30299]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30298]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30297]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30296]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30295]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30294]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30293]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30292]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30291]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30290]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30289]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30288]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30287]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30286]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30285]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30284]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30283]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30282]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30281]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30280]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30279]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30278]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30277]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30276]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30275]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30274]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30273]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30272]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30271]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30270]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30269]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30268]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30267]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30266]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30265]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30264]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30263]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30262]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30261]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30260]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30259]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30258]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30257]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30256]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30255]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30254]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30253]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30252]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30251]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30250]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30249]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30248]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30247]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30246]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30245]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30244]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30243]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30242]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30241]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30240]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30239]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30238]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30237]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30236]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30235]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30234]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30233]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30232]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30231]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30230]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30229]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30228]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30227]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30226]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30225]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30224]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30223]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30222]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30221]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30220]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30219]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30218]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30217]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30216]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30215]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30214]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30213]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30212]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30211]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30210]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30209]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30208]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30207]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30206]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30205]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30204]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30203]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30202]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30201]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30200]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30199]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30198]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30197]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30196]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30195]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30194]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30193]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30192]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30191]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30190]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30189]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30188]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30187]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30186]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30185]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30184]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30183]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30182]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30181]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30180]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30179]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30178]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30177]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30176]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30175]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30174]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30173]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30172]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30171]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30170]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30169]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30168]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30167]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30166]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30165]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30164]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30163]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30162]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30161]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30160]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30159]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30158]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30157]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30156]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30155]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30154]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30153]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30152]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30151]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30150]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30149]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30148]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30147]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30146]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30145]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30144]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30143]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30142]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30141]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30140]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30139]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30138]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30137]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30136]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30135]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30134]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30133]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30132]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30131]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[30130]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 403]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 402]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 401]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 400]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 399]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 398]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 396]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 395]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 394]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 393]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 392]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 391]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 390]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 389]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 388]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 387]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 386]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 385]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 384]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 383]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 382]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 381]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 380]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 379]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 378]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 377]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 376]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 375]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 374]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 373]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 372]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 371]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 370]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 369]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 368]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 367]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 366]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 365]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 364]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 363]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 362]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 361]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 355]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 354]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 353]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 352]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 351]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 350]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 349]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 348]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 347]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 346]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 345]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 344]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 343]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 342]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 341]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 340]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 339]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 338]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 337]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 336]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 335]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 334]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 333]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 332]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 331]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 330]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 329]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 328]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 327]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 326]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 325]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 324]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 323]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 322]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 321]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 320]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 319]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 318]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 317]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 316]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 315]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 314]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 313]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 312]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 311]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 310]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 309]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 308]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 307]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 306]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 305]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 304]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 303]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 302]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 301]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 300]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 299]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 298]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 297]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 296]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 295]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 294]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 293]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 292]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 291]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 290]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 289]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 288]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 287]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 286]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 285]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 284]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 283]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 282]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 281]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 280]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 279]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 278]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 277]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 276]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 275]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 274]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 273]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 272]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 271]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 270]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 269]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 268]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 267]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 266]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 265]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 264]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 263]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 262]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 261]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 260]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 259]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 258]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 257]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 256]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 255]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 254]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 253]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 252]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 251]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 250]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 249]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 248]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 247]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 246]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 245]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 244]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 243]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 242]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 241]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 240]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 239]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 238]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 237]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 236]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 235]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 234]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 233]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 232]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 231]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 230]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 229]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 228]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 227]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 226]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 225]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 224]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 223]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 222]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 221]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 220]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 219]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 218]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 217]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 216]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 215]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 214]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 213]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 212]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 211]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 210]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 209]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 208]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 207]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 206]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 205]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 204]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 203]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 202]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 201]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 200]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 199]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 198]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 197]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 196]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 195]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 194]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 193]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 192]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 191]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 190]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 189]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 188]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 187]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 186]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 185]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 184]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 183]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 182]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 181]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 180]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 179]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 178]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 177]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 176]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 175]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 174]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 173]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 172]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 171]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 170]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 169]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 168]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 167]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 166]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 165]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 164]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 163]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 162]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 161]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 160]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 159]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 158]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 157]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 156]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 155]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 154]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 153]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 152]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 151]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 150]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 149]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 148]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 147]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 146]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 145]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 144]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 143]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 142]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 141]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 140]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 139]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 138]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 137]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 136]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 135]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 134]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 133]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 132]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 131]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 130]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 129]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 128]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 127]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 126]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 125]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 124]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 123]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 122]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 121]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 120]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 119]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 118]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 117]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 116]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 115]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 114]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 113]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 112]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 111]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 110]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 109]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 108]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 107]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 106]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 105]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 104]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 103]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 102]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 101]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 100]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  99]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  98]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  97]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  96]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  95]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  94]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  93]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  92]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  91]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  90]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  89]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  88]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  87]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  86]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  85]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  84]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  83]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  82]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  81]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  80]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  79]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  78]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  77]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  76]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  75]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  74]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  73]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  72]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  71]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  70]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  69]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  68]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  67]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  66]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  65]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  64]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  63]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  62]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  61]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  60]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  59]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  58]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  57]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  56]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  55]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  54]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  53]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  52]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  51]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  50]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  49]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  48]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  47]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  46]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  45]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  44]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  43]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  42]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  41]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  40]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  39]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  38]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  37]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  36]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  35]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  34]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  33]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  32]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  31]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  30]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  29]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  28]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  27]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  26]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  25]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  24]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  23]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  22]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  21]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  20]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  19]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  18]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  17]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  16]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  15]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  14]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  13]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  12]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  11]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  10]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   9]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   8]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   7]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   6]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   5]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   4]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   3]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   2]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   1]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[   0]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  110769   373932 |   36923       0        0     nan |  0.000 % |
c |       100 |  110063   371540 |   40615      22       68     3.1 | 17.386 % |
c |       251 |  109259   368814 |   44676      93      446     4.8 | 18.094 % |
c |       476 |  108711   366954 |   49144     262     1252     4.8 | 18.556 % |
c |       813 |  108163   365096 |   54058     545     2491     4.6 | 19.008 % |
c |      1319 |  107705   363544 |   59464     991     4663     4.7 | 19.371 % |
c |      2080 |  107098   361511 |   65411    1673     8138     4.9 | 19.892 % |
c |      3220 |  106128   358293 |   71952    2677    13965     5.2 | 20.712 % |
c |      4928 |  104534   353002 |   79147    4166    21950     5.3 | 22.054 % |
c |      7490 |  102527   346375 |   87062    6433    35774     5.6 | 23.753 % |
c |     11337 |  102144   345088 |   95768   10180   152566    15.0 | 24.063 % |
c |     17104 |  102108   344971 |  105345   15939   660233    41.4 | 24.097 % |
c |     25754 |  102019   344672 |  115880   24557  1639629    66.8 | 24.176 % |
c |     38729 |  101926   344361 |  127468   37514  3436918    91.6 | 24.259 % |
c |     58190 |  101903   344286 |  140215   56972  6366655   111.8 | 24.279 % |
c |     87384 |  101761   343819 |  154236   86120 10381635   120.5 | 24.407 % |
c |    131174 |  101655   343463 |  169660  129897 16644548   128.1 | 24.500 % |
c |    196858 |  101655   343463 |  186626   38251  4899590   128.1 | 24.500 % |
#### 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.95 0.90 2/54 10069
Raw data (stat): 10069 (runsolver) R 10068 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421617214 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 2728 0 0 0 990 7 0 0 25 0 1 0 421617214 13258752 2701 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3237 2701 603 41 0 3196 0
vsize: 12948
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 2747 0 0 0 1990 7 0 0 25 0 1 0 421617214 13393920 2720 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2720 603 41 0 3229 0
vsize: 13080
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 2758 0 0 0 2989 8 0 0 25 0 1 0 421617214 13393920 2731 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2731 603 41 0 3229 0
vsize: 13080
[startup+40.001 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 2772 0 0 0 3988 8 0 0 25 0 1 0 421617214 13393920 2745 4294967295 134512640 134672761 3221224560 3221223744 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2745 603 41 0 3229 0
vsize: 13080
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 2815 0 0 0 4988 8 0 0 25 0 1 0 421617214 13664256 2788 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3336 2788 603 41 0 3295 0
vsize: 13344
[startup+60.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 4272 0 0 0 5985 12 0 0 25 0 1 0 421617214 19591168 4245 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4783 4245 603 41 0 4742 0
vsize: 19132
[startup+70.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 5374 0 0 0 6981 15 0 0 25 0 1 0 421617214 24154112 5347 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5897 5347 603 41 0 5856 0
vsize: 23588
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 6321 0 0 0 7978 19 0 0 25 0 1 0 421617214 28143616 6294 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6871 6294 603 41 0 6830 0
vsize: 27484
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 7087 0 0 0 8976 21 0 0 25 0 1 0 421617214 31219712 7060 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7622 7060 603 41 0 7581 0
vsize: 30488
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 7870 0 0 0 9974 23 0 0 25 0 1 0 421617214 34402304 7843 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8399 7843 603 41 0 8358 0
vsize: 33596
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 8569 0 0 0 10973 25 0 0 25 0 1 0 421617214 37335040 8542 4294967295 134512640 134672761 3221224560 3221223744 134559509 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9115 8542 603 41 0 9074 0
vsize: 36460
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 9264 0 0 0 11971 27 0 0 25 0 1 0 421617214 40136704 9237 4294967295 134512640 134672761 3221224560 3221223744 134558941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9799 9238 603 41 0 9758 0
vsize: 39196
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 9911 0 0 0 12970 28 0 0 25 0 1 0 421617214 42807296 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10451 9884 603 41 0 10410 0
vsize: 41804
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 10398 0 0 0 13967 30 0 0 25 0 1 0 421617214 44822528 10371 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10943 10371 603 41 0 10902 0
vsize: 43772
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 10904 0 0 0 14965 32 0 0 25 0 1 0 421617214 46817280 10877 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11430 10877 603 41 0 11389 0
vsize: 45720
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 11218 0 0 0 15965 33 0 0 25 0 1 0 421617214 48427008 11191 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11823 11191 603 41 0 11782 0
vsize: 47292
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 11766 0 0 0 16964 34 0 0 25 0 1 0 421617214 50556928 11739 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12343 11739 603 41 0 12302 0
vsize: 49372
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 12384 0 0 0 17962 37 0 0 25 0 1 0 421617214 53116928 12357 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12968 12357 603 41 0 12927 0
vsize: 51872
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 12890 0 0 0 18960 38 0 0 25 0 1 0 421617214 55259136 12863 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13491 12863 603 41 0 13450 0
vsize: 53964
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 13292 0 0 0 19960 39 0 0 25 0 1 0 421617214 56897536 13265 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13891 13265 603 41 0 13850 0
vsize: 55564
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 13720 0 0 0 20959 40 0 0 25 0 1 0 421617214 58654720 13693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14320 13693 603 41 0 14279 0
vsize: 57280
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 14149 0 0 0 21957 42 0 0 25 0 1 0 421617214 60424192 14122 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14752 14122 603 41 0 14711 0
vsize: 59008
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 14528 0 0 0 22956 43 0 0 25 0 1 0 421617214 62038016 14501 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15146 14501 603 41 0 15105 0
vsize: 60584
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 14865 0 0 0 23955 44 0 0 25 0 1 0 421617214 63385600 14838 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15475 14838 603 41 0 15434 0
vsize: 61900
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 15259 0 0 0 24953 46 0 0 25 0 1 0 421617214 64991232 15232 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15867 15232 603 41 0 15826 0
vsize: 63468
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 15570 0 0 0 25953 47 0 0 25 0 1 0 421617214 66191360 15543 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16160 15543 603 41 0 16119 0
vsize: 64640
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 15853 0 0 0 26952 48 0 0 25 0 1 0 421617214 67411968 15826 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16458 15826 603 41 0 16417 0
vsize: 65832
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 16180 0 0 0 27951 48 0 0 25 0 1 0 421617214 68771840 16153 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16790 16153 603 41 0 16749 0
vsize: 67160
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 16515 0 0 0 28951 49 0 0 25 0 1 0 421617214 70107136 16488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17116 16488 603 41 0 17075 0
vsize: 68464
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 16880 0 0 0 29950 50 0 0 25 0 1 0 421617214 71585792 16853 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17477 16853 603 41 0 17436 0
vsize: 69908
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 17221 0 0 0 30949 51 0 0 25 0 1 0 421617214 73056256 17194 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17836 17194 603 41 0 17795 0
vsize: 71344
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 17597 0 0 0 31948 52 0 0 25 0 1 0 421617214 74530816 17570 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18196 17570 603 41 0 18155 0
vsize: 72784
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 17942 0 0 0 32948 53 0 0 25 0 1 0 421617214 76013568 17915 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18558 17915 603 41 0 18517 0
vsize: 74232
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 18278 0 0 0 33947 54 0 0 25 0 1 0 421617214 77361152 18251 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18887 18251 603 41 0 18846 0
vsize: 75548
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 18598 0 0 0 34946 55 0 0 25 0 1 0 421617214 78729216 18571 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19221 18571 603 41 0 19180 0
vsize: 76884
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 18954 0 0 0 35945 56 0 0 25 0 1 0 421617214 80076800 18927 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19550 18927 603 41 0 19509 0
vsize: 78200
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 19255 0 0 0 36945 57 0 0 25 0 1 0 421617214 81408000 19228 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19875 19228 603 41 0 19834 0
vsize: 79500
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 19552 0 0 0 37944 58 0 0 25 0 1 0 421617214 82628608 19525 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20173 19525 603 41 0 20132 0
vsize: 80692
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 19842 0 0 0 38943 59 0 0 25 0 1 0 421617214 83832832 19815 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20467 19815 603 41 0 20426 0
vsize: 81868
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 20135 0 0 0 39943 60 0 0 25 0 1 0 421617214 85053440 20108 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20765 20108 603 41 0 20724 0
vsize: 83060
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 20316 0 0 0 40943 60 0 0 25 0 1 0 421617214 85782528 20289 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20943 20289 603 41 0 20902 0
vsize: 83772
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 20528 0 0 0 41942 61 0 0 25 0 1 0 421617214 86581248 20501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21138 20501 603 41 0 21097 0
vsize: 84552
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 20759 0 0 0 42942 61 0 0 25 0 1 0 421617214 87658496 20732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21401 20732 603 41 0 21360 0
vsize: 85604
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 20989 0 0 0 43942 61 0 0 25 0 1 0 421617214 88616960 20962 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21635 20962 603 41 0 21594 0
vsize: 86540
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 21246 0 0 0 44941 62 0 0 25 0 1 0 421617214 89546752 21219 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21862 21219 603 41 0 21821 0
vsize: 87448
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 21493 0 0 0 45939 63 0 0 25 0 1 0 421617214 91144192 21466 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22252 21466 603 41 0 22211 0
vsize: 89008
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 21780 0 0 0 46938 64 0 0 25 0 1 0 421617214 92364800 21753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22550 21753 603 41 0 22509 0
vsize: 90200
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 22078 0 0 0 47938 65 0 0 25 0 1 0 421617214 93560832 22051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22842 22051 603 41 0 22801 0
vsize: 91368
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 22321 0 0 0 48937 65 0 0 25 0 1 0 421617214 94494720 22294 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23070 22294 603 41 0 23029 0
vsize: 92280
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 22576 0 0 0 49937 66 0 0 25 0 1 0 421617214 95559680 22549 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23330 22549 603 41 0 23289 0
vsize: 93320
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 22819 0 0 0 50936 67 0 0 25 0 1 0 421617214 96497664 22792 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23559 22792 603 41 0 23518 0
vsize: 94236
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 23061 0 0 0 51936 67 0 0 25 0 1 0 421617214 97583104 23034 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23824 23034 603 41 0 23783 0
vsize: 95296
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 23277 0 0 0 52935 68 0 0 25 0 1 0 421617214 98390016 23250 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24021 23250 603 41 0 23980 0
vsize: 96084
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 23505 0 0 0 53935 68 0 0 25 0 1 0 421617214 99364864 23478 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24259 23478 603 41 0 24218 0
vsize: 97036
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 23749 0 0 0 54934 69 0 0 25 0 1 0 421617214 100298752 23722 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24487 23722 603 41 0 24446 0
vsize: 97948
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 23988 0 0 0 55934 70 0 0 25 0 1 0 421617214 101289984 23961 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24729 23961 603 41 0 24688 0
vsize: 98916
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 24235 0 0 0 56934 70 0 0 25 0 1 0 421617214 102379520 24208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24995 24208 603 41 0 24954 0
vsize: 99980
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 24467 0 0 0 57934 71 0 0 25 0 1 0 421617214 103309312 24440 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25222 24440 603 41 0 25181 0
vsize: 100888
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 24671 0 0 0 58933 71 0 0 25 0 1 0 421617214 104235008 24644 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25448 24644 603 41 0 25407 0
vsize: 101792
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 24885 0 0 0 59933 72 0 0 25 0 1 0 421617214 105033728 24858 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25643 24858 603 41 0 25602 0
vsize: 102572
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 25087 0 0 0 60933 72 0 0 25 0 1 0 421617214 105840640 25060 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25840 25060 603 41 0 25799 0
vsize: 103360
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 25279 0 0 0 61932 73 0 0 25 0 1 0 421617214 106639360 25252 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26035 25252 603 41 0 25994 0
vsize: 104140
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 25487 0 0 0 62932 73 0 0 25 0 1 0 421617214 107573248 25460 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26263 25460 603 41 0 26222 0
vsize: 105052
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 25717 0 0 0 63932 74 0 0 25 0 1 0 421617214 108515328 25690 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26493 25690 603 41 0 26452 0
vsize: 105972
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 25922 0 0 0 64931 74 0 0 25 0 1 0 421617214 109318144 25895 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26689 25895 603 41 0 26648 0
vsize: 106756
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 26126 0 0 0 65931 75 0 0 25 0 1 0 421617214 110116864 26099 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26884 26099 603 41 0 26843 0
vsize: 107536
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 26335 0 0 0 66931 75 0 0 25 0 1 0 421617214 110931968 26308 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27083 26308 603 41 0 27042 0
vsize: 108332
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 26522 0 0 0 67930 76 0 0 25 0 1 0 421617214 111804416 26495 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27296 26495 603 41 0 27255 0
vsize: 109184
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 26735 0 0 0 68930 76 0 0 25 0 1 0 421617214 112652288 26708 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27503 26708 603 41 0 27462 0
vsize: 110012
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 26959 0 0 0 69930 77 0 0 25 0 1 0 421617214 113582080 26932 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27730 26932 603 41 0 27689 0
vsize: 110920
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27146 0 0 0 70930 77 0 0 25 0 1 0 421617214 114372608 27119 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27923 27119 603 41 0 27882 0
vsize: 111692
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27341 0 0 0 71929 78 0 0 25 0 1 0 421617214 115150848 27314 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28113 27314 603 41 0 28072 0
vsize: 112452
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27528 0 0 0 72929 78 0 0 25 0 1 0 421617214 115945472 27501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28307 27501 603 41 0 28266 0
vsize: 113228
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27724 0 0 0 73928 79 0 0 25 0 1 0 421617214 116744192 27697 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28502 27697 603 41 0 28461 0
vsize: 114008
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27919 0 0 0 74928 79 0 0 25 0 1 0 421617214 117551104 27892 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27892 603 41 0 28658 0
vsize: 114796
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27919 0 0 0 75928 79 0 0 25 0 1 0 421617214 117551104 27892 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27892 603 41 0 28658 0
vsize: 114796
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27919 0 0 0 76928 79 0 0 25 0 1 0 421617214 117551104 27892 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27892 603 41 0 28658 0
vsize: 114796
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27920 0 0 0 77929 79 0 0 25 0 1 0 421617214 117551104 27893 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27893 603 41 0 28658 0
vsize: 114796
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27921 0 0 0 78929 79 0 0 25 0 1 0 421617214 117551104 27894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27894 603 41 0 28658 0
vsize: 114796
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27921 0 0 0 79929 79 0 0 25 0 1 0 421617214 117551104 27894 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27894 603 41 0 28658 0
vsize: 114796
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27921 0 0 0 80928 80 0 0 25 0 1 0 421617214 117551104 27894 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27894 603 41 0 28658 0
vsize: 114796
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27921 0 0 0 81928 80 0 0 25 0 1 0 421617214 117551104 27894 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27894 603 41 0 28658 0
vsize: 114796
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27921 0 0 0 82928 80 0 0 25 0 1 0 421617214 117551104 27894 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27894 603 41 0 28658 0
vsize: 114796
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27921 0 0 0 83927 80 0 0 25 0 1 0 421617214 117551104 27894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27894 603 41 0 28658 0
vsize: 114796
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27922 0 0 0 84927 80 0 0 25 0 1 0 421617214 117551104 27895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27895 603 41 0 28658 0
vsize: 114796
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27922 0 0 0 85927 80 0 0 25 0 1 0 421617214 117551104 27895 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27895 603 41 0 28658 0
vsize: 114796
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27925 0 0 0 86926 81 0 0 25 0 1 0 421617214 117551104 27898 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27898 603 41 0 28658 0
vsize: 114796
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27925 0 0 0 87926 81 0 0 25 0 1 0 421617214 117551104 27898 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27898 603 41 0 28658 0
vsize: 114796
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27926 0 0 0 88926 81 0 0 25 0 1 0 421617214 117551104 27899 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27899 603 41 0 28658 0
vsize: 114796
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27926 0 0 0 89926 81 0 0 25 0 1 0 421617214 117551104 27899 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27899 603 41 0 28658 0
vsize: 114796
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27926 0 0 0 90925 82 0 0 25 0 1 0 421617214 117551104 27899 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27899 603 41 0 28658 0
vsize: 114796
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27926 0 0 0 91925 82 0 0 25 0 1 0 421617214 117551104 27899 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27899 603 41 0 28658 0
vsize: 114796
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27926 0 0 0 92925 82 0 0 25 0 1 0 421617214 117551104 27899 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27899 603 41 0 28658 0
vsize: 114796
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27926 0 0 0 93924 83 0 0 25 0 1 0 421617214 117551104 27899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27899 603 41 0 28658 0
vsize: 114796
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27927 0 0 0 94924 83 0 0 25 0 1 0 421617214 117551104 27900 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27900 603 41 0 28658 0
vsize: 114796
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27928 0 0 0 95924 83 0 0 25 0 1 0 421617214 117551104 27901 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27901 603 41 0 28658 0
vsize: 114796
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27928 0 0 0 96923 84 0 0 25 0 1 0 421617214 117551104 27901 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27901 603 41 0 28658 0
vsize: 114796
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27928 0 0 0 97923 84 0 0 25 0 1 0 421617214 117551104 27901 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27901 603 41 0 28658 0
vsize: 114796
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27928 0 0 0 98923 84 0 0 25 0 1 0 421617214 117551104 27901 4294967295 134512640 134672761 3221224560 3221223516 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27901 603 41 0 28658 0
vsize: 114796
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27929 0 0 0 99922 84 0 0 25 0 1 0 421617214 117551104 27902 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27902 603 41 0 28658 0
vsize: 114796
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27929 0 0 0 100922 85 0 0 25 0 1 0 421617214 117551104 27902 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28699 27902 603 41 0 28658 0
vsize: 114796
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27929 0 0 0 101922 85 0 0 25 0 1 0 421617214 117551104 27902 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27902 603 41 0 28658 0
vsize: 114796
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27931 0 0 0 102922 85 0 0 25 0 1 0 421617214 117551104 27904 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27904 603 41 0 28658 0
vsize: 114796
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27933 0 0 0 103922 85 0 0 25 0 1 0 421617214 117551104 27906 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27906 603 41 0 28658 0
vsize: 114796
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27934 0 0 0 104922 85 0 0 25 0 1 0 421617214 117551104 27907 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27907 603 41 0 28658 0
vsize: 114796
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27934 0 0 0 105923 85 0 0 25 0 1 0 421617214 117551104 27907 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27907 603 41 0 28658 0
vsize: 114796
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27934 0 0 0 106923 85 0 0 25 0 1 0 421617214 117551104 27907 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27907 603 41 0 28658 0
vsize: 114796
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27934 0 0 0 107923 85 0 0 25 0 1 0 421617214 117551104 27907 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27907 603 41 0 28658 0
vsize: 114796
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27934 0 0 0 108923 85 0 0 25 0 1 0 421617214 117551104 27907 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27907 603 41 0 28658 0
vsize: 114796
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27934 0 0 0 109923 85 0 0 25 0 1 0 421617214 117551104 27907 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27907 603 41 0 28658 0
vsize: 114796
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27935 0 0 0 110923 85 0 0 25 0 1 0 421617214 117551104 27908 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27908 603 41 0 28658 0
vsize: 114796
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27935 0 0 0 111924 85 0 0 25 0 1 0 421617214 117551104 27908 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27908 603 41 0 28658 0
vsize: 114796
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27935 0 0 0 112924 85 0 0 25 0 1 0 421617214 117551104 27908 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27908 603 41 0 28658 0
vsize: 114796
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27941 0 0 0 113924 85 0 0 25 0 1 0 421617214 117551104 27914 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27914 603 41 0 28658 0
vsize: 114796
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27941 0 0 0 114924 85 0 0 25 0 1 0 421617214 117551104 27914 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27914 603 41 0 28658 0
vsize: 114796
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27942 0 0 0 115924 85 0 0 25 0 1 0 421617214 117551104 27915 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27915 603 41 0 28658 0
vsize: 114796
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27942 0 0 0 116925 85 0 0 25 0 1 0 421617214 117551104 27915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27915 603 41 0 28658 0
vsize: 114796
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27942 0 0 0 117925 85 0 0 25 0 1 0 421617214 117551104 27915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27915 603 41 0 28658 0
vsize: 114796
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27942 0 0 0 118925 85 0 0 25 0 1 0 421617214 117551104 27915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27915 603 41 0 28658 0
vsize: 114796
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10069
Raw data (stat): 10069 (minisat+) R 10068 5897 5896 0 -1 0 27942 0 0 0 119925 85 0 0 25 0 1 0 421617214 117551104 27915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28699 27915 603 41 0 28658 0
vsize: 114796
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 10069
Raw data (stat): 10069 (minisat+) Z 10068 5897 5896 0 -1 12 27944 0 0 0 119925 90 0 0 25 0 1 0 421617214 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.09
CPU time (s): 1200.16
CPU user time (s): 1199.26
CPU system time (s): 0.902862
CPU usage (%): 100.006
Max. virtual memory (Kb): 114796
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####