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-12,16.opb
MD5SUM	41edd2db35f2c8eb6d4b1f0a68a60338
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	102
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	6.63699
Number of variables	4662
Total number of constraints	36387
Number of constraints which are clauses	30696
Number of constraints which are cardinality constraints (but not clauses)	5613
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 5282

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-13 23:15:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3746 boxname=wulflinc25 idbench=362 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  41edd2db35f2c8eb6d4b1f0a68a60338  /oldhome/oroussel/tmp/wulflinc25/normalized-ppp:1-12,16.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc25/normalized-ppp:1-12,16.opb /oldhome/oroussel/tmp/wulflinc25/normalized-ppp:1-12,16.opb
IDLAUNCH: 3746
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        897644 kB
Buffers:         33540 kB
Cached:          68764 kB
SwapCached:         36 kB
Active:          47372 kB
Inactive:        57796 kB
HighTotal:      131008 kB
HighFree:        58576 kB
LowTotal:       903652 kB
LowFree:        839068 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26424 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:35:39 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 3746 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 31899 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[31898]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31897]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31896]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31895]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31894]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31893]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31892]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31891]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31890]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31889]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31888]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31887]---> Adder-cost: 64   maxlim: 84   bits: 7/7
c ---[31886]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31885]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31884]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31883]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31882]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31881]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31880]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31879]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31878]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31877]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31876]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31875]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31874]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31873]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31872]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31871]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31870]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31869]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31868]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[31867]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[31866]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[31865]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[31864]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[31863]---> Adder-cost: 64   maxlim: 82   bits: 7/7
c ---[31862]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31861]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31860]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31859]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31858]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31857]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31856]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31855]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31854]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31853]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31852]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31851]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31850]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31849]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31848]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31847]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31846]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31845]---> Adder-cost: 64   maxlim: 83   bits: 7/7
c ---[31844]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31843]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31842]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31841]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31840]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31839]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31838]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31837]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31836]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31835]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31834]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31833]---> Adder-cost: 64   maxlim: 81   bits: 7/7
c ---[31832]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31831]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31830]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31829]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31828]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31827]---> Adder-cost: 58   maxlim: 78   bits: 7/7
c ---[31826]---> Adder-cost: 48   maxlim: 65   bits: 7/7
c ---[31825]---> Adder-cost: 48   maxlim: 65   bits: 7/7
c ---[31824]---> Adder-cost: 48   maxlim: 65   bits: 7/7
c ---[31823]---> Adder-cost: 48   maxlim: 65   bits: 7/7
c ---[31822]---> Adder-cost: 48   maxlim: 65   bits: 7/7
c ---[31821]---> Adder-cost: 48   maxlim: 65   bits: 7/7
c ---[31819]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31817]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31815]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31813]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31811]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31809]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31807]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31805]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31803]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31801]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31799]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31797]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31795]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31793]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31791]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31789]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31787]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31785]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31783]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31781]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31779]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31777]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31775]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31773]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31771]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31769]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31767]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31765]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31763]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31761]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31759]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31757]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31755]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31753]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31751]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31749]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31747]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31745]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31743]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31741]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31739]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31737]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31735]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31733]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31731]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31729]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31727]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31725]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[31723]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31721]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31719]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31717]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31715]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31713]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31711]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31709]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31707]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31705]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31703]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31701]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31699]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31697]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31695]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31693]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31691]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31689]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31687]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31685]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31683]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31681]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31679]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31677]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[31675]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31673]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31671]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31669]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31667]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31665]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31663]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31661]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31659]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31657]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31655]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31653]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31651]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31649]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31647]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31645]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31643]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31641]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31639]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31637]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31635]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31633]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31631]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31629]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31627]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31625]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31623]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31621]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31619]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31617]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31615]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31613]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31611]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31609]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31607]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31605]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31603]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31601]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31599]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31597]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31595]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31593]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31591]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31589]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31587]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31585]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31583]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31581]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31579]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31577]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31575]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31573]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31571]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31569]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31567]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31565]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31563]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31561]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31559]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31557]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31555]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31553]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31551]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31549]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31547]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31545]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31543]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31541]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31539]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31537]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31535]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31533]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31531]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31529]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31527]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31525]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31523]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31521]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31519]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31517]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31515]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31513]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31511]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31509]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31507]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31505]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31503]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31501]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31499]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31497]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31495]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31493]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31491]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31489]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31487]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31485]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31483]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31481]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31479]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31477]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31475]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31473]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[31472]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31471]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31470]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31469]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31468]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31467]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31466]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31465]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31464]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31463]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31462]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31461]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31460]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31459]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31458]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31457]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31456]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31455]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31454]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31453]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31452]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31451]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31450]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31449]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31448]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31447]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31446]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31445]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31444]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31443]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31442]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31441]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31440]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31439]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31438]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31437]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31436]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31435]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31434]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31433]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31432]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31431]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31430]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31429]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31428]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31427]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31426]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31425]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31424]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31423]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31422]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31421]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31420]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31419]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31418]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31417]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31416]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31415]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31414]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31413]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31412]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31411]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31410]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31409]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31408]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31407]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31406]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31403]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31402]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31401]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31400]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31399]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31398]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31396]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31395]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31394]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31393]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31392]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31391]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31390]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31389]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31388]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31387]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31386]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31385]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31384]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31383]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31382]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31381]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31380]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31379]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31378]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31377]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31376]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31375]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31374]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31373]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31372]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31371]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31370]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31369]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31368]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31367]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31366]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31365]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31364]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31363]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31362]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31361]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31355]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31354]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31353]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31352]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31351]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31350]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31349]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31348]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31347]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31346]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31345]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31344]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31343]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31342]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31341]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31340]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31339]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31338]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31337]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31336]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31335]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31334]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31333]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31332]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31331]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31330]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31329]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31328]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31327]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31326]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31325]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31324]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31323]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31322]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31321]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31320]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31319]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31318]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31317]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31316]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31315]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31314]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31313]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31312]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31311]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31310]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31309]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31308]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31307]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31306]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31305]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31304]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31303]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31302]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31301]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31300]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31299]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31298]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31297]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31296]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31295]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31294]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31293]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31292]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31291]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31290]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31289]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31288]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31287]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31286]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31285]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31284]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31283]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31282]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31281]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31280]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31279]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31278]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31277]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31276]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31275]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31274]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31273]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31272]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31271]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31270]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31269]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31268]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31267]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31266]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31265]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31264]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31263]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31262]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31261]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31260]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31259]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31258]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31257]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31256]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31255]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31254]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31253]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31252]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31251]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31250]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31249]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31248]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31247]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31246]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31245]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31244]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31243]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31242]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31241]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31240]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31239]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31238]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31237]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31236]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31235]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31234]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31233]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31232]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31231]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31230]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31229]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31228]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31227]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31226]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31225]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31224]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31223]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31222]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31221]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31220]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31219]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31218]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31217]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31216]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31215]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31214]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31213]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31212]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31211]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31210]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31209]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31208]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31207]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31206]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31205]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31204]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31203]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31202]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31201]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31200]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31199]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31198]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31197]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31196]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31195]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31194]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31193]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31192]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31191]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31190]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31189]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31188]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31187]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31186]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31185]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31184]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31183]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31182]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31181]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31180]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31179]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31178]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31177]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31176]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31175]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31174]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31173]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31172]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31171]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31170]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31169]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31168]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31167]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31166]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31165]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31164]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31163]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31162]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31161]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31160]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31159]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31158]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31157]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31156]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31155]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31154]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31153]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31152]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31151]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31150]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31149]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31148]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31147]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31146]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31145]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31144]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31143]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31142]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31141]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31140]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31139]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31138]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31137]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31136]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31135]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31134]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31133]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31132]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31131]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31130]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31129]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31128]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31127]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31126]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31125]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31124]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31123]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31122]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31121]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31120]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31119]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31118]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31117]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31116]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31115]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31114]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31113]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31112]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31111]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31110]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31109]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31108]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31107]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31106]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31105]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31104]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31103]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[31102]---> 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 |  112899   380634 |   37633       0        0     nan |  0.000 % |
c |       100 |  112254   378453 |   41396      29      123     4.2 | 17.024 % |
c |       250 |  111670   376471 |   45535     118      472     4.0 | 17.550 % |
c |       475 |  110969   374090 |   50089     276     1182     4.3 | 18.163 % |
c |       813 |  110581   372784 |   55098     583     2492     4.3 | 18.484 % |
c |      1319 |  109985   370786 |   60608    1017     4628     4.6 | 18.975 % |
c |      2079 |  108917   367222 |   66669    1648     7768     4.7 | 19.900 % |
c |      3218 |  107524   362602 |   73336    2589    12312     4.8 | 21.082 % |
c |      4926 |  106371   358818 |   80669    4129    20765     5.0 | 22.011 % |
c |      7488 |  104760   353505 |   88736    6455    32880     5.1 | 23.383 % |
c |     11333 |  103376   348946 |   97610   10087    61565     6.1 | 24.571 % |
c |     17099 |  101578   343027 |  107371   15563   144652     9.3 | 26.094 % |
c |     25749 |   99801   337184 |  118108   23892   275740    11.5 | 27.665 % |
c |     38723 |   97923   330953 |  129919   36525   493489    13.5 | 29.319 % |
c |     58184 |   97159   328403 |  142911   55783  1257886    22.5 | 29.971 % |
c |     87376 |   96933   327650 |  157202   84899  4625424    54.5 | 30.146 % |
c |    131165 |   96396   325881 |  172922  128586  9432369    73.4 | 30.555 % |
c |    196851 |   95562   323149 |  190214   39026  2476697    63.5 | 31.193 % |
c |    295377 |   95469   322845 |  209236  137537 15790105   114.8 | 31.266 % |
c |    443166 |   95140   321761 |  230160   96138  7404019    77.0 | 31.519 % |
#### 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.97 0.91 2/54 31066
Raw data (stat): 31066 (runsolver) R 31065 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479844863 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.0001 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 2754 0 0 0 989 9 0 0 25 0 1 0 479844863 13320192 2728 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2728 603 41 0 3211 0
vsize: 13008
[startup+20.001 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 2768 0 0 0 1989 10 0 0 25 0 1 0 479844863 13455360 2742 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3285 2742 603 41 0 3244 0
vsize: 13140
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 2780 0 0 0 2988 10 0 0 25 0 1 0 479844863 13455360 2754 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3285 2754 603 41 0 3244 0
vsize: 13140
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 2803 0 0 0 3988 11 0 0 25 0 1 0 479844863 13602816 2777 4294967295 134512640 134672761 3221224560 3221223604 1075351070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3321 2777 603 41 0 3280 0
vsize: 13284
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 2820 0 0 0 4988 11 0 0 25 0 1 0 479844863 13602816 2794 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2794 603 41 0 3280 0
vsize: 13284
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 2851 0 0 0 5988 11 0 0 25 0 1 0 479844863 13737984 2825 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3354 2825 603 41 0 3313 0
vsize: 13416
[startup+70.0028 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 2940 0 0 0 6988 11 0 0 25 0 1 0 479844863 14143488 2914 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3453 2914 603 41 0 3412 0
vsize: 13812
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3032 0 0 0 7987 12 0 0 25 0 1 0 479844863 14618624 3006 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 3006 603 41 0 3528 0
vsize: 14276
[startup+90.003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3111 0 0 0 8987 12 0 0 25 0 1 0 479844863 14888960 3085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3635 3085 603 41 0 3594 0
vsize: 14540
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3174 0 0 0 9987 12 0 0 25 0 1 0 479844863 15155200 3148 4294967295 134512640 134672761 3221224560 3221223728 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3700 3148 603 41 0 3659 0
vsize: 14800
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3271 0 0 0 10987 13 0 0 25 0 1 0 479844863 15560704 3245 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3799 3245 603 41 0 3758 0
vsize: 15196
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3409 0 0 0 11987 13 0 0 25 0 1 0 479844863 16101376 3383 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3931 3383 603 41 0 3890 0
vsize: 15724
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3505 0 0 0 12987 14 0 0 25 0 1 0 479844863 16498688 3479 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3479 603 41 0 3987 0
vsize: 16112
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3641 0 0 0 13986 14 0 0 25 0 1 0 479844863 17039360 3615 4294967295 134512640 134672761 3221224560 3221223684 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4160 3615 603 41 0 4119 0
vsize: 16640
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 3837 0 0 0 14985 15 0 0 25 0 1 0 479844863 17850368 3811 4294967295 134512640 134672761 3221224560 3221223744 134558324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4358 3812 603 41 0 4317 0
vsize: 17432
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 4586 0 0 0 15983 17 0 0 25 0 1 0 479844863 20938752 4560 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5112 4560 603 41 0 5071 0
vsize: 20448
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 5267 0 0 0 16982 19 0 0 25 0 1 0 479844863 23609344 5241 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5764 5241 603 41 0 5723 0
vsize: 23056
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 6305 0 0 0 17979 22 0 0 25 0 1 0 479844863 28139520 6279 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6279 603 41 0 6829 0
vsize: 27480
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 7088 0 0 0 18977 24 0 0 25 0 1 0 479844863 31318016 7062 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7646 7062 603 41 0 7605 0
vsize: 30584
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 7790 0 0 0 19975 27 0 0 25 0 1 0 479844863 34267136 7764 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8366 7764 603 41 0 8325 0
vsize: 33464
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 8459 0 0 0 20973 29 0 0 25 0 1 0 479844863 36958208 8433 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9023 8433 603 41 0 8982 0
vsize: 36092
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 9175 0 0 0 21970 32 0 0 25 0 1 0 479844863 39903232 9149 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9742 9149 603 41 0 9701 0
vsize: 38968
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 9827 0 0 0 22968 34 0 0 25 0 1 0 479844863 42582016 9801 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10396 9801 603 41 0 10355 0
vsize: 41584
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 10457 0 0 0 23966 36 0 0 25 0 1 0 479844863 45121536 10431 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11016 10431 603 41 0 10975 0
vsize: 44064
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 11003 0 0 0 24965 38 0 0 25 0 1 0 479844863 47276032 10977 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11542 10977 603 41 0 11501 0
vsize: 46168
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 11432 0 0 0 25964 39 0 0 25 0 1 0 479844863 49160192 11406 4294967295 134512640 134672761 3221224560 3221223728 134564764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12002 11406 603 41 0 11961 0
vsize: 48008
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 11981 0 0 0 26963 40 0 0 25 0 1 0 479844863 51302400 11955 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12525 11955 603 41 0 12484 0
vsize: 50100
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 12308 0 0 0 27962 41 0 0 25 0 1 0 479844863 52658176 12282 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12856 12282 603 41 0 12815 0
vsize: 51424
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 12489 0 0 0 28961 42 0 0 25 0 1 0 479844863 53465088 12463 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13053 12463 603 41 0 13012 0
vsize: 52212
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 13042 0 0 0 29961 42 0 0 25 0 1 0 479844863 55607296 13016 4294967295 134512640 134672761 3221224560 3221223664 134559958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13576 13016 603 41 0 13535 0
vsize: 54304
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 13293 0 0 0 30961 43 0 0 25 0 1 0 479844863 56692736 13267 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13841 13267 603 41 0 13800 0
vsize: 55364
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 13680 0 0 0 31960 44 0 0 25 0 1 0 479844863 58306560 13654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14235 13654 603 41 0 14194 0
vsize: 56940
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 13947 0 0 0 32959 45 0 0 25 0 1 0 479844863 59396096 13921 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14501 13921 603 41 0 14460 0
vsize: 58004
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 14349 0 0 0 33958 46 0 0 25 0 1 0 479844863 61538304 14323 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15024 14323 603 41 0 14983 0
vsize: 60096
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 14642 0 0 0 34957 47 0 0 25 0 1 0 479844863 62763008 14616 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15323 14616 603 41 0 15282 0
vsize: 61292
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 15137 0 0 0 35955 49 0 0 25 0 1 0 479844863 64774144 15111 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15814 15111 603 41 0 15773 0
vsize: 63256
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 15383 0 0 0 36955 50 0 0 25 0 1 0 479844863 65716224 15357 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16044 15358 603 41 0 16003 0
vsize: 64176
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 15700 0 0 0 37954 50 0 0 25 0 1 0 479844863 67063808 15674 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16373 15674 603 41 0 16332 0
vsize: 65492
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 16270 0 0 0 38954 51 0 0 25 0 1 0 479844863 69349376 16244 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16931 16244 603 41 0 16890 0
vsize: 67724
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 16444 0 0 0 39954 51 0 0 25 0 1 0 479844863 70025216 16418 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17096 16418 603 41 0 17055 0
vsize: 68384
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 16716 0 0 0 40953 52 0 0 25 0 1 0 479844863 71213056 16690 4294967295 134512640 134672761 3221224560 3221223576 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17386 16690 603 41 0 17345 0
vsize: 69544
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 16913 0 0 0 41953 52 0 0 25 0 1 0 479844863 72028160 16887 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17585 16887 603 41 0 17544 0
vsize: 70340
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 17197 0 0 0 42953 53 0 0 25 0 1 0 479844863 73236480 17171 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17880 17171 603 41 0 17839 0
vsize: 71520
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 17528 0 0 0 43952 54 0 0 25 0 1 0 479844863 74579968 17502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18208 17502 603 41 0 18167 0
vsize: 72832
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 17871 0 0 0 44951 54 0 0 25 0 1 0 479844863 75911168 17845 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18533 17845 603 41 0 18492 0
vsize: 74132
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 18113 0 0 0 45951 56 0 0 25 0 1 0 479844863 76984320 18087 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18795 18087 603 41 0 18754 0
vsize: 75180
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 18563 0 0 0 46950 57 0 0 25 0 1 0 479844863 78729216 18537 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19221 18537 603 41 0 19180 0
vsize: 76884
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 18863 0 0 0 47949 58 0 0 25 0 1 0 479844863 79941632 18837 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19517 18837 603 41 0 19476 0
vsize: 78068
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19205 0 0 0 48948 59 0 0 25 0 1 0 479844863 81412096 19179 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19876 19179 603 41 0 19835 0
vsize: 79504
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19461 0 0 0 49948 59 0 0 25 0 1 0 479844863 82489344 19435 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19435 603 41 0 20098 0
vsize: 80556
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19461 0 0 0 50948 59 0 0 25 0 1 0 479844863 82489344 19435 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19435 603 41 0 20098 0
vsize: 80556
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19461 0 0 0 51948 59 0 0 25 0 1 0 479844863 82489344 19435 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19435 603 41 0 20098 0
vsize: 80556
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19461 0 0 0 52948 59 0 0 25 0 1 0 479844863 82489344 19435 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19435 603 41 0 20098 0
vsize: 80556
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19462 0 0 0 53948 59 0 0 25 0 1 0 479844863 82489344 19436 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19436 603 41 0 20098 0
vsize: 80556
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19462 0 0 0 54948 59 0 0 25 0 1 0 479844863 82489344 19436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19436 603 41 0 20098 0
vsize: 80556
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19463 0 0 0 55948 59 0 0 25 0 1 0 479844863 82489344 19437 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19437 603 41 0 20098 0
vsize: 80556
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19463 0 0 0 56948 59 0 0 25 0 1 0 479844863 82489344 19437 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19437 603 41 0 20098 0
vsize: 80556
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19463 0 0 0 57949 59 0 0 25 0 1 0 479844863 82489344 19437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19437 603 41 0 20098 0
vsize: 80556
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 58949 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 59949 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 60949 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 61949 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223684 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 62950 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 63950 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 64950 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 65950 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 66950 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 67951 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 68951 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 69951 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 70951 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19464 0 0 0 71951 59 0 0 25 0 1 0 479844863 82489344 19438 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19438 603 41 0 20098 0
vsize: 80556
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19476 0 0 0 72951 60 0 0 25 0 1 0 479844863 82489344 19450 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20139 19450 603 41 0 20098 0
vsize: 80556
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 19826 0 0 0 73951 60 0 0 25 0 1 0 479844863 83976192 19800 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20502 19800 603 41 0 20461 0
vsize: 82008
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 20128 0 0 0 74951 61 0 0 25 0 1 0 479844863 85229568 20102 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20808 20102 603 41 0 20767 0
vsize: 83232
[startup+760.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 20415 0 0 0 75950 62 0 0 25 0 1 0 479844863 86302720 20389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21070 20389 603 41 0 21029 0
vsize: 84280
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 20746 0 0 0 76949 62 0 0 25 0 1 0 479844863 87748608 20720 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21423 20720 603 41 0 21382 0
vsize: 85692
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 21024 0 0 0 77949 63 0 0 25 0 1 0 479844863 89006080 20998 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21730 20998 603 41 0 21689 0
vsize: 86920
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 21285 0 0 0 78948 64 0 0 25 0 1 0 479844863 90025984 21259 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21979 21259 603 41 0 21938 0
vsize: 87916
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 21542 0 0 0 79948 65 0 0 25 0 1 0 479844863 91189248 21516 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22263 21516 603 41 0 22222 0
vsize: 89052
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 21857 0 0 0 80948 65 0 0 25 0 1 0 479844863 92536832 21831 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22592 21831 603 41 0 22551 0
vsize: 90368
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 22427 0 0 0 81944 68 0 0 25 0 1 0 479844863 94818304 22401 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23149 22401 603 41 0 23108 0
vsize: 92596
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 23124 0 0 0 82942 70 0 0 25 0 1 0 479844863 97640448 23098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23838 23098 603 41 0 23797 0
vsize: 95352
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 23755 0 0 0 83941 72 0 0 25 0 1 0 479844863 100327424 23729 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24494 23729 603 41 0 24453 0
vsize: 97976
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 24339 0 0 0 84940 73 0 0 25 0 1 0 479844863 102727680 24313 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25080 24313 603 41 0 25039 0
vsize: 100320
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 24782 0 0 0 85938 75 0 0 25 0 1 0 479844863 104542208 24756 4294967295 134512640 134672761 3221224560 3221223744 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25523 24756 603 41 0 25482 0
vsize: 102092
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 25157 0 0 0 86937 76 0 0 25 0 1 0 479844863 106160128 25131 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 25131 603 41 0 25877 0
vsize: 103672
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 25643 0 0 0 87936 77 0 0 25 0 1 0 479844863 108179456 25617 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 25617 603 41 0 26370 0
vsize: 105644
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 25990 0 0 0 88935 78 0 0 25 0 1 0 479844863 109563904 25964 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26749 25964 603 41 0 26708 0
vsize: 106996
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 26246 0 0 0 89935 79 0 0 25 0 1 0 479844863 110653440 26220 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27015 26220 603 41 0 26974 0
vsize: 108060
[startup+910.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 26469 0 0 0 90935 79 0 0 25 0 1 0 479844863 111616000 26443 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27250 26443 603 41 0 27209 0
vsize: 109000
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 26694 0 0 0 91935 79 0 0 25 0 1 0 479844863 112553984 26668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27479 26668 603 41 0 27438 0
vsize: 109916
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 26868 0 0 0 92934 80 0 0 25 0 1 0 479844863 113242112 26842 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27647 26842 603 41 0 27606 0
vsize: 110588
[startup+940.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 27178 0 0 0 93933 81 0 0 25 0 1 0 479844863 114577408 27152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27973 27152 603 41 0 27932 0
vsize: 111892
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 27683 0 0 0 94932 82 0 0 25 0 1 0 479844863 116576256 27657 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28461 27657 603 41 0 28420 0
vsize: 113844
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 28215 0 0 0 95931 83 0 0 25 0 1 0 479844863 118841344 28189 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29014 28189 603 41 0 28973 0
vsize: 116056
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 28581 0 0 0 96930 85 0 0 25 0 1 0 479844863 120332288 28555 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 28555 603 41 0 29337 0
vsize: 117512
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 28771 0 0 0 97929 86 0 0 25 0 1 0 479844863 121147392 28745 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29577 28745 603 41 0 29536 0
vsize: 118308
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 29111 0 0 0 98928 88 0 0 25 0 1 0 479844863 122494976 29085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29906 29085 603 41 0 29865 0
vsize: 119624
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 29382 0 0 0 99927 88 0 0 25 0 1 0 479844863 123568128 29356 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30168 29356 603 41 0 30127 0
vsize: 120672
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 29609 0 0 0 100926 89 0 0 25 0 1 0 479844863 124534784 29583 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30404 29583 603 41 0 30363 0
vsize: 121616
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 29868 0 0 0 101926 90 0 0 25 0 1 0 479844863 125640704 29842 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30674 29842 603 41 0 30633 0
vsize: 122696
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 30207 0 0 0 102925 91 0 0 25 0 1 0 479844863 126976000 30181 4294967295 134512640 134672761 3221224560 3221223728 134564676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31000 30181 603 41 0 30959 0
vsize: 124000
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 30445 0 0 0 103924 92 0 0 25 0 1 0 479844863 128065536 30419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31266 30419 603 41 0 31225 0
vsize: 125064
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 30730 0 0 0 104924 93 0 0 25 0 1 0 479844863 129134592 30704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31527 30704 603 41 0 31486 0
vsize: 126108
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 30974 0 0 0 105923 93 0 0 25 0 1 0 479844863 130220032 30948 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31792 30948 603 41 0 31751 0
vsize: 127168
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31369 0 0 0 106923 94 0 0 25 0 1 0 479844863 131821568 31343 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32183 31343 603 41 0 32142 0
vsize: 128732
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31471 0 0 0 107923 94 0 0 25 0 1 0 479844863 132227072 31445 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31445 603 41 0 32241 0
vsize: 129128
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31471 0 0 0 108923 94 0 0 25 0 1 0 479844863 132227072 31445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31445 603 41 0 32241 0
vsize: 129128
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31471 0 0 0 109923 94 0 0 25 0 1 0 479844863 132227072 31445 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31445 603 41 0 32241 0
vsize: 129128
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31471 0 0 0 110923 94 0 0 25 0 1 0 479844863 132227072 31445 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31445 603 41 0 32241 0
vsize: 129128
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31472 0 0 0 111923 95 0 0 25 0 1 0 479844863 132227072 31446 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31446 603 41 0 32241 0
vsize: 129128
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 112923 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223744 134559358 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 113924 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 114924 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 115924 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 116924 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 117924 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 118924 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31066
Raw data (stat): 31066 (minisat+) R 31065 28099 28098 0 -1 0 31473 0 0 0 119924 95 0 0 25 0 1 0 479844863 132227072 31447 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32282 31447 603 41 0 32241 0
vsize: 129128
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31066
Raw data (stat): 31066 (minisat+) Z 31065 28099 28098 0 -1 12 31475 0 0 0 119924 101 0 0 25 0 1 0 479844863 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.07
CPU time (s): 1200.26
CPU user time (s): 1199.25
CPU system time (s): 1.01085
CPU usage (%): 100.016
Max. virtual memory (Kb): 129128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####