PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-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	13.9929
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 20243

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 20:27:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15259 boxname=wulflinc12 idbench=1174 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9565d6b3010c78b37c39352cc9731cb7  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-sp98ar.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-sp98ar.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-sp98ar.opb
IDLAUNCH: 15259
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 2
cpu MHz		: 451.091
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:        515656 kB
Buffers:         32892 kB
Cached:         463884 kB
SwapCached:        508 kB
Active:         103788 kB
Inactive:       395128 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        515404 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            14340 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 20:47:57 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 15259 7 1200.36 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.92 0.88 0.86 2/54 4944
Raw data (stat): 4944 (runsolver) R 4943 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489733258 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.88 0.86 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 33240 0 0 0 921 77 0 0 25 0 1 0 489733258 150392832 31694 4294967295 134512640 134672761 3221224544 3221221024 134542089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36717 31695 603 41 0 36676 0
vsize: 146868
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.89 0.86 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 38506 0 0 0 1909 89 0 0 25 0 1 0 489733258 175276032 36960 4294967295 134512640 134672761 3221224544 3221223740 134556678 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.002 s]
Raw data (loadavg): 0.95 0.89 0.86 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 38793 0 0 0 2908 90 0 0 25 0 1 0 489733258 176492544 37247 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0029 s]
Raw data (loadavg): 0.96 0.89 0.86 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 38847 0 0 0 3908 91 0 0 25 0 1 0 489733258 176762880 37301 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.0047 s]
Raw data (loadavg): 0.96 0.90 0.86 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 38999 0 0 0 4907 91 0 0 25 0 1 0 489733258 177303552 37453 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43287 37453 603 41 0 43246 0
vsize: 173148
[startup+60.0054 s]
Raw data (loadavg): 0.97 0.90 0.86 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 39202 0 0 0 5907 92 0 0 25 0 1 0 489733258 178114560 37656 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43485 37656 603 41 0 43444 0
vsize: 173940
[startup+70.0119 s]
Raw data (loadavg): 0.97 0.90 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 39346 0 0 0 6907 93 0 0 25 0 1 0 489733258 178790400 37800 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0131 s]
Raw data (loadavg): 0.98 0.90 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 39497 0 0 0 7906 94 0 0 25 0 1 0 489733258 179331072 37951 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0129 s]
Raw data (loadavg): 0.98 0.91 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 39593 0 0 0 8906 94 0 0 25 0 1 0 489733258 179736576 38047 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43881 38047 603 41 0 43840 0
vsize: 175524
[startup+100.014 s]
Raw data (loadavg): 0.98 0.91 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 39778 0 0 0 9905 95 0 0 25 0 1 0 489733258 180547584 38232 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.015 s]
Raw data (loadavg): 0.98 0.91 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 39984 0 0 0 10904 96 0 0 25 0 1 0 489733258 181358592 38438 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44277 38438 603 41 0 44236 0
vsize: 177108
[startup+120.015 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40134 0 0 0 11904 97 0 0 25 0 1 0 489733258 182034432 38588 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44442 38588 603 41 0 44401 0
vsize: 177768
[startup+130.016 s]
Raw data (loadavg): 0.99 0.92 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40299 0 0 0 12903 97 0 0 25 0 1 0 489733258 182575104 38753 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44574 38753 603 41 0 44533 0
vsize: 178296
[startup+140.016 s]
Raw data (loadavg): 0.99 0.92 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40456 0 0 0 13903 98 0 0 25 0 1 0 489733258 183250944 38910 4294967295 134512640 134672761 3221224544 3221223808 134562225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44739 38910 603 41 0 44698 0
vsize: 178956
[startup+150.017 s]
Raw data (loadavg): 0.99 0.92 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40564 0 0 0 14903 98 0 0 25 0 1 0 489733258 183656448 39018 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44838 39018 603 41 0 44797 0
vsize: 179352
[startup+160.018 s]
Raw data (loadavg): 0.99 0.92 0.87 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40636 0 0 0 15903 98 0 0 25 0 1 0 489733258 183926784 39090 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44904 39090 603 41 0 44863 0
vsize: 179616
[startup+170.018 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40728 0 0 0 16903 98 0 0 25 0 1 0 489733258 184332288 39182 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45003 39182 603 41 0 44962 0
vsize: 180012
[startup+180.018 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40768 0 0 0 17903 98 0 0 25 0 1 0 489733258 184467456 39222 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45036 39222 603 41 0 44995 0
vsize: 180144
[startup+190.019 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40831 0 0 0 18903 99 0 0 25 0 1 0 489733258 184737792 39285 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45102 39285 603 41 0 45061 0
vsize: 180408
[startup+200.02 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40861 0 0 0 19904 99 0 0 25 0 1 0 489733258 184872960 39315 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45135 39315 603 41 0 45094 0
vsize: 180540
[startup+210.021 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40897 0 0 0 20904 99 0 0 25 0 1 0 489733258 185008128 39351 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45168 39351 603 41 0 45127 0
vsize: 180672
[startup+220.022 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 40997 0 0 0 21904 99 0 0 25 0 1 0 489733258 185278464 39451 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45234 39451 603 41 0 45193 0
vsize: 180936
[startup+230.034 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41039 0 0 0 22905 99 0 0 25 0 1 0 489733258 185548800 39493 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45300 39493 603 41 0 45259 0
vsize: 181200
[startup+240.034 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41055 0 0 0 23905 99 0 0 25 0 1 0 489733258 185548800 39509 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45300 39509 603 41 0 45259 0
vsize: 181200
[startup+250.035 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41090 0 0 0 24905 99 0 0 25 0 1 0 489733258 185683968 39544 4294967295 134512640 134672761 3221224544 3221223696 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45333 39544 603 41 0 45292 0
vsize: 181332
[startup+260.036 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41116 0 0 0 25906 99 0 0 25 0 1 0 489733258 185819136 39570 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45366 39570 603 41 0 45325 0
vsize: 181464
[startup+270.036 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41169 0 0 0 26906 99 0 0 25 0 1 0 489733258 185954304 39623 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45399 39623 603 41 0 45358 0
vsize: 181596
[startup+280.037 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41222 0 0 0 27906 99 0 0 25 0 1 0 489733258 186224640 39676 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45465 39676 603 41 0 45424 0
vsize: 181860
[startup+290.038 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41249 0 0 0 28906 99 0 0 25 0 1 0 489733258 186224640 39703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45465 39703 603 41 0 45424 0
vsize: 181860
[startup+300.037 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41265 0 0 0 29906 99 0 0 25 0 1 0 489733258 186359808 39719 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45498 39719 603 41 0 45457 0
vsize: 181992
[startup+310.037 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41299 0 0 0 30906 100 0 0 25 0 1 0 489733258 186494976 39753 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45531 39753 603 41 0 45490 0
vsize: 182124
[startup+320.037 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41306 0 0 0 31906 100 0 0 25 0 1 0 489733258 186494976 39760 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45531 39760 603 41 0 45490 0
vsize: 182124
[startup+330.038 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41318 0 0 0 32907 100 0 0 25 0 1 0 489733258 186494976 39772 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45531 39772 603 41 0 45490 0
vsize: 182124
[startup+340.038 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41328 0 0 0 33907 100 0 0 25 0 1 0 489733258 186630144 39782 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45564 39782 603 41 0 45523 0
vsize: 182256
[startup+350.038 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41341 0 0 0 34907 100 0 0 25 0 1 0 489733258 186630144 39795 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45564 39795 603 41 0 45523 0
vsize: 182256
[startup+360.038 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41356 0 0 0 35907 100 0 0 25 0 1 0 489733258 186765312 39810 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45597 39810 603 41 0 45556 0
vsize: 182388
[startup+370.038 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41384 0 0 0 36907 100 0 0 25 0 1 0 489733258 186765312 39838 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45597 39838 603 41 0 45556 0
vsize: 182388
[startup+380.039 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41395 0 0 0 37907 100 0 0 25 0 1 0 489733258 186900480 39849 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45630 39849 603 41 0 45589 0
vsize: 182520
[startup+390.039 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41415 0 0 0 38907 100 0 0 25 0 1 0 489733258 186900480 39869 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45630 39869 603 41 0 45589 0
vsize: 182520
[startup+400.039 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41429 0 0 0 39907 100 0 0 25 0 1 0 489733258 186900480 39883 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45630 39883 603 41 0 45589 0
vsize: 182520
[startup+410.04 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41436 0 0 0 40907 100 0 0 25 0 1 0 489733258 187035648 39890 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45663 39890 603 41 0 45622 0
vsize: 182652
[startup+420.039 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41441 0 0 0 41908 100 0 0 25 0 1 0 489733258 187035648 39895 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45663 39895 603 41 0 45622 0
vsize: 182652
[startup+430.04 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41444 0 0 0 42908 100 0 0 25 0 1 0 489733258 187035648 39898 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45663 39898 603 41 0 45622 0
vsize: 182652
[startup+440.04 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41458 0 0 0 43908 100 0 0 25 0 1 0 489733258 187174912 39912 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45697 39912 603 41 0 45656 0
vsize: 182788
[startup+450.04 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41475 0 0 0 44908 100 0 0 25 0 1 0 489733258 187174912 39929 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45697 39929 603 41 0 45656 0
vsize: 182788
[startup+460.041 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41480 0 0 0 45908 100 0 0 25 0 1 0 489733258 187174912 39934 4294967295 134512640 134672761 3221224544 3221223712 134564502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45697 39934 603 41 0 45656 0
vsize: 182788
[startup+470.042 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41485 0 0 0 46908 100 0 0 25 0 1 0 489733258 187174912 39939 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45697 39939 603 41 0 45656 0
vsize: 182788
[startup+480.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41490 0 0 0 47909 100 0 0 25 0 1 0 489733258 187174912 39944 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45697 39944 603 41 0 45656 0
vsize: 182788
[startup+490.042 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41496 0 0 0 48909 100 0 0 25 0 1 0 489733258 187310080 39950 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45730 39950 603 41 0 45689 0
vsize: 182920
[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41502 0 0 0 49909 100 0 0 25 0 1 0 489733258 187310080 39956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45730 39956 603 41 0 45689 0
vsize: 182920
[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41508 0 0 0 50909 100 0 0 25 0 1 0 489733258 187310080 39962 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45730 39962 603 41 0 45689 0
vsize: 182920
[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41528 0 0 0 51910 100 0 0 25 0 1 0 489733258 187310080 39982 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45730 39982 603 41 0 45689 0
vsize: 182920
[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41539 0 0 0 52910 100 0 0 25 0 1 0 489733258 187310080 39993 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45730 39993 603 41 0 45689 0
vsize: 182920
[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41550 0 0 0 53910 100 0 0 25 0 1 0 489733258 187445248 40004 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45763 40004 603 41 0 45722 0
vsize: 183052
[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41553 0 0 0 54910 100 0 0 25 0 1 0 489733258 187445248 40007 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45763 40007 603 41 0 45722 0
vsize: 183052
[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41556 0 0 0 55911 100 0 0 25 0 1 0 489733258 187445248 40010 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45763 40010 603 41 0 45722 0
vsize: 183052
[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41559 0 0 0 56911 100 0 0 25 0 1 0 489733258 187445248 40013 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45763 40013 603 41 0 45722 0
vsize: 183052
[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41562 0 0 0 57911 101 0 0 25 0 1 0 489733258 187445248 40016 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45763 40016 603 41 0 45722 0
vsize: 183052
[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41582 0 0 0 58910 101 0 0 25 0 1 0 489733258 187445248 40036 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45763 40036 603 41 0 45722 0
vsize: 183052
[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41596 0 0 0 59910 101 0 0 25 0 1 0 489733258 187580416 40050 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45796 40050 603 41 0 45755 0
vsize: 183184
[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41600 0 0 0 60911 101 0 0 25 0 1 0 489733258 187580416 40054 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45796 40054 603 41 0 45755 0
vsize: 183184
[startup+620.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41604 0 0 0 61911 101 0 0 25 0 1 0 489733258 187580416 40058 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45796 40058 603 41 0 45755 0
vsize: 183184
[startup+630.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41607 0 0 0 62911 101 0 0 25 0 1 0 489733258 187580416 40061 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45796 40061 603 41 0 45755 0
vsize: 183184
[startup+640.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41610 0 0 0 63911 101 0 0 25 0 1 0 489733258 187580416 40064 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45796 40064 603 41 0 45755 0
vsize: 183184
[startup+650.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41617 0 0 0 64911 101 0 0 25 0 1 0 489733258 187580416 40071 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45796 40071 603 41 0 45755 0
vsize: 183184
[startup+660.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41627 0 0 0 65911 101 0 0 25 0 1 0 489733258 187715584 40081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45829 40081 603 41 0 45788 0
vsize: 183316
[startup+670.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41632 0 0 0 66912 101 0 0 25 0 1 0 489733258 187715584 40086 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45829 40086 603 41 0 45788 0
vsize: 183316
[startup+680.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41639 0 0 0 67912 101 0 0 25 0 1 0 489733258 187715584 40093 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45829 40093 603 41 0 45788 0
vsize: 183316
[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41645 0 0 0 68912 101 0 0 25 0 1 0 489733258 187715584 40099 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45829 40099 603 41 0 45788 0
vsize: 183316
[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41656 0 0 0 69912 101 0 0 25 0 1 0 489733258 187715584 40110 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45829 40110 603 41 0 45788 0
vsize: 183316
[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41674 0 0 0 70912 101 0 0 25 0 1 0 489733258 187850752 40128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45862 40128 603 41 0 45821 0
vsize: 183448
[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41678 0 0 0 71912 101 0 0 25 0 1 0 489733258 187850752 40132 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45862 40132 603 41 0 45821 0
vsize: 183448
[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41688 0 0 0 72913 101 0 0 25 0 1 0 489733258 187850752 40142 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45862 40142 603 41 0 45821 0
vsize: 183448
[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41703 0 0 0 73913 101 0 0 25 0 1 0 489733258 187850752 40157 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45862 40157 603 41 0 45821 0
vsize: 183448
[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41710 0 0 0 74913 101 0 0 25 0 1 0 489733258 187985920 40164 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40164 603 41 0 45854 0
vsize: 183580
[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41719 0 0 0 75913 101 0 0 25 0 1 0 489733258 187985920 40173 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40173 603 41 0 45854 0
vsize: 183580
[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41728 0 0 0 76913 101 0 0 25 0 1 0 489733258 187985920 40182 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40182 603 41 0 45854 0
vsize: 183580
[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41734 0 0 0 77914 101 0 0 25 0 1 0 489733258 187985920 40188 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40188 603 41 0 45854 0
vsize: 183580
[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41738 0 0 0 78915 101 0 0 25 0 1 0 489733258 187985920 40192 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40192 603 41 0 45854 0
vsize: 183580
[startup+800.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41743 0 0 0 79915 101 0 0 25 0 1 0 489733258 187985920 40197 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40197 603 41 0 45854 0
vsize: 183580
[startup+810.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41747 0 0 0 80915 101 0 0 25 0 1 0 489733258 187985920 40201 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40201 603 41 0 45854 0
vsize: 183580
[startup+820.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41750 0 0 0 81916 101 0 0 25 0 1 0 489733258 187985920 40204 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45895 40204 603 41 0 45854 0
vsize: 183580
[startup+830.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41753 0 0 0 82917 102 0 0 25 0 1 0 489733258 188121088 40207 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40207 603 41 0 45887 0
vsize: 183712
[startup+840.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41756 0 0 0 83917 102 0 0 25 0 1 0 489733258 188121088 40210 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40210 603 41 0 45887 0
vsize: 183712
[startup+850.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41758 0 0 0 84918 102 0 0 25 0 1 0 489733258 188121088 40212 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40212 603 41 0 45887 0
vsize: 183712
[startup+860.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41760 0 0 0 85918 102 0 0 25 0 1 0 489733258 188121088 40214 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40214 603 41 0 45887 0
vsize: 183712
[startup+870.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41763 0 0 0 86918 102 0 0 25 0 1 0 489733258 188121088 40217 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40217 603 41 0 45887 0
vsize: 183712
[startup+880.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41764 0 0 0 87918 102 0 0 25 0 1 0 489733258 188121088 40218 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40218 603 41 0 45887 0
vsize: 183712
[startup+890.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41766 0 0 0 88918 102 0 0 25 0 1 0 489733258 188121088 40220 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40220 603 41 0 45887 0
vsize: 183712
[startup+900.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41767 0 0 0 89919 102 0 0 25 0 1 0 489733258 188121088 40221 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45928 40221 603 41 0 45887 0
vsize: 183712
[startup+910.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41770 0 0 0 90919 102 0 0 25 0 1 0 489733258 188121088 40224 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45928 40224 603 41 0 45887 0
vsize: 183712
[startup+920.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41794 0 0 0 91918 102 0 0 25 0 1 0 489733258 188338176 40248 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40248 603 41 0 45940 0
vsize: 183924
[startup+930.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41799 0 0 0 92918 102 0 0 25 0 1 0 489733258 188338176 40253 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40253 603 41 0 45940 0
vsize: 183924
[startup+940.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41799 0 0 0 93918 102 0 0 25 0 1 0 489733258 188338176 40253 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41799 0 0 0 94917 102 0 0 25 0 1 0 489733258 188338176 40253 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40253 603 41 0 45940 0
vsize: 183924
[startup+960.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41799 0 0 0 95918 102 0 0 25 0 1 0 489733258 188338176 40253 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40253 603 41 0 45940 0
vsize: 183924
[startup+970.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41800 0 0 0 96918 102 0 0 25 0 1 0 489733258 188338176 40254 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40254 603 41 0 45940 0
vsize: 183924
[startup+980.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41802 0 0 0 97918 102 0 0 25 0 1 0 489733258 188338176 40256 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40256 603 41 0 45940 0
vsize: 183924
[startup+990.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41805 0 0 0 98918 102 0 0 25 0 1 0 489733258 188338176 40259 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40259 603 41 0 45940 0
vsize: 183924
[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41815 0 0 0 99918 102 0 0 25 0 1 0 489733258 188338176 40269 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40269 603 41 0 45940 0
vsize: 183924
[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41817 0 0 0 100919 102 0 0 25 0 1 0 489733258 188338176 40271 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40271 603 41 0 45940 0
vsize: 183924
[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41824 0 0 0 101919 102 0 0 25 0 1 0 489733258 188338176 40278 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40278 603 41 0 45940 0
vsize: 183924
[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41826 0 0 0 102919 102 0 0 25 0 1 0 489733258 188338176 40280 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40280 603 41 0 45940 0
vsize: 183924
[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41828 0 0 0 103919 102 0 0 25 0 1 0 489733258 188338176 40282 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40282 603 41 0 45940 0
vsize: 183924
[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41831 0 0 0 104919 102 0 0 25 0 1 0 489733258 188338176 40285 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40285 603 41 0 45940 0
vsize: 183924
[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41834 0 0 0 105920 102 0 0 25 0 1 0 489733258 188338176 40288 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40288 603 41 0 45940 0
vsize: 183924
[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41839 0 0 0 106920 103 0 0 25 0 1 0 489733258 188338176 40293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40293 603 41 0 45940 0
vsize: 183924
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41841 0 0 0 107920 103 0 0 25 0 1 0 489733258 188338176 40295 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45981 40295 603 41 0 45940 0
vsize: 183924
[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41846 0 0 0 108920 103 0 0 25 0 1 0 489733258 188473344 40300 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46014 40300 603 41 0 45973 0
vsize: 184056
[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41894 0 0 0 109920 103 0 0 25 0 1 0 489733258 188608512 40348 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40348 603 41 0 46006 0
vsize: 184188
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41901 0 0 0 110920 103 0 0 25 0 1 0 489733258 188608512 40355 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40355 603 41 0 46006 0
vsize: 184188
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41903 0 0 0 111921 103 0 0 25 0 1 0 489733258 188608512 40357 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40357 603 41 0 46006 0
vsize: 184188
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41904 0 0 0 112921 103 0 0 25 0 1 0 489733258 188608512 40358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40358 603 41 0 46006 0
vsize: 184188
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41907 0 0 0 113921 103 0 0 25 0 1 0 489733258 188608512 40361 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40361 603 41 0 46006 0
vsize: 184188
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41908 0 0 0 114921 103 0 0 25 0 1 0 489733258 188608512 40362 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40362 603 41 0 46006 0
vsize: 184188
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41909 0 0 0 115921 103 0 0 25 0 1 0 489733258 188608512 40363 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40363 603 41 0 46006 0
vsize: 184188
[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41910 0 0 0 116922 103 0 0 25 0 1 0 489733258 188608512 40364 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40364 603 41 0 46006 0
vsize: 184188
[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41912 0 0 0 117923 103 0 0 25 0 1 0 489733258 188608512 40366 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 40366 603 41 0 46006 0
vsize: 184188
[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41915 0 0 0 118923 103 0 0 25 0 1 0 489733258 188743680 40369 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46080 40369 603 41 0 46039 0
vsize: 184320
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4944
Raw data (stat): 4944 (minisat+) R 4943 25285 25284 0 -1 0 41916 0 0 0 119924 103 0 0 25 0 1 0 489733258 188743680 40370 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46080 40370 603 41 0 46039 0
vsize: 184320
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4944
Raw data (stat): 4944 (minisat+) Z 4943 25285 25284 0 -1 12 41918 0 0 0 119924 111 0 0 25 0 1 0 489733258 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.2
CPU time (s): 1200.36
CPU user time (s): 1199.24
CPU system time (s): 1.11383
CPU usage (%): 100.013
Max. virtual memory (Kb): 184320
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####