PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-sp98ar.opb
MD5SUM	9565d6b3010c78b37c39352cc9731cb7
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	15085
Biggest coefficient in the objective function	504328818
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	2067304124713
Number of bits of the sum of numbers in the objective function	41
Biggest number in a constraint	504328818
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	2067304124713
Number of bits of the biggest sum of numbers	41
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	14.4348
Number of variables	15085
Total number of constraints	16520
Number of constraints which are clauses	181
Number of constraints which are cardinality constraints (but not clauses)	15927
Number of constraints which are nor clauses,nor cardinality constraints	412
Minimum length of a constraint	1
Maximum length of a constraint	4222
Trace number 13860

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        637016 kB
Buffers:         33464 kB
Cached:         330172 kB
SwapCached:        164 kB
Active:          86692 kB
Inactive:       279368 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        636764 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6088 kB
Slab:            25968 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:25:27 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 20264 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1430 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===
c   -- Clauses(.)/Splits(s): sssssss.sss..ss...s.....s...s.....ss.s..s...s.s..s.s.....s.s..sssss.......s....s........ss...s..sssssssss.ssssssss.sss..sss.ss..s.sssssss.ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssssssssssssssss.sssssssssssssssssssssssssss.sss.sssss..s.s...sssss..s.s..s..sssss.ss.ss...s..s.....s..ss.ssssss.s.ssssssss.s..sss.sssss.s.s..sssss.s.sss..sss.s.ssssssssssss..ssss........ss..s.s.sssssssssssssss.ssss.sssssssssssssssss.s.s.sss..s..ss.s.ssss.ssssssssssssssssss.ssssssssssssssssssssss.ss..ss.s.ssssssss.....sss..ss.......s.......ssss.....ssssss..ss
c ---[1816]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1815]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1814]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1813]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1812]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1811]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1810]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1809]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1808]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1807]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1805]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1804]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1803]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1802]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1801]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1800]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1799]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1798]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1797]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1796]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1794]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1793]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1792]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1791]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1790]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1789]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1788]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1787]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1786]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1785]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1783]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1782]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1781]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1780]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1779]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1778]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1777]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1776]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1775]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1774]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1772]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1770]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1769]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1768]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1767]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1766]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1765]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1763]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1762]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1761]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1760]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1759]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1758]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1757]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1756]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1755]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1754]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1752]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1751]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1750]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1749]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1748]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1747]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1746]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1745]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1744]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1743]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1741]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1740]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1739]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1738]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1737]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1736]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1735]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1734]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1733]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1732]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1731]---> Adder-cost: 928   maxlim: 9   bits: 5/4
c ---[1730]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1729]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1728]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1727]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1726]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1725]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1724]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1723]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1722]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1721]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1720]---> Adder-cost: 1283   maxlim: 26   bits: 6/5
c ---[1719]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1718]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1717]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1716]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1715]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1712]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1711]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1710]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1707]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1706]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1704]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1703]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1702]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1699]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1698]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1693]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1692]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1691]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1689]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1688]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1685]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1684]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1681]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1679]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1678]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1677]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1676]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1674]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1671]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1670]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1669]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1668]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1667]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1666]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1665]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1663]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1662]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1661]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1658]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1657]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1656]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1655]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1654]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1652]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1651]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1650]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1649]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1648]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1647]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1646]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1645]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[1644]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1643]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1641]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1640]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1639]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[1638]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1637]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1636]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1635]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1634]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1633]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1632]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[1630]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1629]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1628]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1627]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1626]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1625]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1624]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1623]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[1622]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1621]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1619]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1618]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1617]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1616]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1615]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1614]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1613]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1612]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1611]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1610]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1608]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1607]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1606]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1605]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1604]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1603]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1602]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1601]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1599]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1596]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1594]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1591]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1590]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1589]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1588]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1587]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1584]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1583]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1582]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1581]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1580]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1579]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1578]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1577]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1576]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1574]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1573]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1572]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1571]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1569]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1567]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1566]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1565]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1563]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1562]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1561]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1560]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1559]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1558]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1557]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1556]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1555]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1554]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1552]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1551]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1550]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1549]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[1548]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1547]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1546]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1545]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1544]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1543]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1541]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1540]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1539]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1538]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1537]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1536]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1535]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1534]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1533]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1532]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1530]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1529]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1527]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1524]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1519]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1518]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1517]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1516]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1515]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1514]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1513]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1512]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1511]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1509]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1508]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1507]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1504]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1503]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1502]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1501]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1500]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1498]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1497]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1496]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1495]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1494]---> Adder-cost: 40   maxlim: 24   bits: 5/5
c ---[1493]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1492]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1491]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1490]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1489]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1486]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1485]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1484]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1483]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1482]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1481]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1480]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1479]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1478]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1477]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1475]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1474]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1473]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1472]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1471]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[1470]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1469]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1468]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1467]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1466]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1464]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1462]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1458]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1457]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1456]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1455]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1453]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1451]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1450]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1449]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1448]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1447]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1445]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1444]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1442]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1441]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1440]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1438]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1436]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1433]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1431]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1429]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1428]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1427]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1426]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1425]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1424]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1423]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1422]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1420]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1418]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1417]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1416]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1415]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1414]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1413]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1412]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1411]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1408]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1406]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1404]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1403]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1402]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1401]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1399]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1398]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1397]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1396]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1395]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1394]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1393]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1392]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1391]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1390]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1388]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1387]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1386]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1385]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1384]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1383]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1382]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1381]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1380]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1379]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[1376]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1375]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1374]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1373]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1371]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1369]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1368]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1367]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1365]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1364]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1363]---> Adder-cost: 52   maxlim: 29   bits: 5/5
c ---[1362]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1361]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1360]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[1359]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1358]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1357]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1356]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[1355]---> Adder-cost: 481   maxlim: 9   bits: 5/4
c ---[1354]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1353]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1352]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1351]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1350]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1348]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1347]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1346]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[1345]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[1344]---> Adder-cost: 761   maxlim: 19   bits: 6/5
c ---[1343]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1342]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1341]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1339]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1338]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1333]---> Adder-cost: 250   maxlim: 5   bits: 4/3
c ---[1302]---> Adder-cost: 3486   maxlim: 9   bits: 5/4
c ---[1301]---> Adder-cost: 5783   maxlim: 27   bits: 6/5
c ---[1300]---> Adder-cost: 2665   maxlim: 7   bits: 4/3
c ---[1296]---> Adder-cost: 5240   maxlim: 9   bits: 5/4
c ---[1275]---> Adder-cost: 7841   maxlim: 5   bits: 4/3
c ---[1253]---> Adder-cost: 6003   maxlim: 7   bits: 4/3
c ---[1242]---> Adder-cost: 10495   maxlim: 29   bits: 6/5
c ---[1214]---> Adder-cost: 3653   maxlim: 17   bits: 6/5
c ---[1189]---> Adder-cost: 18   maxlim: 1   bits: 2/1
c ---[1184]---> Adder-cost: 18   maxlim: 1   bits: 2/1
c ---[1176]---> Adder-cost: 3076   maxlim: 5   bits: 4/3
c ---[1164]---> Adder-cost: 5657   maxlim: 29   bits: 6/5
c ---[1054]---> Adder-cost: 3028   maxlim: 5   bits: 4/3
c ---[1043]---> Adder-cost: 368   maxlim: 13   bits: 5/4
c ---[ 916]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 915]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 914]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 913]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 912]---> Adder-cost: 30   maxlim: 29   bits: 5/5
c ---[ 911]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[ 910]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 908]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[ 907]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[ 906]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 905]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 904]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 903]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 902]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 901]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 900]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 899]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 897]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 896]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 895]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 894]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 893]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 892]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 891]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 890]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 889]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 888]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 886]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 885]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 884]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 883]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 882]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 881]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 880]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 879]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 878]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 877]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 875]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 874]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[ 873]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 872]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 871]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 870]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 869]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[ 868]---> Adder-cost: 46   maxlim: 24   bits: 5/5
c ---[ 867]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 866]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 865]---> Adder-cost: 5142   maxlim: 5   bits: 4/3
c ---[ 864]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 863]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 862]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 861]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 860]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 859]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 858]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 857]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 856]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 855]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 853]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 852]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 851]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 850]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[ 849]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 848]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 847]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 846]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 845]---> Adder-cost: 30   maxlim: 20   bits: 5/5
c ---[ 844]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 842]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 841]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 840]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 839]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 838]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 837]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 836]---> Adder-cost: 32   maxlim: 24   bits: 5/5
c ---[ 835]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 834]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 833]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 830]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 829]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 828]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 827]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 826]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 825]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 824]---> Adder-cost: 48   maxlim: 26   bits: 5/5
c ---[ 823]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 822]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 821]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 819]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 818]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 817]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 816]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 815]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 814]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 813]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 811]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[ 810]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[ 808]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 807]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 806]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[ 805]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 804]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 803]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 802]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 801]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 800]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 799]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 797]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 796]---> Adder-cost: 36   maxlim: 26   bits: 5/5
c ---[ 795]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 794]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 793]---> Adder-cost: 38   maxlim: 26   bits: 5/5
c ---[ 792]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 791]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 790]---> Adder-cost: 30   maxlim: 29   bits: 5/5
c ---[ 789]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 788]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 786]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 785]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 784]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 782]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 781]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 780]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 779]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 778]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 777]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 775]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 774]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 772]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 771]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 770]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 769]---> Adder-cost: 32   maxlim: 22   bits: 5/5
c ---[ 768]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 767]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 766]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 764]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[ 763]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[ 762]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 761]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 760]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 759]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 758]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 757]---> Adder-cost: 34   maxlim: 26   bits: 5/5
c ---[ 756]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 755]---> Adder-cost: 30   maxlim: 29   bits: 5/5
c ---[ 753]---> Adder-cost: 30   maxlim: 29   bits: 5/5
c ---[ 752]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 751]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 750]---> Adder-cost: 30   maxlim: 20   bits: 5/5
c ---[ 749]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 748]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 747]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 746]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 745]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 744]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 742]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 741]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 740]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 739]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 738]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[ 737]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 736]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 735]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 734]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 733]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 731]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 730]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 729]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 728]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 727]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 726]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 725]---> Adder-cost: 32   maxlim: 24   bits: 5/5
c ---[ 724]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 723]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 722]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 719]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 718]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 717]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 716]---> Adder-cost: 40   maxlim: 24   bits: 5/5
c ---[ 715]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 714]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 713]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 712]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[ 711]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 710]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 708]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 707]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 706]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 705]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 704]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 703]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 702]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 701]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 700]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 699]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 697]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 696]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 695]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 694]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[ 693]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 692]---> Adder-cost: 36   maxlim: 29   bits: 5/5
c ---[ 691]---> Adder-cost: 36   maxlim: 29   bits: 5/5
c ---[ 690]---> Adder-cost: 36   maxlim: 29   bits: 5/5
c ---[ 689]---> Adder-cost: 36   maxlim: 29   bits: 5/5
c ---[ 688]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 685]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 684]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 683]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 681]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 679]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 678]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 677]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 675]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 674]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[ 673]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 672]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 671]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 670]---> Adder-cost: 34   maxlim: 26   bits: 5/5
c ---[ 669]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 668]---> Adder-cost: 42   maxlim: 29   bits: 5/5
c ---[ 667]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 666]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 664]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 663]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 662]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 661]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 660]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 659]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 658]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 657]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[ 656]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 655]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 653]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 652]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 651]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 650]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 649]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 648]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 647]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 646]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 645]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 644]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 642]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 641]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 640]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 639]---> Adder-cost: 42   maxlim: 23   bits: 5/5
c ---[ 638]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 637]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 636]---> Adder-cost: 42   maxlim: 23   bits: 5/5
c ---[ 635]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 634]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 633]---> Adder-cost: 38   maxlim: 26   bits: 5/5
c ---[ 631]---> Adder-cost: 46   maxlim: 29   bits: 5/5
c ---[ 630]---> Adder-cost: 42   maxlim: 29   bits: 5/5
c ---[ 629]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 628]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 627]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[ 626]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 625]---> Adder-cost: 32   maxlim: 20   bits: 5/5
c ---[ 624]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 623]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 622]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 620]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 619]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 618]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 617]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 616]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 615]---> Adder-cost: 34   maxlim: 24   bits: 5/5
c ---[ 614]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 613]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 612]---> Adder-cost: 42   maxlim: 23   bits: 5/5
c ---[ 611]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 608]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 607]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 606]---> Adder-cost: 44   maxlim: 27   bits: 5/5
c ---[ 605]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 604]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 603]---> Adder-cost: 34   maxlim: 24   bits: 5/5
c ---[ 602]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 601]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 599]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 595]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 594]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 593]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 592]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 591]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 589]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 588]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 586]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 584]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 583]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 582]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 581]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 579]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 577]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 574]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 573]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 571]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 570]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 569]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 568]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 567]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 566]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 564]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 563]---> Adder-cost: 38   maxlim: 24   bits: 5/5
c ---[ 562]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 561]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 560]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 559]---> Adder-cost: 36   maxlim: 26   bits: 5/5
c ---[ 558]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 557]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 556]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 555]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 554]---> Adder-cost: 5521   maxlim: 5   bits: 4/3
c ---[ 553]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 552]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 551]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 550]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 549]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 548]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 547]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 544]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 543]---> Adder-cost: 9320   maxlim: 11   bits: 5/4
c ---[ 542]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 540]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 539]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 537]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 536]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 535]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 534]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 533]---> Adder-cost: 36   maxlim: 24   bits: 5/5
c ---[ 531]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 530]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 529]---> Adder-cost: 36   maxlim: 26   bits: 5/5
c ---[ 528]---> Adder-cost: 38   maxlim: 29   bits: 5/5
c ---[ 527]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 526]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 525]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 524]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 523]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 522]---> Adder-cost: 42   maxlim: 24   bits: 5/5
c ---[ 520]---> Adder-cost: 48   maxlim: 26   bits: 5/5
c ---[ 519]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 518]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 517]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 516]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 515]---> Adder-cost: 42   maxlim: 23   bits: 5/5
c ---[ 514]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 513]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 512]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 511]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 509]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 508]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[ 507]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[ 506]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 505]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 504]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 503]---> Adder-cost: 38   maxlim: 29   bits: 5/5
c ---[ 502]---> Adder-cost: 48   maxlim: 26   bits: 5/5
c ---[ 501]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 500]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 497]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 496]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 495]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 493]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 492]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 490]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 489]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 486]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 485]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 484]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 483]---> Adder-cost: 42   maxlim: 22   bits: 5/5
c ---[ 482]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 481]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 480]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 479]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 478]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 477]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 475]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 474]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 473]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 472]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 471]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 470]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 469]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 468]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 467]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 466]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 464]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 463]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 462]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 461]---> Adder-cost: 38   maxlim: 26   bits: 5/5
c ---[ 460]---> Adder-cost: 26   maxlim: 20   bits: 5/5
c ---[ 459]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 458]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 457]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 456]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 455]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 453]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 452]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 451]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 450]---> Adder-cost: 44   maxlim: 26   bits: 5/5
c ---[ 449]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 448]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 447]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 446]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 445]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 444]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 442]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 441]---> Adder-cost: 40   maxlim: 23   bits: 5/5
c ---[ 440]---> Adder-cost: 30   maxlim: 29   bits: 5/5
c ---[ 439]---> Adder-cost: 42   maxlim: 24   bits: 5/5
c ---[ 438]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 437]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 436]---> Adder-cost: 42   maxlim: 26   bits: 5/5
c ---[ 435]---> Adder-cost: 32   maxlim: 29   bits: 5/5
c ---[ 434]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 433]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 431]---> Adder-cost: 40   maxlim: 22   bits: 5/5
c ---[ 430]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 429]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 428]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 427]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 426]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 425]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 424]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 423]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 422]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 420]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 418]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 417]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 416]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 415]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 414]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 413]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 410]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 409]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 408]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 407]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 406]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 405]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 404]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 403]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 402]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[ 401]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[ 399]---> Adder-cost: 48   maxlim: 26   bits: 5/5
c ---[ 398]---> Adder-cost: 34   maxlim: 29   bits: 5/5
c ---[ 397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 396]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 395]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[ 394]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 393]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 392]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 391]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 390]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 389]---> Adder-cost: 3215   maxlim: 3   bits: 3/2
c ---[ 388]---> Adder-cost: 443   maxlim: 1   bits: 2/1
c ---[ 387]---> Adder-cost: 417   maxlim: 1   bits: 2/1
c ---[ 386]---> Adder-cost: 90   maxlim: 2   bits: 3/2
c ---[ 385]---> Adder-cost: 396   maxlim: 1   bits: 2/1
c ---[ 384]---> Adder-cost: 210   maxlim: 3   bits: 3/2
c ---[ 383]---> Adder-cost: 89   maxlim: 3   bits: 3/2
c ---[ 382]---> Adder-cost: 96   maxlim: 7   bits: 4/3
c ---[ 381]---> Adder-cost: 12   maxlim: 1   bits: 2/1
c ---[ 380]---> Adder-cost: 5   maxlim: 3   bits: 3/2
c ---[ 379]---> Adder-cost: 2120   maxlim: 11   bits: 5/4
c ---[ 378]---> Adder-cost: 307   maxlim: 1   bits: 2/1
c ---[ 377]---> Adder-cost: 2941   maxlim: 19   bits: 6/5
c ---[ 376]---> Adder-cost: 706   maxlim: 3   bits: 3/2
c ---[ 375]---> Adder-cost: 20   maxlim: 1   bits: 2/1
c ---[ 374]---> Adder-cost: 168   maxlim: 1   bits: 2/1
c ---[ 373]---> Adder-cost: 59   maxlim: 2   bits: 3/2
c ---[ 372]---> Adder-cost: 98   maxlim: 3   bits: 3/2
c ---[ 371]---> Adder-cost: 312   maxlim: 1   bits: 2/1
c ---[ 370]---> Adder-cost: 322   maxlim: 1   bits: 2/1
c ---[ 369]---> Adder-cost: 57   maxlim: 2   bits: 3/2
c ---[ 368]---> Adder-cost: 9   maxlim: 1   bits: 2/1
c ---[ 367]---> Adder-cost: 17   maxlim: 1   bits: 2/1
c ---[ 366]---> Adder-cost: 62   maxlim: 1   bits: 2/1
c ---[ 365]---> Adder-cost: 144   maxlim: 1   bits: 2/1
c ---[ 364]---> Adder-cost: 786   maxlim: 10   bits: 5/4
c ---[ 363]---> Adder-cost: 65   maxlim: 2   bits: 3/2
c ---[ 362]---> Adder-cost: 309   maxlim: 1   bits: 2/1
c ---[ 361]---> Adder-cost: 1764   maxlim: 13   bits: 5/4
c ---[ 360]---> Adder-cost: 17   maxlim: 2   bits: 3/2
c ---[ 359]---> Adder-cost: 15   maxlim: 1   bits: 2/1
c ---[ 358]---> Adder-cost: 13   maxlim: 3   bits: 3/2
c ---[ 357]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 356]---> Adder-cost: 284   maxlim: 5   bits: 4/3
c ---[ 355]---> Adder-cost: 26   maxlim: 2   bits: 3/2
c ---[ 354]---> Adder-cost: 1013   maxlim: 3   bits: 3/2
c ---[ 353]---> Adder-cost: 881   maxlim: 8   bits: 5/4
c ---[ 352]---> Adder-cost: 113   maxlim: 3   bits: 3/2
c ---[ 351]---> Adder-cost: 19   maxlim: 3   bits: 3/2
c ---[ 350]---> Adder-cost: 12   maxlim: 1   bits: 2/1
c ---[ 349]---> Adder-cost: 448   maxlim: 3   bits: 3/2
c ---[ 348]---> Adder-cost: 5   maxlim: 3   bits: 3/2
c ---[ 347]---> Adder-cost: 2149   maxlim: 9   bits: 5/4
c ---[ 346]---> Adder-cost: 242   maxlim: 1   bits: 2/1
c ---[ 345]---> Adder-cost: 1850   maxlim: 3   bits: 3/2
c ---[ 344]---> Adder-cost: 1203   maxlim: 3   bits: 3/2
c ---[ 343]---> Adder-cost: 1200   maxlim: 7   bits: 4/3
c ---[ 342]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 341]---> Adder-cost: 20   maxlim: 3   bits: 3/2
c ---[ 340]---> Adder-cost: 232   maxlim: 4   bits: 4/3
c ---[ 339]---> Adder-cost: 30   maxlim: 1   bits: 2/1
c ---[ 338]---> Adder-cost: 66   maxlim: 4   bits: 4/3
c ---[ 337]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[ 336]---> Adder-cost: 283   maxlim: 1   bits: 2/1
c ---[ 335]---> Adder-cost: 247   maxlim: 3   bits: 3/2
c ---[ 334]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 333]---> Adder-cost: 44   maxlim: 1   bits: 2/1
c ---[ 332]---> Adder-cost: 3   maxlim: 1   bits: 2/1
c ---[ 331]---> Adder-cost: 41   maxlim: 1   bits: 2/1
c ---[ 330]---> Adder-cost: 57   maxlim: 3   bits: 3/2
c ---[ 329]---> Adder-cost: 14   maxlim: 2   bits: 3/2
c ---[ 328]---> Adder-cost: 8466   maxlim: 27   bits: 6/5
c ---[ 327]---> Adder-cost: 5944   maxlim: 12   bits: 5/4
c ---[ 326]---> Adder-cost: 123   maxlim: 1   bits: 2/1
c ---[ 325]---> Adder-cost: 93   maxlim: 3   bits: 3/2
c ---[ 324]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 323]---> Adder-cost: 5   maxlim: 2   bits: 3/2
c ---[ 322]---> Adder-cost: 58   maxlim: 1   bits: 2/1
c ---[ 321]---> Adder-cost: 138   maxlim: 1   bits: 2/1
c ---[ 320]---> Adder-cost: 2832   maxlim: 3   bits: 3/2
c ---[ 319]---> Adder-cost: 865   maxlim: 1   bits: 2/1
c ---[ 318]---> Adder-cost: 1927   maxlim: 4   bits: 4/3
c ---[ 317]---> Adder-cost: 460   maxlim: 1   bits: 2/1
c ---[ 316]---> Adder-cost: 838   maxlim: 4   bits: 4/3
c ---[ 315]---> Adder-cost: 792   maxlim: 9   bits: 5/4
c ---[ 314]---> Adder-cost: 255   maxlim: 1   bits: 2/1
c ---[ 313]---> Adder-cost: 696   maxlim: 8   bits: 5/4
c ---[ 312]---> Adder-cost: 3089   maxlim: 3   bits: 3/2
c ---[ 311]---> Adder-cost: 4581   maxlim: 11   bits: 5/4
c ---[ 310]---> Adder-cost: 2066   maxlim: 7   bits: 4/3
c ---[ 309]---> Adder-cost: 620   maxlim: 1   bits: 2/1
c ---[ 308]---> Adder-cost: 1017   maxlim: 9   bits: 5/4
c ---[ 307]---> Adder-cost: 188   maxlim: 1   bits: 2/1
c ---[ 306]---> Adder-cost: 89   maxlim: 1   bits: 2/1
c ---[ 305]---> Adder-cost: 225   maxlim: 6   bits: 4/3
c ---[ 304]---> Adder-cost: 64   maxlim: 1   bits: 2/1
c ---[ 303]---> Adder-cost: 123   maxlim: 4   bits: 4/3
c ---[ 302]---> Adder-cost: 442   maxlim: 9   bits: 5/4
c ---[ 301]---> Adder-cost: 265   maxlim: 1   bits: 2/1
c ---[ 300]---> Adder-cost: 339   maxlim: 5   bits: 4/3
c ---[ 299]---> Adder-cost: 10086   maxlim: 20   bits: 6/5
c ---[ 298]---> Adder-cost: 2433   maxlim: 3   bits: 3/2
c ---[ 297]---> Adder-cost: 1201   maxlim: 1   bits: 2/1
c ---[ 296]---> Adder-cost: 2335   maxlim: 10   bits: 5/4
c ---[ 295]---> Adder-cost: 840   maxlim: 1   bits: 2/1
c ---[ 294]---> Adder-cost: 1486   maxlim: 9   bits: 5/4
c ---[ 293]---> Adder-cost: 679   maxlim: 1   bits: 2/1
c ---[ 292]---> Adder-cost: 1166   maxlim: 7   bits: 4/3
c ---[ 291]---> Adder-cost: 559   maxlim: 1   bits: 2/1
c ---[ 290]---> Adder-cost: 1188   maxlim: 6   bits: 4/3
c ---[ 289]---> Adder-cost: 133   maxlim: 1   bits: 2/1
c ---[ 288]---> Adder-cost: 320   maxlim: 6   bits: 4/3
c ---[ 287]---> Adder-cost: 842   maxlim: 1   bits: 2/1
c ---[ 286]---> Adder-cost: 59   maxlim: 1   bits: 2/1
c ---[ 285]---> Adder-cost: 145   maxlim: 4   bits: 4/3
c ---[ 284]---> Adder-cost: 357   maxlim: 1   bits: 2/1
c ---[ 283]---> Adder-cost: 820   maxlim: 4   bits: 4/3
c ---[ 282]---> Adder-cost: 518   maxlim: 1   bits: 2/1
c ---[ 281]---> Adder-cost: 683   maxlim: 5   bits: 4/3
c ---[ 280]---> Adder-cost: 213   maxlim: 4   bits: 4/3
c ---[ 279]---> Adder-cost: 1041   maxlim: 13   bits: 5/4
c ---[ 278]---> Adder-cost: 124   maxlim: 1   bits: 2/1
c ---[ 277]---> Adder-cost: 40   maxlim: 1   bits: 2/1
c ---[ 276]---> Adder-cost: 384   maxlim: 6   bits: 4/3
c ---[ 275]---> Adder-cost: 124   maxlim: 1   bits: 2/1
c ---[ 274]---> Adder-cost: 3082   maxlim: 3   bits: 3/2
c ---[ 273]---> Adder-cost: 6180   maxlim: 12   bits: 5/4
c ---[ 272]---> Adder-cost: 314   maxlim: 1   bits: 2/1
c ---[ 271]---> Adder-cost: 939   maxlim: 8   bits: 5/4
c ---[ 270]---> Adder-cost: 458   maxlim: 1   bits: 2/1
c ---[ 269]---> Adder-cost: 676   maxlim: 9   bits: 5/4
c ---[ 268]---> Adder-cost: 3115   maxlim: 13   bits: 5/4
c ---[ 267]---> Adder-cost: 262   maxlim: 1   bits: 2/1
c ---[ 266]---> Adder-cost: 360   maxlim: 5   bits: 4/3
c ---[ 265]---> Adder-cost: 1342   maxlim: 8   bits: 5/4
c ---[ 264]---> Adder-cost: 228   maxlim: 1   bits: 2/1
c ---[ 263]---> Adder-cost: 355   maxlim: 5   bits: 4/3
c ---[ 262]---> Adder-cost: 2668   maxlim: 9   bits: 5/4
c ---[ 261]---> Adder-cost: 779   maxlim: 1   bits: 2/1
c ---[ 260]---> Adder-cost: 2378   maxlim: 8   bits: 5/4
c ---[ 259]---> Adder-cost: 952   maxlim: 1   bits: 2/1
c ---[ 258]---> Adder-cost: 525   maxlim: 7   bits: 4/3
c ---[ 257]---> Adder-cost: 95   maxlim: 1   bits: 2/1
c ---[ 256]---> Adder-cost: 196   maxlim: 4   bits: 4/3
c ---[ 255]---> Adder-cost: 3979   maxlim: 14   bits: 5/4
c ---[ 254]---> Adder-cost: 333   maxlim: 1   bits: 2/1
c ---[ 253]---> Adder-cost: 742   maxlim: 4   bits: 4/3
c ---[ 252]---> Adder-cost: 16   maxlim: 1   bits: 2/1
c ---[ 251]---> Adder-cost: 49   maxlim: 4   bits: 4/3
c ---[ 250]---> Adder-cost: 746   maxlim: 3   bits: 3/2
c ---[ 249]---> Adder-cost: 2060   maxlim: 16   bits: 6/5
c ---[ 248]---> Adder-cost: 64   maxlim: 3   bits: 3/2
c ---[ 247]---> Adder-cost: 5647   maxlim: 19   bits: 6/5
c ---[ 246]---> Adder-cost: 1635   maxlim: 14   bits: 5/4
c ---[ 245]---> Adder-cost: 1575   maxlim: 11   bits: 5/4
c ---[ 244]---> Adder-cost: 1452   maxlim: 9   bits: 5/4
c ---[ 243]---> Adder-cost: 535   maxlim: 5   bits: 4/3
c ---[ 242]---> Adder-cost: 819   maxlim: 9   bits: 5/4
c ---[ 241]---> Adder-cost: 2501   maxlim: 10   bits: 5/4
c ---[ 240]---> Adder-cost: 1871   maxlim: 6   bits: 4/3
c ---[ 239]---> Adder-cost: 237   maxlim: 4   bits: 4/3
c ---[ 238]---> Adder-cost: 230   maxlim: 1   bits: 2/1
c ---[ 237]---> Adder-cost: 1521   maxlim: 5   bits: 4/3
c ---[ 236]---> Adder-cost: 625   maxlim: 5   bits: 4/3
c ---[ 235]---> Adder-cost: 6997   maxlim: 20   bits: 6/5
c ---[ 234]---> Adder-cost: 449   maxlim: 4   bits: 4/3
c ---[ 233]---> Adder-cost: 263   maxlim: 4   bits: 4/3
c ---[ 232]---> Adder-cost: 8002   maxlim: 9   bits: 5/4
c ---[ 231]---> Adder-cost: 1007   maxlim: 1   bits: 2/1
c ---[ 230]---> Adder-cost: 215   maxlim: 2   bits: 3/2
c ---[ 229]---> Adder-cost: 888   maxlim: 2   bits: 3/2
c ---[ 228]---> Adder-cost: 70   maxlim: 3   bits: 3/2
c ---[ 227]---> Adder-cost: 765   maxlim: 10   bits: 5/4
c ---[ 226]---> Adder-cost: 2065   maxlim: 13   bits: 5/4
c ---[ 225]---> Adder-cost: 1412   maxlim: 9   bits: 5/4
c ---[ 224]---> Adder-cost: 21   maxlim: 2   bits: 3/2
c ---[ 223]---> Adder-cost: 414   maxlim: 1   bits: 2/1
c ---[ 222]---> Adder-cost: 116   maxlim: 2   bits: 3/2
c ---[ 221]---> Adder-cost: 48   maxlim: 1   bits: 2/1
c ---[ 220]---> Adder-cost: 53   maxlim: 4   bits: 4/3
c ---[ 219]---> Adder-cost: 1522   maxlim: 16   bits: 6/5
c ---[ 218]---> Adder-cost: 455   maxlim: 1   bits: 2/1
c ---[ 217]---> Adder-cost: 333   maxlim: 1   bits: 2/1
c ---[ 216]---> Adder-cost: 174   maxlim: 1   bits: 2/1
c ---[ 215]---> Adder-cost: 199   maxlim: 1   bits: 2/1
c ---[ 214]---> Adder-cost: 474   maxlim: 1   bits: 2/1
c ---[ 213]---> Adder-cost: 757   maxlim: 1   bits: 2/1
c ---[ 212]---> Adder-cost: 581   maxlim: 1   bits: 2/1
c ---[ 211]---> Adder-cost: 32   maxlim: 1   bits: 2/1
c ---[ 210]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 209]---> Adder-cost: 1431   maxlim: 9   bits: 5/4
c ---[ 208]---> Adder-cost: 25   maxlim: 1   bits: 2/1
c ---[ 207]---> Adder-cost: 1373   maxlim: 1   bits: 2/1
c ---[ 206]---> Adder-cost: 519   maxlim: 1   bits: 2/1
c ---[ 205]---> Adder-cost: 644   maxlim: 1   bits: 2/1
c ---[ 204]---> Adder-cost: 155   maxlim: 1   bits: 2/1
c ---[ 203]---> Adder-cost: 44   maxlim: 1   bits: 2/1
c ---[ 202]---> Adder-cost: 9   maxlim: 1   bits: 2/1
c ---[ 201]---> Adder-cost: 614   maxlim: 1   bits: 2/1
c ---[ 200]---> Adder-cost: 192   maxlim: 1   bits: 2/1
c ---[ 199]---> Adder-cost: 1228   maxlim: 1   bits: 2/1
c ---[ 198]---> Adder-cost: 14   maxlim: 1   bits: 2/1
c ---[ 197]---> Adder-cost: 291   maxlim: 1   bits: 2/1
c ---[ 196]---> Adder-cost: 84   maxlim: 1   bits: 2/1
c ---[ 195]---> Adder-cost: 10   maxlim: 1   bits: 2/1
c ---[ 194]---> Adder-cost: 749   maxlim: 1   bits: 2/1
c ---[ 193]---> Adder-cost: 1759   maxlim: 1   bits: 2/1
c ---[ 192]---> Adder-cost: 156   maxlim: 1   bits: 2/1
c ---[ 191]---> Adder-cost: 199   maxlim: 1   bits: 2/1
c ---[ 190]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 189]---> Adder-cost: 140   maxlim: 1   bits: 2/1
c ---[ 188]---> Adder-cost: 168   maxlim: 1   bits: 2/1
c ---[ 187]---> Adder-cost: 60   maxlim: 1   bits: 2/1
c ---[ 186]---> Adder-cost: 416   maxlim: 1   bits: 2/1
c ---[ 185]---> Adder-cost: 90   maxlim: 1   bits: 2/1
c ---[ 184]---> Adder-cost: 274   maxlim: 1   bits: 2/1
c ---[ 183]---> Adder-cost: 744   maxlim: 1   bits: 2/1
c ---[ 182]---> Adder-cost: 932   maxlim: 1   bits: 2/1
c ---[ 181]---> Adder-cost: 189   maxlim: 1   bits: 2/1
c ---[ 180]---> Adder-cost: 511   maxlim: 1   bits: 2/1
c ---[ 179]---> Adder-cost: 2196   maxlim: 1   bits: 2/1
c ---[ 178]---> Adder-cost: 508   maxlim: 2   bits: 3/2
c ---[ 177]---> Adder-cost: 364   maxlim: 2   bits: 3/2
c ---[ 176]---> Adder-cost: 356   maxlim: 3   bits: 3/2
c ---[ 175]---> Adder-cost: 245   maxlim: 2   bits: 3/2
c ---[ 174]---> Adder-cost: 857   maxlim: 2   bits: 3/2
c ---[ 173]---> Adder-cost: 1740   maxlim: 2   bits: 3/2
c ---[ 172]---> Adder-cost: 643   maxlim: 3   bits: 3/2
c ---[ 171]---> Adder-cost: 118   maxlim: 3   bits: 3/2
c ---[ 170]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 227   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 309   maxlim: 4   bits: 4/3
c ---[ 167]---> Adder-cost: 2522   maxlim: 3   bits: 3/2
c ---[ 166]---> Adder-cost: 1313   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 1255   maxlim: 3   bits: 3/2
c ---[ 164]---> Adder-cost: 765   maxlim: 3   bits: 3/2
c ---[ 163]---> Adder-cost: 590   maxlim: 3   bits: 3/2
c ---[ 162]---> Adder-cost: 192   maxlim: 5   bits: 4/3
c ---[ 161]---> Adder-cost: 1120   maxlim: 4   bits: 4/3
c ---[ 160]---> Adder-cost: 59   maxlim: 3   bits: 3/2
c ---[ 159]---> Adder-cost: 195   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 84   maxlim: 2   bits: 3/2
c ---[ 157]---> Adder-cost: 629   maxlim: 3   bits: 3/2
c ---[ 156]---> Adder-cost: 216   maxlim: 1   bits: 2/1
c ---[ 155]---> Adder-cost: 130   maxlim: 3   bits: 3/2
c ---[ 154]---> Adder-cost: 72   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 3412   maxlim: 3   bits: 3/2
c ---[ 152]---> Adder-cost: 552   maxlim: 5   bits: 4/3
c ---[ 151]---> Adder-cost: 419   maxlim: 2   bits: 3/2
c ---[ 150]---> Adder-cost: 309   maxlim: 4   bits: 4/3
c ---[ 149]---> Adder-cost: 51   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 600   maxlim: 3   bits: 3/2
c ---[ 147]---> Adder-cost: 818   maxlim: 2   bits: 3/2
c ---[ 146]---> Adder-cost: 929   maxlim: 2   bits: 3/2
c ---[ 145]---> Adder-cost: 163   maxlim: 2   bits: 3/2
c ---[ 144]---> Adder-cost: 63   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 68   maxlim: 4   bits: 4/3
c ---[ 142]---> Adder-cost: 32   maxlim: 1   bits: 2/1
c ---[ 141]---> Adder-cost: 47   maxlim: 4   bits: 4/3
c ---[ 140]---> Adder-cost: 423   maxlim: 2   bits: 3/2
c ---[ 139]---> Adder-cost: 655   maxlim: 2   bits: 3/2
c ---[ 138]---> Adder-cost: 3004   maxlim: 2   bits: 3/2
c ---[ 137]---> Adder-cost: 33   maxlim: 1   bits: 2/1
c ---[ 136]---> Adder-cost: 167   maxlim: 4   bits: 4/3
c ---[ 135]---> Adder-cost: 1987   maxlim: 3   bits: 3/2
c ---[ 134]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 133]---> Adder-cost: 186   maxlim: 3   bits: 3/2
c ---[ 132]---> Adder-cost: 1459   maxlim: 9   bits: 5/4
c ---[ 131]---> Adder-cost: 1547   maxlim: 16   bits: 6/5
c ---[ 130]---> Adder-cost: 21   maxlim: 1   bits: 2/1
c ---[ 129]---> Adder-cost: 356   maxlim: 1   bits: 2/1
c ---[ 128]---> Adder-cost: 373   maxlim: 1   bits: 2/1
c ---[ 127]---> Adder-cost: 18   maxlim: 1   bits: 2/1
c ---[ 126]---> Adder-cost: 743   maxlim: 1   bits: 2/1
c ---[ 125]---> Adder-cost: 22   maxlim: 1   bits: 2/1
c ---[ 124]---> Adder-cost: 371   maxlim: 1   bits: 2/1
c ---[ 123]---> Adder-cost: 69   maxlim: 1   bits: 2/1
c ---[ 122]---> Adder-cost: 23   maxlim: 3   bits: 3/2
c ---[ 121]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 120]---> Adder-cost: 188   maxlim: 1   bits: 2/1
c ---[ 119]---> Adder-cost: 156   maxlim: 1   bits: 2/1
c ---[ 118]---> Adder-cost: 6   maxlim: 1   bits: 2/1
c ---[ 117]---> Adder-cost: 188   maxlim: 1   bits: 2/1
c ---[ 116]---> Adder-cost: 138   maxlim: 1   bits: 2/1
c ---[ 115]---> Adder-cost: 65   maxlim: 1   bits: 2/1
c ---[ 114]---> Adder-cost: 767   maxlim: 1   bits: 2/1
c ---[ 113]---> Adder-cost: 1029   maxlim: 1   bits: 2/1
c ---[ 112]---> Adder-cost: 314   maxlim: 1   bits: 2/1
c ---[ 111]---> Adder-cost: 1828   maxlim: 1   bits: 2/1
c ---[ 110]---> Adder-cost: 364   maxlim: 3   bits: 3/2
c ---[ 109]---> Adder-cost: 773   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 86   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 145   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 1738   maxlim: 4   bits: 4/3
c ---[ 105]---> Adder-cost: 21   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 387   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 2703   maxlim: 4   bits: 4/3
c ---[ 102]---> Adder-cost: 171   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 486   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 49   maxlim: 4   bits: 4/3
c ---[  99]---> Adder-cost: 936   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 557   maxlim: 3   bits: 3/2
c ---[  97]---> Adder-cost: 50   maxlim: 4   bits: 4/3
c ---[  96]---> Adder-cost: 46   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 1286   maxlim: 3   bits: 3/2
c ---[  94]---> Adder-cost: 78   maxlim: 4   bits: 4/3
c ---[  93]---> Adder-cost: 1366   maxlim: 5   bits: 4/3
c ---[  92]---> Adder-cost: 67   maxlim: 5   bits: 4/3
c ---[  91]---> Adder-cost: 518   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 400   maxlim: 5   bits: 4/3
c ---[  89]---> Adder-cost: 1954   maxlim: 5   bits: 4/3
c ---[  88]---> Adder-cost: 4513   maxlim: 4   bits: 4/3
c ---[  87]---> Adder-cost: 2749   maxlim: 16   bits: 6/5
c ---[  86]---> Adder-cost: 45   maxlim: 1   bits: 2/1
c ---[  85]---> Adder-cost: 417   maxlim: 1   bits: 2/1
c ---[  84]---> Adder-cost: 1380   maxlim: 8   bits: 5/4
c ---[  83]---> Adder-cost: 325   maxlim: 1   bits: 2/1
c ---[  82]---> Adder-cost: 294   maxlim: 1   bits: 2/1
c ---[  81]---> Adder-cost: 382   maxlim: 1   bits: 2/1
c ---[  80]---> Adder-cost: 1155   maxlim: 1   bits: 2/1
c ---[  79]---> Adder-cost: 60   maxlim: 1   bits: 2/1
c ---[  78]---> Adder-cost: 1057   maxlim: 6   bits: 4/3
c ---[  77]---> Adder-cost: 112   maxlim: 1   bits: 2/1
c ---[  76]---> Adder-cost: 497   maxlim: 1   bits: 2/1
c ---[  75]---> Adder-cost: 1691   maxlim: 1   bits: 2/1
c ---[  74]---> Adder-cost: 420   maxlim: 5   bits: 4/3
c ---[  73]---> Adder-cost: 947   maxlim: 3   bits: 3/2
c ---[  72]---> Adder-cost: 1130   maxlim: 3   bits: 3/2
c ---[  71]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[  70]---> Adder-cost: 51   maxlim: 4   bits: 4/3
c ---[  69]---> Adder-cost: 2725   maxlim: 4   bits: 4/3
c ---[  68]---> Adder-cost: 1485   maxlim: 5   bits: 4/3
c ---[  67]---> Adder-cost: 1174   maxlim: 3   bits: 3/2
c ---[  66]---> Adder-cost: 138   maxlim: 1   bits: 2/1
c ---[  65]---> Adder-cost: 210   maxlim: 1   bits: 2/1
c ---[  64]---> Adder-cost: 350   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 19   maxlim: 1   bits: 2/1
c ---[  62]---> Adder-cost: 256   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 3765   maxlim: 14   bits: 5/4
c ---[  60]---> Adder-cost: 19   maxlim: 6   bits: 4/3
c ---[  59]---> Adder-cost: 32   maxlim: 1   bits: 2/1
c ---[  58]---> Adder-cost: 395   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 529   maxlim: 1   bits: 2/1
c ---[  56]---> Adder-cost: 104   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 2821   maxlim: 3   bits: 3/2
c ---[  54]---> Adder-cost: 1534   maxlim: 3   bits: 3/2
c ---[  53]---> Adder-cost: 651   maxlim: 3   bits: 3/2
c ---[  52]---> Adder-cost: 524   maxlim: 1   bits: 2/1
c ---[  51]---> Adder-cost: 231   maxlim: 1   bits: 2/1
c ---[  50]---> Adder-cost: 58   maxlim: 1   bits: 2/1
c ---[  49]---> Adder-cost: 12   maxlim: 1   bits: 2/1
c ---[  48]---> Adder-cost: 2795   maxlim: 5   bits: 4/3
c ---[  47]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 48   maxlim: 1   bits: 2/1
c ---[  45]---> Adder-cost: 91   maxlim: 4   bits: 4/3
c ---[  44]---> Adder-cost: 221   maxlim: 1   bits: 2/1
c ---[  43]---> Adder-cost: 1242   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 30   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 81   maxlim: 1   bits: 2/1
c ---[  40]---> Adder-cost: 1020   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 19   maxlim: 3   bits: 3/2
c ---[  38]---> Adder-cost: 40   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 4090   maxlim: 4   bits: 4/3
c ---[  36]---> Adder-cost: 3210   maxlim: 5   bits: 4/3
c ---[  35]---> Adder-cost: 120   maxlim: 1   bits: 2/1
c ---[  34]---> Adder-cost: 142   maxlim: 3   bits: 3/2
c ---[  33]---> Adder-cost: 572   maxlim: 1   bits: 2/1
c ---[  32]---> Adder-cost: 3885   maxlim: 14   bits: 5/4
c ---[  31]---> Adder-cost: 6566   maxlim: 20   bits: 6/5
c ---[  30]---> Adder-cost: 972   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 12   maxlim: 2   bits: 3/2
c ---[  28]---> Adder-cost: 69   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 513   maxlim: 3   bits: 3/2
c ---[  26]---> Adder-cost: 305   maxlim: 9   bits: 5/4
c ---[  25]---> Adder-cost: 161   maxlim: 3   bits: 3/2
c ---[  24]---> Adder-cost: 16   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 5   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 388   maxlim: 3   bits: 3/2
c ---[  20]---> Adder-cost: 1   maxlim: 3   bits: 3/2
c ---[  19]---> Adder-cost: 419   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 203   maxlim: 3   bits: 3/2
c ---[  17]---> Adder-cost: 98   maxlim: 4   bits: 4/3
c ---[  16]---> Adder-cost: 36   maxlim: 4   bits: 4/3
c ---[  15]---> Adder-cost: 84   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 945   maxlim: 3   bits: 3/2
c ---[  13]---> Adder-cost: 104   maxlim: 4   bits: 4/3
c ---[  12]---> Adder-cost: 298   maxlim: 1   bits: 2/1
c ---[  11]---> Adder-cost: 310   maxlim: 1   bits: 2/1
c ---[  10]---> Adder-cost: 880   maxlim: 1   bits: 2/1
c ---[   9]---> Adder-cost: 3515   maxlim: 9   bits: 5/4
c ---[   8]---> Adder-cost: 1536   maxlim: 14   bits: 5/4
c ---[   7]---> Adder-cost: 682   maxlim: 1   bits: 2/1
c ---[   6]---> Adder-cost: 450   maxlim: 3   bits: 3/2
c ---[   5]---> Adder-cost: 378   maxlim: 1   bits: 2/1
c ---[   4]---> Adder-cost: 278   maxlim: 3   bits: 3/2
c ---[   3]---> Adder-cost: 2896   maxlim: 3   bits: 3/2
c ---[   2]---> Adder-cost: 7367   maxlim: 18   bits: 6/5
c ---[   1]---> Adder-cost: 20   maxlim: 1   bits: 2/1
c ---[   0]---> Adder-cost: 23   maxlim: 3   bits: 3/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2111413  7914753 |  703804       0        0     nan |  0.000 % |
c |       100 | 2111413  7914753 |  774184     100      493     4.9 |  1.388 % |
c |       250 | 2111406  7914730 |  851602     249     1336     5.4 |  1.388 % |
c |       475 | 2111365  7914589 |  936763     471     2276     4.8 |  1.391 % |
c |       812 | 2111217  7914085 | 1030439     794     3730     4.7 |  1.399 % |
c |      1318 | 2110815  7912713 | 1133483    1267     6556     5.2 |  1.424 % |
c |      2077 | 2110080  7910209 | 1246831    1961     9601     4.9 |  1.468 % |
c |      3216 | 2109107  7906868 | 1371514    3011    14601     4.8 |  1.525 % |
c |      4925 | 2108490  7904729 | 1508666    4660    24040     5.2 |  1.557 % |
c |      7487 | 2107635  7901760 | 1659533    7127    53749     7.5 |  1.599 % |
c |     11333 | 2105785  7895320 | 1825486   10738    78359     7.3 |  1.688 % |
c |     17099 | 2103211  7886234 | 2008034   16189   119310     7.4 |  1.803 % |
#### 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.86 0.97 0.91 2/54 9431
Raw data (stat): 9431 (runsolver) R 9430 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539907006 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+9.99974 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 9431
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 33053 0 0 0 923 75 0 0 25 0 1 0 539907006 149852160 31507 4294967295 134512640 134672761 3221224544 3221222512 134556775 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36585 31508 603 41 0 36544 0
vsize: 146340
[startup+20.0007 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 9431
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 38506 0 0 0 1909 89 0 0 25 0 1 0 539907006 175276032 36960 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42792 36960 603 41 0 42751 0
vsize: 171168
[startup+30.0001 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 9431
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 38793 0 0 0 2908 90 0 0 25 0 1 0 539907006 176492544 37247 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43089 37247 603 41 0 43048 0
vsize: 172356
[startup+40.0008 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 9431
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 38847 0 0 0 3908 90 0 0 25 0 1 0 539907006 176762880 37301 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43155 37301 603 41 0 43114 0
vsize: 172620
[startup+50.0014 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 9431
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 39002 0 0 0 4907 90 0 0 25 0 1 0 539907006 177303552 37456 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43287 37456 603 41 0 43246 0
vsize: 173148
[startup+60.0011 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 39208 0 0 0 5907 91 0 0 25 0 1 0 539907006 178249728 37662 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43518 37662 603 41 0 43477 0
vsize: 174072
[startup+70.0008 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 39346 0 0 0 6907 91 0 0 25 0 1 0 539907006 178790400 37800 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43650 37800 603 41 0 43609 0
vsize: 174600
[startup+80.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 39497 0 0 0 7906 92 0 0 25 0 1 0 539907006 179331072 37951 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43782 37951 603 41 0 43741 0
vsize: 175128
[startup+90.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 39616 0 0 0 8906 92 0 0 25 0 1 0 539907006 179871744 38070 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43914 38070 603 41 0 43873 0
vsize: 175656
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 39778 0 0 0 9906 92 0 0 25 0 1 0 539907006 180547584 38232 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44079 38232 603 41 0 44038 0
vsize: 176316
[startup+110.007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40002 0 0 0 10907 93 0 0 25 0 1 0 539907006 181493760 38456 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44310 38456 603 41 0 44269 0
vsize: 177240
[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40170 0 0 0 11907 93 0 0 25 0 1 0 539907006 182169600 38624 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44475 38624 603 41 0 44434 0
vsize: 177900
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40321 0 0 0 12906 93 0 0 25 0 1 0 539907006 182710272 38775 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44607 38775 603 41 0 44566 0
vsize: 178428
[startup+140.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40462 0 0 0 13906 94 0 0 25 0 1 0 539907006 183250944 38916 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44739 38916 603 41 0 44698 0
vsize: 178956
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40566 0 0 0 14906 94 0 0 25 0 1 0 539907006 183656448 39020 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44838 39020 603 41 0 44797 0
vsize: 179352
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40637 0 0 0 15906 94 0 0 25 0 1 0 539907006 183926784 39091 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44904 39091 603 41 0 44863 0
vsize: 179616
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40732 0 0 0 16906 95 0 0 25 0 1 0 539907006 184332288 39186 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45003 39186 603 41 0 44962 0
vsize: 180012
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40768 0 0 0 17906 95 0 0 25 0 1 0 539907006 184467456 39222 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45036 39222 603 41 0 44995 0
vsize: 180144
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40831 0 0 0 18906 95 0 0 25 0 1 0 539907006 184737792 39285 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45102 39285 603 41 0 45061 0
vsize: 180408
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40861 0 0 0 19906 95 0 0 25 0 1 0 539907006 184872960 39315 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45135 39315 603 41 0 45094 0
vsize: 180540
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40899 0 0 0 20906 95 0 0 25 0 1 0 539907006 185008128 39353 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45168 39353 603 41 0 45127 0
vsize: 180672
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 40998 0 0 0 21905 96 0 0 25 0 1 0 539907006 185278464 39452 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45234 39452 603 41 0 45193 0
vsize: 180936
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41039 0 0 0 22905 96 0 0 25 0 1 0 539907006 185548800 39493 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45300 39493 603 41 0 45259 0
vsize: 181200
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41060 0 0 0 23906 96 0 0 25 0 1 0 539907006 185548800 39514 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45300 39514 603 41 0 45259 0
vsize: 181200
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41100 0 0 0 24906 96 0 0 25 0 1 0 539907006 185819136 39554 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45366 39554 603 41 0 45325 0
vsize: 181464
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41117 0 0 0 25906 96 0 0 25 0 1 0 539907006 185819136 39571 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45366 39571 603 41 0 45325 0
vsize: 181464
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41172 0 0 0 26906 96 0 0 25 0 1 0 539907006 186089472 39626 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45432 39626 603 41 0 45391 0
vsize: 181728
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41224 0 0 0 27906 97 0 0 25 0 1 0 539907006 186224640 39678 4294967295 134512640 134672761 3221224544 3221223744 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45465 39678 603 41 0 45424 0
vsize: 181860
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41251 0 0 0 28906 97 0 0 25 0 1 0 539907006 186359808 39705 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45498 39705 603 41 0 45457 0
vsize: 181992
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41266 0 0 0 29906 97 0 0 25 0 1 0 539907006 186359808 39720 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45498 39720 603 41 0 45457 0
vsize: 181992
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41300 0 0 0 30906 97 0 0 25 0 1 0 539907006 186494976 39754 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45531 39754 603 41 0 45490 0
vsize: 182124
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41310 0 0 0 31906 97 0 0 25 0 1 0 539907006 186494976 39764 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45531 39764 603 41 0 45490 0
vsize: 182124
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41320 0 0 0 32906 97 0 0 25 0 1 0 539907006 186630144 39774 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45564 39774 603 41 0 45523 0
vsize: 182256
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41329 0 0 0 33907 97 0 0 25 0 1 0 539907006 186630144 39783 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45564 39783 603 41 0 45523 0
vsize: 182256
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41341 0 0 0 34907 97 0 0 25 0 1 0 539907006 186630144 39795 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45564 39795 603 41 0 45523 0
vsize: 182256
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41357 0 0 0 35908 97 0 0 25 0 1 0 539907006 186765312 39811 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45597 39811 603 41 0 45556 0
vsize: 182388
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41384 0 0 0 36907 97 0 0 25 0 1 0 539907006 186765312 39838 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45597 39838 603 41 0 45556 0
vsize: 182388
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41397 0 0 0 37908 97 0 0 25 0 1 0 539907006 186900480 39851 4294967295 134512640 134672761 3221224544 3221223792 134562294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45630 39851 603 41 0 45589 0
vsize: 182520
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41415 0 0 0 38908 97 0 0 25 0 1 0 539907006 186900480 39869 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45630 39869 603 41 0 45589 0
vsize: 182520
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41430 0 0 0 39908 97 0 0 25 0 1 0 539907006 186900480 39884 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45630 39884 603 41 0 45589 0
vsize: 182520
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41436 0 0 0 40908 97 0 0 25 0 1 0 539907006 187035648 39890 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45663 39890 603 41 0 45622 0
vsize: 182652
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41441 0 0 0 41908 97 0 0 25 0 1 0 539907006 187035648 39895 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45663 39895 603 41 0 45622 0
vsize: 182652
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41445 0 0 0 42908 97 0 0 25 0 1 0 539907006 187035648 39899 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45663 39899 603 41 0 45622 0
vsize: 182652
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41458 0 0 0 43909 97 0 0 25 0 1 0 539907006 187174912 39912 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45697 39912 603 41 0 45656 0
vsize: 182788
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41475 0 0 0 44908 97 0 0 25 0 1 0 539907006 187174912 39929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45697 39929 603 41 0 45656 0
vsize: 182788
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41483 0 0 0 45909 97 0 0 25 0 1 0 539907006 187174912 39937 4294967295 134512640 134672761 3221224544 3221223696 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45697 39937 603 41 0 45656 0
vsize: 182788
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41486 0 0 0 46909 97 0 0 25 0 1 0 539907006 187174912 39940 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45697 39940 603 41 0 45656 0
vsize: 182788
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41490 0 0 0 47909 97 0 0 25 0 1 0 539907006 187174912 39944 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45697 39944 603 41 0 45656 0
vsize: 182788
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41496 0 0 0 48909 97 0 0 25 0 1 0 539907006 187310080 39950 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45730 39950 603 41 0 45689 0
vsize: 182920
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41502 0 0 0 49910 97 0 0 25 0 1 0 539907006 187310080 39956 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45730 39956 603 41 0 45689 0
vsize: 182920
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41508 0 0 0 50910 97 0 0 25 0 1 0 539907006 187310080 39962 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45730 39962 603 41 0 45689 0
vsize: 182920
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41529 0 0 0 51910 97 0 0 25 0 1 0 539907006 187310080 39983 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45730 39983 603 41 0 45689 0
vsize: 182920
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41539 0 0 0 52910 97 0 0 25 0 1 0 539907006 187310080 39993 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45730 39993 603 41 0 45689 0
vsize: 182920
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41550 0 0 0 53910 97 0 0 25 0 1 0 539907006 187445248 40004 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45763 40004 603 41 0 45722 0
vsize: 183052
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41553 0 0 0 54910 97 0 0 25 0 1 0 539907006 187445248 40007 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45763 40007 603 41 0 45722 0
vsize: 183052
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41557 0 0 0 55910 98 0 0 25 0 1 0 539907006 187445248 40011 4294967295 134512640 134672761 3221224544 3221223712 134564689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45763 40011 603 41 0 45722 0
vsize: 183052
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41560 0 0 0 56911 98 0 0 25 0 1 0 539907006 187445248 40014 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45763 40014 603 41 0 45722 0
vsize: 183052
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41563 0 0 0 57911 98 0 0 25 0 1 0 539907006 187445248 40017 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45763 40017 603 41 0 45722 0
vsize: 183052
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41582 0 0 0 58910 98 0 0 25 0 1 0 539907006 187445248 40036 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45763 40036 603 41 0 45722 0
vsize: 183052
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41596 0 0 0 59910 98 0 0 25 0 1 0 539907006 187580416 40050 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45796 40050 603 41 0 45755 0
vsize: 183184
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41601 0 0 0 60911 98 0 0 25 0 1 0 539907006 187580416 40055 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45796 40055 603 41 0 45755 0
vsize: 183184
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41604 0 0 0 61912 98 0 0 25 0 1 0 539907006 187580416 40058 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45796 40058 603 41 0 45755 0
vsize: 183184
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41607 0 0 0 62912 98 0 0 25 0 1 0 539907006 187580416 40061 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45796 40061 603 41 0 45755 0
vsize: 183184
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41610 0 0 0 63912 98 0 0 25 0 1 0 539907006 187580416 40064 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45796 40064 603 41 0 45755 0
vsize: 183184
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41617 0 0 0 64912 98 0 0 25 0 1 0 539907006 187580416 40071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45796 40071 603 41 0 45755 0
vsize: 183184
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41627 0 0 0 65912 98 0 0 25 0 1 0 539907006 187715584 40081 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45829 40081 603 41 0 45788 0
vsize: 183316
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41633 0 0 0 66912 98 0 0 25 0 1 0 539907006 187715584 40087 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45829 40087 603 41 0 45788 0
vsize: 183316
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41639 0 0 0 67912 98 0 0 25 0 1 0 539907006 187715584 40093 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45829 40093 603 41 0 45788 0
vsize: 183316
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41645 0 0 0 68913 98 0 0 25 0 1 0 539907006 187715584 40099 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45829 40099 603 41 0 45788 0
vsize: 183316
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41656 0 0 0 69913 98 0 0 25 0 1 0 539907006 187715584 40110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45829 40110 603 41 0 45788 0
vsize: 183316
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41677 0 0 0 70913 98 0 0 25 0 1 0 539907006 187850752 40131 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45862 40131 603 41 0 45821 0
vsize: 183448
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41678 0 0 0 71913 98 0 0 25 0 1 0 539907006 187850752 40132 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45862 40132 603 41 0 45821 0
vsize: 183448
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41689 0 0 0 72913 98 0 0 25 0 1 0 539907006 187850752 40143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45862 40143 603 41 0 45821 0
vsize: 183448
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41704 0 0 0 73913 98 0 0 25 0 1 0 539907006 187850752 40158 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45862 40158 603 41 0 45821 0
vsize: 183448
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41710 0 0 0 74913 98 0 0 25 0 1 0 539907006 187985920 40164 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40164 603 41 0 45854 0
vsize: 183580
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41719 0 0 0 75914 98 0 0 25 0 1 0 539907006 187985920 40173 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40173 603 41 0 45854 0
vsize: 183580
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41728 0 0 0 76914 98 0 0 25 0 1 0 539907006 187985920 40182 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40182 603 41 0 45854 0
vsize: 183580
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41734 0 0 0 77914 98 0 0 25 0 1 0 539907006 187985920 40188 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40188 603 41 0 45854 0
vsize: 183580
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41738 0 0 0 78914 98 0 0 25 0 1 0 539907006 187985920 40192 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40192 603 41 0 45854 0
vsize: 183580
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41743 0 0 0 79914 98 0 0 25 0 1 0 539907006 187985920 40197 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40197 603 41 0 45854 0
vsize: 183580
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41747 0 0 0 80914 98 0 0 25 0 1 0 539907006 187985920 40201 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40201 603 41 0 45854 0
vsize: 183580
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41750 0 0 0 81915 98 0 0 25 0 1 0 539907006 187985920 40204 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45895 40204 603 41 0 45854 0
vsize: 183580
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41753 0 0 0 82915 98 0 0 25 0 1 0 539907006 188121088 40207 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40207 603 41 0 45887 0
vsize: 183712
[startup+840.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41756 0 0 0 83915 98 0 0 25 0 1 0 539907006 188121088 40210 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40210 603 41 0 45887 0
vsize: 183712
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41758 0 0 0 84915 98 0 0 25 0 1 0 539907006 188121088 40212 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40212 603 41 0 45887 0
vsize: 183712
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41760 0 0 0 85915 98 0 0 25 0 1 0 539907006 188121088 40214 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40214 603 41 0 45887 0
vsize: 183712
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41763 0 0 0 86916 98 0 0 25 0 1 0 539907006 188121088 40217 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40217 603 41 0 45887 0
vsize: 183712
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41765 0 0 0 87916 98 0 0 25 0 1 0 539907006 188121088 40219 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40219 603 41 0 45887 0
vsize: 183712
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41766 0 0 0 88916 98 0 0 25 0 1 0 539907006 188121088 40220 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40220 603 41 0 45887 0
vsize: 183712
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41767 0 0 0 89916 98 0 0 25 0 1 0 539907006 188121088 40221 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40221 603 41 0 45887 0
vsize: 183712
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41770 0 0 0 90916 99 0 0 25 0 1 0 539907006 188121088 40224 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40224 603 41 0 45887 0
vsize: 183712
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41794 0 0 0 91915 99 0 0 25 0 1 0 539907006 188338176 40248 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40248 603 41 0 45940 0
vsize: 183924
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41799 0 0 0 92915 99 0 0 25 0 1 0 539907006 188338176 40253 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40253 603 41 0 45940 0
vsize: 183924
[startup+940.028 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41799 0 0 0 93916 99 0 0 25 0 1 0 539907006 188338176 40253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40253 603 41 0 45940 0
vsize: 183924
[startup+950.027 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41799 0 0 0 94916 99 0 0 25 0 1 0 539907006 188338176 40253 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40253 603 41 0 45940 0
vsize: 183924
[startup+960.027 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41799 0 0 0 95916 99 0 0 25 0 1 0 539907006 188338176 40253 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40253 603 41 0 45940 0
vsize: 183924
[startup+970.027 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41800 0 0 0 96916 99 0 0 25 0 1 0 539907006 188338176 40254 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40254 603 41 0 45940 0
vsize: 183924
[startup+980.031 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41802 0 0 0 97917 99 0 0 25 0 1 0 539907006 188338176 40256 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40256 603 41 0 45940 0
vsize: 183924
[startup+990.035 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41805 0 0 0 98917 99 0 0 25 0 1 0 539907006 188338176 40259 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40259 603 41 0 45940 0
vsize: 183924
[startup+1000.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41815 0 0 0 99917 99 0 0 25 0 1 0 539907006 188338176 40269 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40269 603 41 0 45940 0
vsize: 183924
[startup+1010.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41817 0 0 0 100918 99 0 0 25 0 1 0 539907006 188338176 40271 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40271 603 41 0 45940 0
vsize: 183924
[startup+1020.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41824 0 0 0 101918 99 0 0 25 0 1 0 539907006 188338176 40278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40278 603 41 0 45940 0
vsize: 183924
[startup+1030.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41826 0 0 0 102918 99 0 0 25 0 1 0 539907006 188338176 40280 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40280 603 41 0 45940 0
vsize: 183924
[startup+1040.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41828 0 0 0 103918 99 0 0 25 0 1 0 539907006 188338176 40282 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40282 603 41 0 45940 0
vsize: 183924
[startup+1050.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41831 0 0 0 104918 99 0 0 25 0 1 0 539907006 188338176 40285 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40285 603 41 0 45940 0
vsize: 183924
[startup+1060.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41834 0 0 0 105918 99 0 0 25 0 1 0 539907006 188338176 40288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40288 603 41 0 45940 0
vsize: 183924
[startup+1070.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41839 0 0 0 106919 99 0 0 25 0 1 0 539907006 188338176 40293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40293 603 41 0 45940 0
vsize: 183924
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41841 0 0 0 107919 99 0 0 25 0 1 0 539907006 188338176 40295 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45981 40295 603 41 0 45940 0
vsize: 183924
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41846 0 0 0 108919 99 0 0 25 0 1 0 539907006 188473344 40300 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46014 40300 603 41 0 45973 0
vsize: 184056
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41894 0 0 0 109919 99 0 0 25 0 1 0 539907006 188608512 40348 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40348 603 41 0 46006 0
vsize: 184188
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41901 0 0 0 110919 99 0 0 25 0 1 0 539907006 188608512 40355 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40355 603 41 0 46006 0
vsize: 184188
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41903 0 0 0 111920 99 0 0 25 0 1 0 539907006 188608512 40357 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40357 603 41 0 46006 0
vsize: 184188
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41904 0 0 0 112920 99 0 0 25 0 1 0 539907006 188608512 40358 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40358 603 41 0 46006 0
vsize: 184188
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41907 0 0 0 113920 99 0 0 25 0 1 0 539907006 188608512 40361 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40361 603 41 0 46006 0
vsize: 184188
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41908 0 0 0 114920 99 0 0 25 0 1 0 539907006 188608512 40362 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40362 603 41 0 46006 0
vsize: 184188
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41909 0 0 0 115920 99 0 0 25 0 1 0 539907006 188608512 40363 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40363 603 41 0 46006 0
vsize: 184188
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41910 0 0 0 116921 99 0 0 25 0 1 0 539907006 188608512 40364 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40364 603 41 0 46006 0
vsize: 184188
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41912 0 0 0 117921 99 0 0 25 0 1 0 539907006 188608512 40366 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 40366 603 41 0 46006 0
vsize: 184188
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41915 0 0 0 118921 99 0 0 25 0 1 0 539907006 188743680 40369 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46080 40369 603 41 0 46039 0
vsize: 184320
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9433
Raw data (stat): 9431 (minisat+) R 9430 10614 10613 0 -1 0 41916 0 0 0 119921 99 0 0 25 0 1 0 539907006 188743680 40370 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46080 40370 603 41 0 46039 0
vsize: 184320
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 9433
Raw data (stat): 9431 (minisat+) Z 9430 10614 10613 0 -1 12 41918 0 0 0 119921 107 0 0 25 0 1 0 539907006 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.12
CPU time (s): 1200.29
CPU user time (s): 1199.22
CPU system time (s): 1.07384
CPU usage (%): 100.014
Max. virtual memory (Kb): 184320
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####