PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        308072 kB
Buffers:         35816 kB
Cached:         667372 kB
SwapCached:          0 kB
Active:         377056 kB
Inactive:       328936 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        307820 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14940 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:40:32 (client local time) WITH STATUS 0 IN 1200.64 SECONDS
stats: 20265 7 1200.64 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]---> BDD-cost:   19
c ---[1815]---> BDD-cost:    5
c ---[1814]---> BDD-cost:    3
c ---[1813]---> BDD-cost:    7
c ---[1812]---> BDD-cost:    5
c ---[1811]---> BDD-cost:   47
c ---[1810]---> BDD-cost:   45
c ---[1809]---> BDD-cost:   17
c ---[1808]---> BDD-cost:   17
c ---[1807]---> BDD-cost:   17
c ---[1805]---> BDD-cost:    3
c ---[1804]---> BDD-cost:   17
c ---[1803]---> BDD-cost:   47
c ---[1802]---> BDD-cost:   45
c ---[1801]---> BDD-cost:   45
c ---[1800]---> BDD-cost:   17
c ---[1799]---> BDD-cost:   17
c ---[1798]---> BDD-cost:   17
c ---[1797]---> BDD-cost:   17
c ---[1796]---> BDD-cost:   17
c ---[1794]---> BDD-cost:   17
c ---[1793]---> BDD-cost:   17
c ---[1792]---> BDD-cost:   45
c ---[1791]---> BDD-cost:   45
c ---[1790]---> BDD-cost:    3
c ---[1789]---> BDD-cost:   19
c ---[1788]---> BDD-cost:   19
c ---[1787]---> BDD-cost:   59
c ---[1786]---> BDD-cost:   59
c ---[1785]---> BDD-cost:   19
c ---[1783]---> BDD-cost:    7
c ---[1782]---> BDD-cost:   59
c ---[1781]---> BDD-cost:   59
c ---[1780]---> BDD-cost:   59
c ---[1779]---> BDD-cost:   59
c ---[1778]---> BDD-cost:   59
c ---[1777]---> BDD-cost:   59
c ---[1776]---> BDD-cost:    9
c ---[1775]---> BDD-cost:    9
c ---[1774]---> BDD-cost:    3
c ---[1772]---> BDD-cost:    3
c ---[1770]---> BDD-cost:    3
c ---[1769]---> BDD-cost:   19
c ---[1768]---> BDD-cost:   19
c ---[1767]---> BDD-cost:   11
c ---[1766]---> BDD-cost:   11
c ---[1765]---> BDD-cost:   19
c ---[1763]---> BDD-cost:   19
c ---[1762]---> BDD-cost:   11
c ---[1761]---> BDD-cost:    5
c ---[1760]---> BDD-cost:   11
c ---[1759]---> BDD-cost:   19
c ---[1758]---> BDD-cost:    5
c ---[1757]---> BDD-cost:   11
c ---[1756]---> BDD-cost:    5
c ---[1755]---> BDD-cost:   23
c ---[1754]---> BDD-cost:   17
c ---[1752]---> BDD-cost:   39
c ---[1751]---> BDD-cost:   53
c ---[1750]---> BDD-cost:   53
c ---[1749]---> BDD-cost:   59
c ---[1748]---> BDD-cost:   47
c ---[1747]---> BDD-cost:   41
c ---[1746]---> BDD-cost:   47
c ---[1745]---> BDD-cost:   39
c ---[1744]---> BDD-cost:   53
c ---[1743]---> BDD-cost:   25
c ---[1741]---> BDD-cost:   39
c ---[1740]---> BDD-cost:   43
c ---[1739]---> BDD-cost:   41
c ---[1738]---> BDD-cost:   47
c ---[1737]---> BDD-cost:   29
c ---[1736]---> BDD-cost:   39
c ---[1735]---> BDD-cost:   53
c ---[1734]---> BDD-cost:   53
c ---[1733]---> BDD-cost:   59
c ---[1732]---> BDD-cost:   39
c ---[1731]---> Adder-cost: 928   maxlim: 9   bits: 5/4
c ---[1730]---> BDD-cost:   37
c ---[1729]---> BDD-cost:   39
c ---[1728]---> BDD-cost:   43
c ---[1727]---> BDD-cost:   53
c ---[1726]---> BDD-cost:   29
c ---[1725]---> BDD-cost:   21
c ---[1724]---> BDD-cost:   43
c ---[1723]---> BDD-cost:   41
c ---[1722]---> BDD-cost:   49
c ---[1721]---> BDD-cost:   43
c ---[1720]---> Adder-cost: 1283   maxlim: 26   bits: 6/5
c ---[1719]---> BDD-cost:   47
c ---[1718]---> BDD-cost:   53
c ---[1717]---> BDD-cost:   53
c ---[1716]---> BDD-cost:   59
c ---[1715]---> BDD-cost:   59
c ---[1712]---> BDD-cost:    7
c ---[1711]---> BDD-cost:    7
c ---[1710]---> BDD-cost:   29
c ---[1707]---> BDD-cost:   47
c ---[1706]---> BDD-cost:   39
c ---[1704]---> BDD-cost:    7
c ---[1703]---> BDD-cost:   47
c ---[1702]---> BDD-cost:   19
c ---[1699]---> BDD-cost:   13
c ---[1698]---> BDD-cost:   13
c ---[1693]---> BDD-cost:    3
c ---[1692]---> BDD-cost:    3
c ---[1691]---> BDD-cost:   11
c ---[1689]---> BDD-cost:    9
c ---[1688]---> BDD-cost:   11
c ---[1685]---> BDD-cost:    9
c ---[1684]---> BDD-cost:    9
c ---[1681]---> BDD-cost:    9
c ---[1679]---> BDD-cost:    9
c ---[1678]---> BDD-cost:    9
c ---[1677]---> BDD-cost:   53
c ---[1676]---> BDD-cost:   53
c ---[1674]---> BDD-cost:   43
c ---[1671]---> BDD-cost:    7
c ---[1670]---> BDD-cost:    7
c ---[1669]---> BDD-cost:   27
c ---[1668]---> BDD-cost:   39
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:   19
c ---[1665]---> BDD-cost:   53
c ---[1663]---> BDD-cost:   53
c ---[1662]---> BDD-cost:   43
c ---[1661]---> BDD-cost:   53
c ---[1658]---> BDD-cost:    7
c ---[1657]---> BDD-cost:    7
c ---[1656]---> BDD-cost:   29
c ---[1655]---> BDD-cost:   41
c ---[1654]---> BDD-cost:   19
c ---[1652]---> BDD-cost:   27
c ---[1651]---> BDD-cost:   51
c ---[1650]---> BDD-cost:   49
c ---[1649]---> BDD-cost:   35
c ---[1648]---> BDD-cost:   53
c ---[1647]---> BDD-cost:   53
c ---[1646]---> BDD-cost:   49
c ---[1645]---> BDD-cost:   37
c ---[1644]---> BDD-cost:   53
c ---[1643]---> BDD-cost:   51
c ---[1641]---> BDD-cost:   49
c ---[1640]---> BDD-cost:   49
c ---[1639]---> BDD-cost:   37
c ---[1638]---> BDD-cost:   37
c ---[1637]---> BDD-cost:   49
c ---[1636]---> BDD-cost:   49
c ---[1635]---> BDD-cost:   49
c ---[1634]---> BDD-cost:   53
c ---[1633]---> BDD-cost:   53
c ---[1632]---> BDD-cost:   35
c ---[1630]---> BDD-cost:   53
c ---[1629]---> BDD-cost:   37
c ---[1628]---> BDD-cost:   49
c ---[1627]---> BDD-cost:   49
c ---[1626]---> BDD-cost:   49
c ---[1625]---> BDD-cost:   49
c ---[1624]---> BDD-cost:   37
c ---[1623]---> BDD-cost:   33
c ---[1622]---> BDD-cost:   49
c ---[1621]---> BDD-cost:   53
c ---[1619]---> BDD-cost:   53
c ---[1618]---> BDD-cost:   29
c ---[1617]---> BDD-cost:    5
c ---[1616]---> BDD-cost:   35
c ---[1615]---> BDD-cost:   53
c ---[1614]---> BDD-cost:   43
c ---[1613]---> BDD-cost:   53
c ---[1612]---> BDD-cost:   53
c ---[1611]---> BDD-cost:   53
c ---[1610]---> BDD-cost:   53
c ---[1608]---> BDD-cost:   17
c ---[1607]---> BDD-cost:   19
c ---[1606]---> BDD-cost:   19
c ---[1605]---> BDD-cost:   11
c ---[1604]---> BDD-cost:   11
c ---[1603]---> BDD-cost:   19
c ---[1602]---> BDD-cost:   19
c ---[1601]---> BDD-cost:   11
c ---[1599]---> BDD-cost:   11
c ---[1596]---> BDD-cost:   19
c ---[1594]---> BDD-cost:   11
c ---[1592]---> BDD-cost:    3
c ---[1591]---> BDD-cost:    3
c ---[1590]---> BDD-cost:   43
c ---[1589]---> BDD-cost:    9
c ---[1588]---> BDD-cost:   41
c ---[1587]---> BDD-cost:   53
c ---[1584]---> BDD-cost:   43
c ---[1583]---> BDD-cost:   35
c ---[1582]---> BDD-cost:   43
c ---[1581]---> BDD-cost:   53
c ---[1580]---> BDD-cost:   43
c ---[1579]---> BDD-cost:   47
c ---[1578]---> BDD-cost:   41
c ---[1577]---> BDD-cost:    5
c ---[1576]---> BDD-cost:   39
c ---[1574]---> BDD-cost:   53
c ---[1573]---> BDD-cost:   43
c ---[1572]---> BDD-cost:   35
c ---[1571]---> BDD-cost:   41
c ---[1569]---> BDD-cost:   13
c ---[1567]---> BDD-cost:   13
c ---[1566]---> BDD-cost:   53
c ---[1565]---> BDD-cost:   53
c ---[1563]---> BDD-cost:   53
c ---[1562]---> BDD-cost:   53
c ---[1561]---> BDD-cost:   53
c ---[1560]---> BDD-cost:   53
c ---[1559]---> BDD-cost:   53
c ---[1558]---> BDD-cost:   53
c ---[1557]---> BDD-cost:   53
c ---[1556]---> BDD-cost:   53
c ---[1555]---> BDD-cost:   53
c ---[1554]---> BDD-cost:   53
c ---[1552]---> BDD-cost:    5
c ---[1551]---> BDD-cost:   53
c ---[1550]---> BDD-cost:   53
c ---[1549]---> BDD-cost:   53
c ---[1548]---> BDD-cost:    3
c ---[1547]---> BDD-cost:   17
c ---[1546]---> BDD-cost:   17
c ---[1545]---> BDD-cost:   17
c ---[1544]---> BDD-cost:   45
c ---[1543]---> BDD-cost:   59
c ---[1541]---> BDD-cost:   59
c ---[1540]---> BDD-cost:   59
c ---[1539]---> BDD-cost:   59
c ---[1538]---> BDD-cost:   59
c ---[1537]---> BDD-cost:   59
c ---[1536]---> BDD-cost:   59
c ---[1535]---> BDD-cost:   59
c ---[1534]---> BDD-cost:   59
c ---[1533]---> BDD-cost:   59
c ---[1532]---> BDD-cost:   59
c ---[1530]---> BDD-cost:   59
c ---[1529]---> BDD-cost:   59
c ---[1527]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    3
c ---[1524]---> BDD-cost:    5
c ---[1519]---> BDD-cost:   47
c ---[1518]---> BDD-cost:   39
c ---[1517]---> BDD-cost:   41
c ---[1516]---> BDD-cost:   43
c ---[1515]---> BDD-cost:   47
c ---[1514]---> BDD-cost:    5
c ---[1513]---> BDD-cost:    7
c ---[1512]---> BDD-cost:   47
c ---[1511]---> BDD-cost:    9
c ---[1509]---> BDD-cost:    7
c ---[1508]---> BDD-cost:   29
c ---[1507]---> BDD-cost:   47
c ---[1504]---> BDD-cost:   37
c ---[1503]---> BDD-cost:   59
c ---[1502]---> BDD-cost:   43
c ---[1501]---> BDD-cost:   47
c ---[1500]---> BDD-cost:    7
c ---[1498]---> BDD-cost:   39
c ---[1497]---> BDD-cost:   17
c ---[1496]---> BDD-cost:   19
c ---[1495]---> BDD-cost:   19
c ---[1494]---> BDD-cost:   49
c ---[1493]---> BDD-cost:   19
c ---[1492]---> BDD-cost:   19
c ---[1491]---> BDD-cost:   53
c ---[1490]---> BDD-cost:   47
c ---[1489]---> BDD-cost:   41
c ---[1486]---> BDD-cost:   39
c ---[1485]---> BDD-cost:   43
c ---[1484]---> BDD-cost:   43
c ---[1483]---> BDD-cost:   11
c ---[1482]---> BDD-cost:   43
c ---[1481]---> BDD-cost:    3
c ---[1480]---> BDD-cost:   11
c ---[1479]---> BDD-cost:    5
c ---[1478]---> BDD-cost:    3
c ---[1477]---> BDD-cost:    7
c ---[1475]---> BDD-cost:   35
c ---[1474]---> BDD-cost:   37
c ---[1473]---> BDD-cost:   39
c ---[1472]---> BDD-cost:   53
c ---[1471]---> BDD-cost:   51
c ---[1470]---> BDD-cost:   25
c ---[1469]---> BDD-cost:   35
c ---[1468]---> BDD-cost:   59
c ---[1467]---> BDD-cost:   53
c ---[1466]---> BDD-cost:    9
c ---[1464]---> BDD-cost:   11
c ---[1462]---> BDD-cost:    9
c ---[1458]---> BDD-cost:    9
c ---[1457]---> BDD-cost:   33
c ---[1456]---> BDD-cost:   39
c ---[1455]---> BDD-cost:   37
c ---[1453]---> BDD-cost:   43
c ---[1451]---> BDD-cost:   43
c ---[1450]---> BDD-cost:   39
c ---[1449]---> BDD-cost:   41
c ---[1448]---> BDD-cost:    5
c ---[1447]---> BDD-cost:    3
c ---[1445]---> BDD-cost:    5
c ---[1444]---> BDD-cost:    7
c ---[1442]---> BDD-cost:   31
c ---[1441]---> BDD-cost:   19
c ---[1440]---> BDD-cost:    7
c ---[1438]---> BDD-cost:   41
c ---[1436]---> BDD-cost:    7
c ---[1433]---> BDD-cost:   33
c ---[1431]---> BDD-cost:   39
c ---[1429]---> BDD-cost:   37
c ---[1428]---> BDD-cost:   39
c ---[1427]---> BDD-cost:   17
c ---[1426]---> BDD-cost:   19
c ---[1425]---> BDD-cost:   19
c ---[1424]---> BDD-cost:   19
c ---[1423]---> BDD-cost:   19
c ---[1422]---> BDD-cost:   33
c ---[1420]---> BDD-cost:   39
c ---[1418]---> BDD-cost:   19
c ---[1417]---> BDD-cost:   19
c ---[1416]---> BDD-cost:   19
c ---[1415]---> BDD-cost:   43
c ---[1414]---> BDD-cost:   43
c ---[1413]---> BDD-cost:    3
c ---[1412]---> BDD-cost:   11
c ---[1411]---> BDD-cost:   35
c ---[1408]---> BDD-cost:   11
c ---[1406]---> BDD-cost:   43
c ---[1404]---> BDD-cost:   11
c ---[1403]---> BDD-cost:   41
c ---[1402]---> BDD-cost:   33
c ---[1401]---> BDD-cost:   19
c ---[1399]---> BDD-cost:   27
c ---[1398]---> BDD-cost:    5
c ---[1397]---> BDD-cost:   53
c ---[1396]---> BDD-cost:    7
c ---[1395]---> BDD-cost:   43
c ---[1394]---> BDD-cost:   39
c ---[1393]---> BDD-cost:   43
c ---[1392]---> BDD-cost:    3
c ---[1391]---> BDD-cost:   43
c ---[1390]---> BDD-cost:   25
c ---[1388]---> BDD-cost:   53
c ---[1387]---> BDD-cost:   29
c ---[1386]---> BDD-cost:   47
c ---[1385]---> BDD-cost:   41
c ---[1384]---> BDD-cost:   59
c ---[1383]---> BDD-cost:   33
c ---[1382]---> BDD-cost:   31
c ---[1381]---> BDD-cost:   41
c ---[1380]---> BDD-cost:   53
c ---[1379]---> BDD-cost:   49
c ---[1376]---> BDD-cost:   39
c ---[1375]---> BDD-cost:   43
c ---[1374]---> BDD-cost:    5
c ---[1373]---> BDD-cost:   13
c ---[1371]---> BDD-cost:   39
c ---[1369]---> BDD-cost:   19
c ---[1368]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   47
c ---[1365]---> BDD-cost:   19
c ---[1364]---> BDD-cost:   59
c ---[1363]---> BDD-cost:   59
c ---[1362]---> BDD-cost:   41
c ---[1361]---> BDD-cost:   19
c ---[1360]---> BDD-cost:   45
c ---[1359]---> BDD-cost:   43
c ---[1358]---> BDD-cost:   37
c ---[1357]---> BDD-cost:   43
c ---[1356]---> BDD-cost:   49
c ---[1355]---> Adder-cost: 515   maxlim: 9   bits: 5/4
c ---[1354]---> BDD-cost:   37
c ---[1353]---> BDD-cost:   43
c ---[1352]---> BDD-cost:   53
c ---[1351]---> BDD-cost:   53
c ---[1350]---> BDD-cost:    5
c ---[1348]---> BDD-cost:   19
c ---[1347]---> BDD-cost:   19
c ---[1346]---> BDD-cost:   43
c ---[1345]---> BDD-cost:   41
c ---[1344]---> Adder-cost: 761   maxlim: 19   bits: 6/5
c ---[1343]---> BDD-cost:   19
c ---[1342]---> BDD-cost:   13
c ---[1341]---> BDD-cost:   19
c ---[1339]---> BDD-cost:    3
c ---[1338]---> BDD-cost:   11
c ---[1333]---> BDD-cost:  771
c ---[1302]---> Adder-cost: 3666   maxlim: 9   bits: 5/4
c ---[1301]---> Adder-cost: 5783   maxlim: 27   bits: 6/5
c ---[1300]---> Adder-cost: 2769   maxlim: 7   bits: 4/3
c ---[1296]---> Adder-cost: 5328   maxlim: 9   bits: 5/4
c ---[1275]---> BDD-cost:18365
c ---[1253]---> Adder-cost: 7051   maxlim: 7   bits: 4/3
c ---[1242]---> Adder-cost: 10495   maxlim: 29   bits: 6/5
c ---[1214]---> Adder-cost: 3777   maxlim: 17   bits: 6/5
c ---[1189]---> BDD-cost:   27
c ---[1184]---> BDD-cost:   27
c ---[1176]---> BDD-cost: 8536
c ---[1164]---> Adder-cost: 5657   maxlim: 29   bits: 6/5
c ---[1054]---> BDD-cost: 6713
c ---[1043]---> BDD-cost:  823
c ---[ 916]---> BDD-cost:   37
c ---[ 915]---> BDD-cost:   27
c ---[ 914]---> BDD-cost:   43
c ---[ 913]---> BDD-cost:   47
c ---[ 912]---> BDD-cost:   43
c ---[ 911]---> BDD-cost:   49
c ---[ 910]---> BDD-cost:   39
c ---[ 908]---> BDD-cost:   49
c ---[ 907]---> BDD-cost:   59
c ---[ 906]---> BDD-cost:   47
c ---[ 905]---> BDD-cost:   37
c ---[ 904]---> BDD-cost:   47
c ---[ 903]---> BDD-cost:   43
c ---[ 902]---> BDD-cost:   31
c ---[ 901]---> BDD-cost:   29
c ---[ 900]---> BDD-cost:   23
c ---[ 899]---> BDD-cost:    5
c ---[ 897]---> BDD-cost:   25
c ---[ 896]---> BDD-cost:   19
c ---[ 895]---> BDD-cost:   19
c ---[ 894]---> BDD-cost:   37
c ---[ 893]---> BDD-cost:   43
c ---[ 892]---> BDD-cost:    3
c ---[ 891]---> BDD-cost:    5
c ---[ 890]---> BDD-cost:    3
c ---[ 889]---> BDD-cost:   15
c ---[ 888]---> BDD-cost:   15
c ---[ 886]---> BDD-cost:    3
c ---[ 885]---> BDD-cost:    9
c ---[ 884]---> BDD-cost:   21
c ---[ 883]---> BDD-cost:   17
c ---[ 882]---> BDD-cost:   17
c ---[ 881]---> BDD-cost:   19
c ---[ 880]---> BDD-cost:   19
c ---[ 879]---> BDD-cost:    3
c ---[ 878]---> BDD-cost:   17
c ---[ 877]---> BDD-cost:   17
c ---[ 875]---> BDD-cost:   19
c ---[ 874]---> BDD-cost:   41
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:    3
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    3
c ---[ 869]---> BDD-cost:   49
c ---[ 868]---> BDD-cost:   49
c ---[ 867]---> BDD-cost:   19
c ---[ 866]---> BDD-cost:   53
c ---[ 865]---> BDD-cost:12879
c ---[ 864]---> BDD-cost:   17
c ---[ 863]---> BDD-cost:   17
c ---[ 862]---> BDD-cost:    9
c ---[ 861]---> BDD-cost:    3
c ---[ 860]---> BDD-cost:   27
c ---[ 859]---> BDD-cost:   37
c ---[ 858]---> BDD-cost:   33
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:    3
c ---[ 855]---> BDD-cost:   25
c ---[ 853]---> BDD-cost:   19
c ---[ 852]---> BDD-cost:    5
c ---[ 851]---> BDD-cost:    3
c ---[ 850]---> BDD-cost:   41
c ---[ 849]---> BDD-cost:    3
c ---[ 848]---> BDD-cost:    3
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:   33
c ---[ 845]---> BDD-cost:   41
c ---[ 844]---> BDD-cost:    3
c ---[ 842]---> BDD-cost:   37
c ---[ 841]---> BDD-cost:   17
c ---[ 840]---> BDD-cost:   19
c ---[ 839]---> BDD-cost:   19
c ---[ 838]---> BDD-cost:   25
c ---[ 837]---> BDD-cost:   19
c ---[ 836]---> BDD-cost:   33
c ---[ 835]---> BDD-cost:   19
c ---[ 834]---> BDD-cost:   19
c ---[ 833]---> BDD-cost:   43
c ---[ 830]---> BDD-cost:   19
c ---[ 829]---> BDD-cost:   19
c ---[ 828]---> BDD-cost:   19
c ---[ 827]---> BDD-cost:    5
c ---[ 826]---> BDD-cost:   49
c ---[ 825]---> BDD-cost:    5
c ---[ 824]---> BDD-cost:   53
c ---[ 823]---> BDD-cost:   19
c ---[ 822]---> BDD-cost:   19
c ---[ 821]---> BDD-cost:   19
c ---[ 819]---> BDD-cost:   41
c ---[ 818]---> BDD-cost:   37
c ---[ 817]---> BDD-cost:   43
c ---[ 816]---> BDD-cost:   19
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:    5
c ---[ 813]---> BDD-cost:   35
c ---[ 812]---> BDD-cost:    3
c ---[ 811]---> BDD-cost:   59
c ---[ 810]---> BDD-cost:   41
c ---[ 808]---> BDD-cost:   59
c ---[ 807]---> BDD-cost:   53
c ---[ 806]---> BDD-cost:   59
c ---[ 805]---> BDD-cost:   35
c ---[ 804]---> BDD-cost:   37
c ---[ 803]---> BDD-cost:   35
c ---[ 802]---> BDD-cost:   51
c ---[ 801]---> BDD-cost:   59
c ---[ 800]---> BDD-cost:   59
c ---[ 799]---> BDD-cost:   35
c ---[ 797]---> BDD-cost:   11
c ---[ 796]---> BDD-cost:   53
c ---[ 795]---> BDD-cost:   35
c ---[ 794]---> BDD-cost:   59
c ---[ 793]---> BDD-cost:   53
c ---[ 792]---> BDD-cost:   53
c ---[ 791]---> BDD-cost:   35
c ---[ 790]---> BDD-cost:   59
c ---[ 789]---> BDD-cost:   19
c ---[ 788]---> BDD-cost:   43
c ---[ 786]---> BDD-cost:   43
c ---[ 785]---> BDD-cost:   23
c ---[ 784]---> BDD-cost:    7
c ---[ 782]---> BDD-cost:   47
c ---[ 781]---> BDD-cost:   59
c ---[ 780]---> BDD-cost:    7
c ---[ 779]---> BDD-cost:   45
c ---[ 778]---> BDD-cost:   47
c ---[ 777]---> BDD-cost:   17
c ---[ 775]---> BDD-cost:   47
c ---[ 774]---> BDD-cost:   19
c ---[ 772]---> BDD-cost:   47
c ---[ 771]---> BDD-cost:   43
c ---[ 770]---> BDD-cost:   43
c ---[ 769]---> BDD-cost:   45
c ---[ 768]---> BDD-cost:   47
c ---[ 767]---> BDD-cost:   45
c ---[ 766]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   49
c ---[ 763]---> BDD-cost:   49
c ---[ 762]---> BDD-cost:   43
c ---[ 761]---> BDD-cost:   35
c ---[ 760]---> BDD-cost:   23
c ---[ 759]---> BDD-cost:   43
c ---[ 758]---> BDD-cost:   43
c ---[ 757]---> BDD-cost:   53
c ---[ 756]---> BDD-cost:   47
c ---[ 755]---> BDD-cost:   59
c ---[ 753]---> BDD-cost:   59
c ---[ 752]---> BDD-cost:   23
c ---[ 751]---> BDD-cost:   47
c ---[ 750]---> BDD-cost:   41
c ---[ 749]---> BDD-cost:   23
c ---[ 748]---> BDD-cost:   43
c ---[ 747]---> BDD-cost:   23
c ---[ 746]---> BDD-cost:   43
c ---[ 745]---> BDD-cost:    7
c ---[ 744]---> BDD-cost:    7
c ---[ 742]---> BDD-cost:   19
c ---[ 741]---> BDD-cost:   23
c ---[ 740]---> BDD-cost:    5
c ---[ 739]---> BDD-cost:   43
c ---[ 738]---> BDD-cost:   49
c ---[ 737]---> BDD-cost:   47
c ---[ 736]---> BDD-cost:   45
c ---[ 735]---> BDD-cost:   43
c ---[ 734]---> BDD-cost:   47
c ---[ 733]---> BDD-cost:   43
c ---[ 731]---> BDD-cost:   59
c ---[ 730]---> BDD-cost:   43
c ---[ 729]---> BDD-cost:   43
c ---[ 728]---> BDD-cost:   47
c ---[ 727]---> BDD-cost:   23
c ---[ 726]---> BDD-cost:   19
c ---[ 725]---> BDD-cost:   49
c ---[ 724]---> BDD-cost:   19
c ---[ 723]---> BDD-cost:   53
c ---[ 722]---> BDD-cost:   43
c ---[ 719]---> BDD-cost:   45
c ---[ 718]---> BDD-cost:   47
c ---[ 717]---> BDD-cost:   47
c ---[ 716]---> BDD-cost:   49
c ---[ 715]---> BDD-cost:   43
c ---[ 714]---> BDD-cost:   29
c ---[ 713]---> BDD-cost:   43
c ---[ 712]---> BDD-cost:   53
c ---[ 711]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:   47
c ---[ 708]---> BDD-cost:   31
c ---[ 707]---> BDD-cost:   43
c ---[ 706]---> BDD-cost:   39
c ---[ 705]---> BDD-cost:   17
c ---[ 704]---> BDD-cost:   35
c ---[ 703]---> BDD-cost:    7
c ---[ 702]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:   19
c ---[ 700]---> BDD-cost:    5
c ---[ 699]---> BDD-cost:   19
c ---[ 697]---> BDD-cost:    7
c ---[ 696]---> BDD-cost:    5
c ---[ 695]---> BDD-cost:    7
c ---[ 694]---> BDD-cost:   57
c ---[ 693]---> BDD-cost:   11
c ---[ 692]---> BDD-cost:   59
c ---[ 691]---> BDD-cost:   59
c ---[ 690]---> BDD-cost:   59
c ---[ 689]---> BDD-cost:   59
c ---[ 688]---> BDD-cost:    5
c ---[ 685]---> BDD-cost:   19
c ---[ 684]---> BDD-cost:   19
c ---[ 683]---> BDD-cost:   37
c ---[ 681]---> BDD-cost:   11
c ---[ 679]---> BDD-cost:   43
c ---[ 678]---> BDD-cost:   39
c ---[ 677]---> BDD-cost:   43
c ---[ 675]---> BDD-cost:   45
c ---[ 674]---> BDD-cost:   59
c ---[ 673]---> BDD-cost:   37
c ---[ 672]---> BDD-cost:   17
c ---[ 671]---> BDD-cost:   39
c ---[ 670]---> BDD-cost:   53
c ---[ 669]---> BDD-cost:   53
c ---[ 668]---> BDD-cost:   59
c ---[ 667]---> BDD-cost:   39
c ---[ 666]---> BDD-cost:   37
c ---[ 664]---> BDD-cost:   39
c ---[ 663]---> BDD-cost:   39
c ---[ 662]---> BDD-cost:   43
c ---[ 661]---> BDD-cost:   25
c ---[ 660]---> BDD-cost:   31
c ---[ 659]---> BDD-cost:   25
c ---[ 658]---> BDD-cost:   43
c ---[ 657]---> BDD-cost:   41
c ---[ 656]---> BDD-cost:   43
c ---[ 655]---> BDD-cost:   43
c ---[ 653]---> BDD-cost:   47
c ---[ 652]---> BDD-cost:   47
c ---[ 651]---> BDD-cost:   57
c ---[ 650]---> BDD-cost:   49
c ---[ 649]---> BDD-cost:   45
c ---[ 648]---> BDD-cost:   43
c ---[ 647]---> BDD-cost:   43
c ---[ 646]---> BDD-cost:   47
c ---[ 645]---> BDD-cost:   59
c ---[ 644]---> BDD-cost:   43
c ---[ 642]---> BDD-cost:   43
c ---[ 641]---> BDD-cost:   47
c ---[ 640]---> BDD-cost:   47
c ---[ 639]---> BDD-cost:   47
c ---[ 638]---> BDD-cost:   47
c ---[ 637]---> BDD-cost:   47
c ---[ 636]---> BDD-cost:   47
c ---[ 635]---> BDD-cost:   43
c ---[ 634]---> BDD-cost:   43
c ---[ 633]---> BDD-cost:   53
c ---[ 631]---> BDD-cost:   59
c ---[ 630]---> BDD-cost:   59
c ---[ 629]---> BDD-cost:   47
c ---[ 628]---> BDD-cost:   47
c ---[ 627]---> BDD-cost:   41
c ---[ 626]---> BDD-cost:   43
c ---[ 625]---> BDD-cost:   41
c ---[ 624]---> BDD-cost:   43
c ---[ 623]---> BDD-cost:   43
c ---[ 622]---> BDD-cost:   47
c ---[ 620]---> BDD-cost:   43
c ---[ 619]---> BDD-cost:   47
c ---[ 618]---> BDD-cost:   43
c ---[ 617]---> BDD-cost:   43
c ---[ 616]---> BDD-cost:   43
c ---[ 615]---> BDD-cost:   49
c ---[ 614]---> BDD-cost:   47
c ---[ 613]---> BDD-cost:   45
c ---[ 612]---> BDD-cost:   47
c ---[ 611]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   43
c ---[ 607]---> BDD-cost:   43
c ---[ 606]---> BDD-cost:   55
c ---[ 605]---> BDD-cost:   43
c ---[ 604]---> BDD-cost:   43
c ---[ 603]---> BDD-cost:   49
c ---[ 602]---> BDD-cost:   43
c ---[ 601]---> BDD-cost:   49
c ---[ 599]---> BDD-cost:   19
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    3
c ---[ 595]---> BDD-cost:    9
c ---[ 594]---> BDD-cost:    5
c ---[ 593]---> BDD-cost:   53
c ---[ 592]---> BDD-cost:   43
c ---[ 591]---> BDD-cost:    7
c ---[ 589]---> BDD-cost:   27
c ---[ 588]---> BDD-cost:   43
c ---[ 586]---> BDD-cost:   39
c ---[ 584]---> BDD-cost:   17
c ---[ 583]---> BDD-cost:   17
c ---[ 582]---> BDD-cost:   19
c ---[ 581]---> BDD-cost:   19
c ---[ 579]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:    5
c ---[ 574]---> BDD-cost:   33
c ---[ 573]---> BDD-cost:   39
c ---[ 571]---> BDD-cost:   19
c ---[ 570]---> BDD-cost:   19
c ---[ 569]---> BDD-cost:   19
c ---[ 568]---> BDD-cost:   45
c ---[ 567]---> BDD-cost:   47
c ---[ 566]---> BDD-cost:   47
c ---[ 564]---> BDD-cost:   19
c ---[ 563]---> BDD-cost:   49
c ---[ 562]---> BDD-cost:   43
c ---[ 561]---> BDD-cost:   19
c ---[ 560]---> BDD-cost:   43
c ---[ 559]---> BDD-cost:   53
c ---[ 558]---> BDD-cost:   59
c ---[ 557]---> BDD-cost:   47
c ---[ 556]---> BDD-cost:    9
c ---[ 555]---> BDD-cost:    7
c ---[ 554]---> BDD-cost:14669
c ---[ 553]---> BDD-cost:   43
c ---[ 552]---> BDD-cost:   43
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:   19
c ---[ 549]---> BDD-cost:   19
c ---[ 548]---> BDD-cost:   25
c ---[ 547]---> BDD-cost:   19
c ---[ 544]---> BDD-cost:   13
c ---[ 543]---> BDD-cost:13317
c ---[ 542]---> BDD-cost:   13
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 537]---> BDD-cost:   19
c ---[ 536]---> BDD-cost:   45
c ---[ 535]---> BDD-cost:   47
c ---[ 534]---> BDD-cost:   47
c ---[ 533]---> BDD-cost:   49
c ---[ 531]---> BDD-cost:   43
c ---[ 530]---> BDD-cost:   43
c ---[ 529]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:   59
c ---[ 527]---> BDD-cost:   47
c ---[ 526]---> BDD-cost:   43
c ---[ 525]---> BDD-cost:   39
c ---[ 524]---> BDD-cost:   11
c ---[ 523]---> BDD-cost:   11
c ---[ 522]---> BDD-cost:   49
c ---[ 520]---> BDD-cost:   53
c ---[ 519]---> BDD-cost:    7
c ---[ 518]---> BDD-cost:    9
c ---[ 517]---> BDD-cost:   11
c ---[ 516]---> BDD-cost:   29
c ---[ 515]---> BDD-cost:   47
c ---[ 514]---> BDD-cost:   39
c ---[ 513]---> BDD-cost:   11
c ---[ 512]---> BDD-cost:   19
c ---[ 511]---> BDD-cost:   19
c ---[ 509]---> BDD-cost:    3
c ---[ 508]---> BDD-cost:   59
c ---[ 507]---> BDD-cost:   59
c ---[ 506]---> BDD-cost:   53
c ---[ 505]---> BDD-cost:   59
c ---[ 504]---> BDD-cost:   53
c ---[ 503]---> BDD-cost:   59
c ---[ 502]---> BDD-cost:   53
c ---[ 501]---> BDD-cost:    7
c ---[ 500]---> BDD-cost:   17
c ---[ 497]---> BDD-cost:   17
c ---[ 496]---> BDD-cost:   19
c ---[ 495]---> BDD-cost:   19
c ---[ 493]---> BDD-cost:    7
c ---[ 492]---> BDD-cost:    5
c ---[ 490]---> BDD-cost:   33
c ---[ 489]---> BDD-cost:   39
c ---[ 486]---> BDD-cost:   19
c ---[ 485]---> BDD-cost:   19
c ---[ 484]---> BDD-cost:   19
c ---[ 483]---> BDD-cost:   45
c ---[ 482]---> BDD-cost:   47
c ---[ 481]---> BDD-cost:   17
c ---[ 480]---> BDD-cost:   43
c ---[ 479]---> BDD-cost:   17
c ---[ 478]---> BDD-cost:   37
c ---[ 477]---> BDD-cost:   43
c ---[ 475]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:   53
c ---[ 471]---> BDD-cost:   53
c ---[ 470]---> BDD-cost:   53
c ---[ 469]---> BDD-cost:   43
c ---[ 468]---> BDD-cost:   43
c ---[ 467]---> BDD-cost:   53
c ---[ 466]---> BDD-cost:   17
c ---[ 464]---> BDD-cost:    7
c ---[ 463]---> BDD-cost:   43
c ---[ 462]---> BDD-cost:   47
c ---[ 461]---> BDD-cost:   53
c ---[ 460]---> BDD-cost:   41
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    7
c ---[ 455]---> BDD-cost:   43
c ---[ 453]---> BDD-cost:    3
c ---[ 452]---> BDD-cost:   21
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:   53
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:   43
c ---[ 447]---> BDD-cost:   39
c ---[ 446]---> BDD-cost:   39
c ---[ 445]---> BDD-cost:    5
c ---[ 444]---> BDD-cost:   43
c ---[ 442]---> BDD-cost:   19
c ---[ 441]---> BDD-cost:   47
c ---[ 440]---> BDD-cost:   59
c ---[ 439]---> BDD-cost:   49
c ---[ 438]---> BDD-cost:   43
c ---[ 437]---> BDD-cost:   43
c ---[ 436]---> BDD-cost:   53
c ---[ 435]---> BDD-cost:   59
c ---[ 434]---> BDD-cost:   47
c ---[ 433]---> BDD-cost:   21
c ---[ 431]---> BDD-cost:   45
c ---[ 430]---> BDD-cost:   47
c ---[ 429]---> BDD-cost:   43
c ---[ 428]---> BDD-cost:   35
c ---[ 427]---> BDD-cost:   33
c ---[ 426]---> BDD-cost:   23
c ---[ 425]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:   17
c ---[ 423]---> BDD-cost:   17
c ---[ 422]---> BDD-cost:   17
c ---[ 420]---> BDD-cost:   45
c ---[ 418]---> BDD-cost:   19
c ---[ 417]---> BDD-cost:   19
c ---[ 416]---> BDD-cost:   19
c ---[ 415]---> BDD-cost:   37
c ---[ 414]---> BDD-cost:   43
c ---[ 413]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:   11
c ---[ 409]---> BDD-cost:   11
c ---[ 408]---> BDD-cost:   11
c ---[ 407]---> BDD-cost:    5
c ---[ 406]---> BDD-cost:   19
c ---[ 405]---> BDD-cost:   17
c ---[ 404]---> BDD-cost:   19
c ---[ 403]---> BDD-cost:   49
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   41
c ---[ 399]---> BDD-cost:   53
c ---[ 398]---> BDD-cost:   59
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    7
c ---[ 395]---> BDD-cost:   41
c ---[ 394]---> BDD-cost:   33
c ---[ 393]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:   19
c ---[ 391]---> BDD-cost:   19
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost: 6553
c ---[ 388]---> BDD-cost:  914
c ---[ 387]---> BDD-cost:  710
c ---[ 386]---> BDD-cost:  122
c ---[ 385]---> BDD-cost:  716
c ---[ 384]---> BDD-cost:  232
c ---[ 383]---> BDD-cost:  147
c ---[ 382]---> BDD-cost:  127
c ---[ 381]---> BDD-cost:   14
c ---[ 380]---> BDD-cost:    1
c ---[ 379]---> BDD-cost: 4032
c ---[ 378]---> BDD-cost:  714
c ---[ 377]---> Adder-cost: 2947   maxlim: 19   bits: 6/5
c ---[ 376]---> BDD-cost: 1340
c ---[ 375]---> BDD-cost:   24
c ---[ 374]---> BDD-cost:  240
c ---[ 373]---> BDD-cost:   78
c ---[ 372]---> BDD-cost:   94
c ---[ 371]---> BDD-cost:  598
c ---[ 370]---> BDD-cost:  734
c ---[ 369]---> BDD-cost:   86
c ---[ 368]---> BDD-cost:   12
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:  126
c ---[ 365]---> BDD-cost:  358
c ---[ 364]---> BDD-cost: 1423
c ---[ 363]---> BDD-cost:   86
c ---[ 362]---> BDD-cost:  738
c ---[ 361]---> BDD-cost: 4656
c ---[ 360]---> BDD-cost:   23
c ---[ 359]---> BDD-cost:   18
c ---[ 358]---> BDD-cost:   12
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:  339
c ---[ 355]---> BDD-cost:   34
c ---[ 354]---> BDD-cost: 2048
c ---[ 353]---> BDD-cost: 1280
c ---[ 352]---> BDD-cost:  236
c ---[ 351]---> BDD-cost:   14
c ---[ 350]---> BDD-cost:   16
c ---[ 349]---> BDD-cost:  774
c ---[ 348]---> BDD-cost:    1
c ---[ 347]---> BDD-cost: 2988
c ---[ 346]---> BDD-cost:  374
c ---[ 345]---> BDD-cost: 3816
c ---[ 344]---> BDD-cost: 3452
c ---[ 343]---> BDD-cost: 1484
c ---[ 342]---> BDD-cost:   42
c ---[ 341]---> BDD-cost:   20
c ---[ 340]---> BDD-cost:  268
c ---[ 339]---> BDD-cost:   36
c ---[ 338]---> BDD-cost:   63
c ---[ 337]---> BDD-cost:   14
c ---[ 336]---> BDD-cost:  458
c ---[ 335]---> BDD-cost:  212
c ---[ 334]---> BDD-cost:   40
c ---[ 333]---> BDD-cost:   56
c ---[ 332]---> BDD-cost:    1
c ---[ 331]---> BDD-cost:   58
c ---[ 330]---> BDD-cost:   54
c ---[ 329]---> BDD-cost:   18
c ---[ 328]---> Adder-cost: 8674   maxlim: 27   bits: 6/5
c ---[ 327]---> BDD-cost:12445
c ---[ 326]---> BDD-cost:  194
c ---[ 325]---> BDD-cost:  104
c ---[ 324]---> BDD-cost:   14
c ---[ 323]---> BDD-cost:    4
c ---[ 322]---> BDD-cost:   82
c ---[ 321]---> BDD-cost:  214
c ---[ 320]---> BDD-cost: 6029
c ---[ 319]---> BDD-cost: 1476
c ---[ 318]---> BDD-cost: 1586
c ---[ 317]---> BDD-cost:  768
c ---[ 316]---> BDD-cost:  850
c ---[ 315]---> BDD-cost: 1317
c ---[ 314]---> BDD-cost:  402
c ---[ 313]---> BDD-cost:  681
c ---[ 312]---> BDD-cost: 6252
c ---[ 311]---> BDD-cost: 9408
c ---[ 310]---> BDD-cost: 2650
c ---[ 309]---> BDD-cost: 1034
c ---[ 308]---> BDD-cost: 1992
c ---[ 307]---> BDD-cost:  296
c ---[ 306]---> BDD-cost:  158
c ---[ 305]---> BDD-cost:  218
c ---[ 304]---> BDD-cost:   84
c ---[ 303]---> BDD-cost:  105
c ---[ 302]---> BDD-cost:  674
c ---[ 301]---> BDD-cost:  464
c ---[ 300]---> BDD-cost:  529
c ---[ 299]---> Adder-cost: 10512   maxlim: 20   bits: 6/5
c ---[ 298]---> BDD-cost: 1330
c ---[ 297]---> BDD-cost: 2050
c ---[ 296]---> BDD-cost: 4523
c ---[ 295]---> BDD-cost: 1380
c ---[ 294]---> BDD-cost: 2608
c ---[ 293]---> BDD-cost: 1264
c ---[ 292]---> BDD-cost: 1785
c ---[ 291]---> BDD-cost:  958
c ---[ 290]---> BDD-cost: 1203
c ---[ 289]---> BDD-cost:  262
c ---[ 288]---> BDD-cost:  346
c ---[ 287]---> BDD-cost: 1298
c ---[ 286]---> BDD-cost:   98
c ---[ 285]---> BDD-cost:  121
c ---[ 284]---> BDD-cost:  610
c ---[ 283]---> BDD-cost:  665
c ---[ 282]---> BDD-cost:  898
c ---[ 281]---> BDD-cost: 1025
c ---[ 280]---> BDD-cost:  201
c ---[ 279]---> BDD-cost: 2210
c ---[ 278]---> BDD-cost:  198
c ---[ 277]---> BDD-cost:   64
c ---[ 276]---> BDD-cost:  412
c ---[ 275]---> BDD-cost:  182
c ---[ 274]---> BDD-cost: 6136
c ---[ 273]---> BDD-cost: 9887
c ---[ 272]---> BDD-cost:  530
c ---[ 271]---> BDD-cost:  898
c ---[ 270]---> BDD-cost:  684
c ---[ 269]---> BDD-cost: 1314
c ---[ 268]---> BDD-cost: 9446
c ---[ 267]---> BDD-cost:  526
c ---[ 266]---> BDD-cost:  597
c ---[ 265]---> BDD-cost: 1898
c ---[ 264]---> BDD-cost:  352
c ---[ 263]---> BDD-cost:  437
c ---[ 262]---> BDD-cost: 4608
c ---[ 261]---> BDD-cost: 1452
c ---[ 260]---> BDD-cost: 2414
c ---[ 259]---> BDD-cost: 1628
c ---[ 258]---> BDD-cost:  810
c ---[ 257]---> BDD-cost:  168
c ---[ 256]---> BDD-cost:  181
c ---[ 255]---> Adder-cost: 4121   maxlim: 14   bits: 5/4
c ---[ 254]---> BDD-cost:  568
c ---[ 253]---> BDD-cost:  618
c ---[ 252]---> BDD-cost:   36
c ---[ 251]---> BDD-cost:   40
c ---[ 250]---> BDD-cost: 1808
c ---[ 249]---> BDD-cost: 3823
c ---[ 248]---> BDD-cost:   58
c ---[ 247]---> BDD-cost: 4462
c ---[ 246]---> Adder-cost: 2035   maxlim: 14   bits: 5/4
c ---[ 245]---> Adder-cost: 2163   maxlim: 11   bits: 5/4
c ---[ 244]---> BDD-cost: 2612
c ---[ 243]---> Adder-cost: 587   maxlim: 5   bits: 4/3
c ---[ 242]---> BDD-cost: 1609
c ---[ 241]---> BDD-cost: 7110
c ---[ 240]---> Adder-cost: 2371   maxlim: 6   bits: 4/3
c ---[ 239]---> Adder-cost: 279   maxlim: 4   bits: 4/3
c ---[ 238]---> BDD-cost:  386
c ---[ 237]---> Adder-cost: 1815   maxlim: 5   bits: 4/3
c ---[ 236]---> BDD-cost: 1174
c ---[ 235]---> Adder-cost: 7711   maxlim: 20   bits: 6/5
c ---[ 234]---> BDD-cost:  312
c ---[ 233]---> BDD-cost:  408
c ---[ 232]---> BDD-cost:19533
c ---[ 231]---> BDD-cost: 1819
c ---[ 230]---> BDD-cost:  437
c ---[ 229]---> BDD-cost: 2422
c ---[ 228]---> BDD-cost:   70
c ---[ 227]---> Adder-cost: 882   maxlim: 10   bits: 5/4
c ---[ 226]---> Adder-cost: 2457   maxlim: 13   bits: 5/4
c ---[ 225]---> BDD-cost: 3474
c ---[ 224]---> BDD-cost:   29
c ---[ 223]---> BDD-cost:  588
c ---[ 222]---> BDD-cost:  213
c ---[ 221]---> BDD-cost:   70
c ---[ 220]---> BDD-cost:   64
c ---[ 219]---> BDD-cost: 3375
c ---[ 218]---> BDD-cost:  742
c ---[ 217]---> BDD-cost:  536
c ---[ 216]---> BDD-cost:  294
c ---[ 215]---> BDD-cost:  338
c ---[ 214]---> BDD-cost:  820
c ---[ 213]---> BDD-cost: 1332
c ---[ 212]---> BDD-cost:  932
c ---[ 211]---> BDD-cost:   16
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost: 1220
c ---[ 208]---> BDD-cost:   40
c ---[ 207]---> BDD-cost: 2412
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost: 1270
c ---[ 204]---> BDD-cost:  208
c ---[ 203]---> BDD-cost:   38
c ---[ 202]---> BDD-cost:    4
c ---[ 201]---> BDD-cost: 1078
c ---[ 200]---> BDD-cost:  298
c ---[ 199]---> BDD-cost: 2278
c ---[ 198]---> BDD-cost:    2
c ---[ 197]---> BDD-cost:  506
c ---[ 196]---> BDD-cost:  130
c ---[ 195]---> BDD-cost:   12
c ---[ 194]---> BDD-cost: 1426
c ---[ 193]---> BDD-cost: 3402
c ---[ 192]---> BDD-cost:  238
c ---[ 191]---> BDD-cost:  308
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:  224
c ---[ 188]---> BDD-cost:  280
c ---[ 187]---> BDD-cost:   76
c ---[ 186]---> BDD-cost:  662
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:  410
c ---[ 183]---> BDD-cost: 1508
c ---[ 182]---> BDD-cost: 1882
c ---[ 181]---> BDD-cost:  250
c ---[ 180]---> BDD-cost:  974
c ---[ 179]---> BDD-cost: 4460
c ---[ 178]---> BDD-cost:  550
c ---[ 177]---> BDD-cost:  400
c ---[ 176]---> BDD-cost:  520
c ---[ 175]---> BDD-cost:  418
c ---[ 174]---> BDD-cost: 1538
c ---[ 173]---> BDD-cost: 2989
c ---[ 172]---> BDD-cost:  744
c ---[ 171]---> BDD-cost:  128
c ---[ 170]---> BDD-cost:   30
c ---[ 169]---> BDD-cost:  381
c ---[ 168]---> BDD-cost:  192
c ---[ 167]---> BDD-cost: 4854
c ---[ 166]---> BDD-cost: 2388
c ---[ 165]---> BDD-cost: 1773
c ---[ 164]---> BDD-cost: 1077
c ---[ 163]---> BDD-cost:  693
c ---[ 162]---> BDD-cost:  202
c ---[ 161]---> BDD-cost: 1231
c ---[ 160]---> BDD-cost:   54
c ---[ 159]---> BDD-cost:  220
c ---[ 158]---> BDD-cost:  100
c ---[ 157]---> BDD-cost: 1052
c ---[ 156]---> BDD-cost:  402
c ---[ 155]---> BDD-cost:  132
c ---[ 154]---> BDD-cost:  103
c ---[ 153]---> BDD-cost: 4879
c ---[ 152]---> BDD-cost:  979
c ---[ 151]---> BDD-cost:  747
c ---[ 150]---> BDD-cost:  229
c ---[ 149]---> BDD-cost:   74
c ---[ 148]---> BDD-cost:  861
c ---[ 147]---> BDD-cost: 1367
c ---[ 146]---> BDD-cost: 1764
c ---[ 145]---> BDD-cost:  176
c ---[ 144]---> BDD-cost:   64
c ---[ 143]---> BDD-cost:   16
c ---[ 142]---> BDD-cost:   46
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:  719
c ---[ 139]---> BDD-cost: 1247
c ---[ 138]---> BDD-cost: 5433
c ---[ 137]---> BDD-cost:   42
c ---[ 136]---> BDD-cost:  164
c ---[ 135]---> BDD-cost: 4280
c ---[ 134]---> BDD-cost:   26
c ---[ 133]---> BDD-cost:  495
c ---[ 132]---> Adder-cost: 2261   maxlim: 9   bits: 5/4
c ---[ 131]---> Adder-cost: 1869   maxlim: 16   bits: 6/5
c ---[ 130]---> BDD-cost:   28
c ---[ 129]---> BDD-cost:  712
c ---[ 128]---> BDD-cost:  642
c ---[ 127]---> BDD-cost:   10
c ---[ 126]---> BDD-cost: 1438
c ---[ 125]---> BDD-cost:   46
c ---[ 124]---> BDD-cost:  832
c ---[ 123]---> BDD-cost:   88
c ---[ 122]---> BDD-cost:   32
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:  330
c ---[ 119]---> BDD-cost:  204
c ---[ 118]---> BDD-cost:    6
c ---[ 117]---> BDD-cost:   42
c ---[ 116]---> BDD-cost:  242
c ---[ 115]---> BDD-cost:   96
c ---[ 114]---> BDD-cost:  328
c ---[ 113]---> BDD-cost: 1814
c ---[ 112]---> BDD-cost:  650
c ---[ 111]---> BDD-cost: 2914
c ---[ 110]---> BDD-cost:  393
c ---[ 109]---> BDD-cost: 1491
c ---[ 108]---> BDD-cost:  133
c ---[ 107]---> BDD-cost:  222
c ---[ 106]---> BDD-cost: 2917
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:  731
c ---[ 103]---> BDD-cost: 4814
c ---[ 102]---> BDD-cost:  242
c ---[ 101]---> BDD-cost:  860
c ---[ 100]---> BDD-cost:   42
c ---[  99]---> BDD-cost: 2263
c ---[  98]---> BDD-cost:  889
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:   46
c ---[  95]---> BDD-cost: 2502
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost: 1412
c ---[  92]---> BDD-cost:   40
c ---[  91]---> BDD-cost:  962
c ---[  90]---> BDD-cost:  593
c ---[  89]---> BDD-cost: 3603
c ---[  88]---> BDD-cost: 7334
c ---[  87]---> BDD-cost: 6232
c ---[  86]---> BDD-cost:   56
c ---[  85]---> BDD-cost:  854
c ---[  84]---> BDD-cost: 2132
c ---[  83]---> BDD-cost:  564
c ---[  82]---> BDD-cost:  530
c ---[  81]---> BDD-cost:  588
c ---[  80]---> BDD-cost: 1928
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost: 1526
c ---[  77]---> BDD-cost:  164
c ---[  76]---> BDD-cost:  836
c ---[  75]---> BDD-cost: 3300
c ---[  74]---> BDD-cost:  436
c ---[  73]---> BDD-cost: 1340
c ---[  72]---> BDD-cost: 1157
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:   30
c ---[  69]---> BDD-cost: 4103
c ---[  68]---> BDD-cost: 2830
c ---[  67]---> BDD-cost: 1784
c ---[  66]---> BDD-cost:  246
c ---[  65]---> BDD-cost:  362
c ---[  64]---> BDD-cost:  576
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:  358
c ---[  61]---> Adder-cost: 3827   maxlim: 14   bits: 5/4
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   40
c ---[  58]---> BDD-cost:  746
c ---[  57]---> BDD-cost:  962
c ---[  56]---> BDD-cost:  154
c ---[  55]---> BDD-cost: 3669
c ---[  54]---> BDD-cost: 2307
c ---[  53]---> BDD-cost: 1162
c ---[  52]---> BDD-cost: 1022
c ---[  51]---> BDD-cost:   88
c ---[  50]---> BDD-cost:  118
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost: 5703
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:   72
c ---[  45]---> BDD-cost:   84
c ---[  44]---> BDD-cost:   70
c ---[  43]---> BDD-cost: 2172
c ---[  42]---> BDD-cost:   52
c ---[  41]---> BDD-cost:   68
c ---[  40]---> BDD-cost: 1812
c ---[  39]---> BDD-cost:   34
c ---[  38]---> BDD-cost:   36
c ---[  37]---> BDD-cost: 5810
c ---[  36]---> BDD-cost: 5039
c ---[  35]---> BDD-cost:  306
c ---[  34]---> BDD-cost:  154
c ---[  33]---> BDD-cost: 1326
c ---[  32]---> Adder-cost: 3997   maxlim: 14   bits: 5/4
c ---[  31]---> Adder-cost: 6712   maxlim: 20   bits: 6/5
c ---[  30]---> BDD-cost: 2005
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:  140
c ---[  27]---> BDD-cost: 1014
c ---[  26]---> BDD-cost:  360
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:    6
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:  414
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:  774
c ---[  18]---> BDD-cost:  216
c ---[  17]---> BDD-cost:  144
c ---[  16]---> BDD-cost:   45
c ---[  15]---> BDD-cost:  222
c ---[  14]---> BDD-cost: 2136
c ---[  13]---> BDD-cost:  120
c ---[  12]---> BDD-cost:  502
c ---[  11]---> BDD-cost:  680
c ---[  10]---> BDD-cost: 2384
c ---[   9]---> BDD-cost: 7427
c ---[   8]---> Adder-cost: 1614   maxlim: 14   bits: 5/4
c ---[   7]---> BDD-cost: 1352
c ---[   6]---> BDD-cost:  398
c ---[   5]---> BDD-cost:  664
c ---[   4]---> BDD-cost:  246
c ---[   3]---> BDD-cost: 7708
c ---[   2]---> Adder-cost: 7609   maxlim: 18   bits: 6/5
c ---[   1]---> BDD-cost:   34
c ---[   0]---> BDD-cost:   28
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 1777837  5996986 |  533351       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/597502          
c   -- var.elim.:  2000/597502          
c   -- var.elim.:  3000/597502          
c   -- var.elim.:  4000/597502          
c   -- var.elim.:  5000/59#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.86 0.97 0.92 2/54 19854
Raw data (stat): 19854 (runsolver) R 19853 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482139315 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99976 s]
Raw data (loadavg): 0.88 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 14731 0 0 0 963 36 0 0 25 0 1 0 482139315 58597376 12203 4294967295 134512640 134672761 3221224544 3221223840 134593975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14306 12203 603 41 0 14265 0
vsize: 57224
[startup+20.0003 s]
Raw data (loadavg): 0.90 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 58638 0 0 0 1855 144 0 0 25 0 1 0 482139315 262787072 54661 4294967295 134512640 134672761 3221224544 3221220344 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64157 54661 603 41 0 64116 0
vsize: 256628
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 93122 0 0 0 2765 231 0 0 25 0 1 0 482139315 425689088 89140 4294967295 134512640 134672761 3221224544 3221223088 134621104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103928 89140 603 41 0 103887 0
vsize: 415712
[startup+40.0013 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 93122 0 0 0 3765 231 0 0 25 0 1 0 482139315 425689088 89140 4294967295 134512640 134672761 3221224544 3221223088 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103928 89140 603 41 0 103887 0
vsize: 415712
[startup+50.0018 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 93122 0 0 0 4765 231 0 0 25 0 1 0 482139315 425689088 89140 4294967295 134512640 134672761 3221224544 3221223008 1075349734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103928 89140 603 41 0 103887 0
vsize: 415712
[startup+60.0017 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 93122 0 0 0 5766 231 0 0 25 0 1 0 482139315 425689088 89140 4294967295 134512640 134672761 3221224544 3221223088 134621116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103928 89140 603 41 0 103887 0
vsize: 415712
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 98067 0 0 0 6750 247 0 0 25 0 1 0 482139315 435695616 91146 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106371 91146 603 41 0 106330 0
vsize: 425484
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 100217 0 0 0 7738 259 0 0 25 0 1 0 482139315 444776448 93296 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108588 93296 603 41 0 108547 0
vsize: 434352
[startup+90.0023 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 101702 0 0 0 8730 266 0 0 25 0 1 0 482139315 451424256 94781 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 110211 94781 603 41 0 110170 0
vsize: 440844
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 103876 0 0 0 9719 276 0 0 25 0 1 0 482139315 460427264 96955 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112409 96955 603 41 0 112368 0
vsize: 449636
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 105466 0 0 0 10711 285 0 0 25 0 1 0 482139315 467677184 98545 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114179 98545 603 41 0 114138 0
vsize: 456716
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 106820 0 0 0 11705 291 0 0 25 0 1 0 482139315 473239552 99899 4294967295 134512640 134672761 3221224544 3221222808 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115537 99899 603 41 0 115496 0
vsize: 462148
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 107984 0 0 0 12700 296 0 0 25 0 1 0 482139315 477822976 101063 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116656 101063 603 41 0 116615 0
vsize: 466624
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 108954 0 0 0 13697 299 0 0 25 0 1 0 482139315 481992704 102033 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117674 102033 603 41 0 117633 0
vsize: 470696
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 109710 0 0 0 14693 304 0 0 25 0 1 0 482139315 485060608 102789 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118423 102789 603 41 0 118382 0
vsize: 473692
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 110363 0 0 0 15689 307 0 0 25 0 1 0 482139315 487735296 103442 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119076 103442 603 41 0 119035 0
vsize: 476304
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 110981 0 0 0 16686 311 0 0 25 0 1 0 482139315 490278912 104060 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119697 104060 603 41 0 119656 0
vsize: 478788
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 111672 0 0 0 17683 314 0 0 25 0 1 0 482139315 493674496 104751 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120526 104751 603 41 0 120485 0
vsize: 482104
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 112487 0 0 0 18679 318 0 0 25 0 1 0 482139315 497680384 105566 4294967295 134512640 134672761 3221224544 3221222728 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121504 105566 603 41 0 121463 0
vsize: 486016
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 113297 0 0 0 19676 322 0 0 25 0 1 0 482139315 502128640 106376 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122590 106376 603 41 0 122549 0
vsize: 490360
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 113996 0 0 0 20674 324 0 0 25 0 1 0 482139315 505630720 107075 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123445 107075 603 41 0 123404 0
vsize: 493780
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 114691 0 0 0 21671 327 0 0 25 0 1 0 482139315 509304832 107770 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124342 107770 603 41 0 124301 0
vsize: 497368
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 115293 0 0 0 22668 331 0 0 25 0 1 0 482139315 512446464 108372 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125109 108372 603 41 0 125068 0
vsize: 500436
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 115911 0 0 0 23664 334 0 0 25 0 1 0 482139315 515764224 108990 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125919 108990 603 41 0 125878 0
vsize: 503676
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 116494 0 0 0 24662 336 0 0 25 0 1 0 482139315 518545408 109573 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126598 109573 603 41 0 126557 0
vsize: 506392
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 116940 0 0 0 25654 343 0 0 25 0 1 0 482139315 520757248 110019 4294967295 134512640 134672761 3221224544 3221222992 134606966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 127138 110019 603 41 0 127097 0
vsize: 508552
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 117920 0 0 0 26648 349 0 0 25 0 1 0 482139315 525234176 110999 4294967295 134512640 134672761 3221224544 3221222992 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 128231 110999 603 41 0 128190 0
vsize: 512924
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 118934 0 0 0 27644 354 0 0 25 0 1 0 482139315 529870848 112013 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129363 112013 603 41 0 129322 0
vsize: 517452
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 119766 0 0 0 28640 358 0 0 25 0 1 0 482139315 534032384 112845 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130379 112845 603 41 0 130338 0
vsize: 521516
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 120549 0 0 0 29636 362 0 0 25 0 1 0 482139315 537772032 113628 4294967295 134512640 134672761 3221224544 3221222992 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131292 113628 603 41 0 131251 0
vsize: 525168
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 121424 0 0 0 30633 365 0 0 25 0 1 0 482139315 541483008 114503 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132198 114503 603 41 0 132157 0
vsize: 528792
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 122324 0 0 0 31629 369 0 0 25 0 1 0 482139315 545488896 115403 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133176 115403 603 41 0 133135 0
vsize: 532704
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 123170 0 0 0 32626 372 0 0 25 0 1 0 482139315 549052416 116249 4294967295 134512640 134672761 3221224544 3221222960 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 134046 116249 603 41 0 134005 0
vsize: 536184
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 124038 0 0 0 33623 375 0 0 25 0 1 0 482139315 552783872 117117 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 134957 117117 603 41 0 134916 0
vsize: 539828
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 124916 0 0 0 34620 379 0 0 25 0 1 0 482139315 556662784 117995 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135904 117995 603 41 0 135863 0
vsize: 543616
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 125766 0 0 0 35616 383 0 0 25 0 1 0 482139315 560111616 118845 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136746 118845 603 41 0 136705 0
vsize: 546984
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 126614 0 0 0 36613 387 0 0 25 0 1 0 482139315 563798016 119693 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 137646 119693 603 41 0 137605 0
vsize: 550584
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 127043 0 0 0 37611 389 0 0 25 0 1 0 482139315 565350400 120122 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 138025 120122 603 41 0 137984 0
vsize: 552100
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 127450 0 0 0 38608 392 0 0 25 0 1 0 482139315 567468032 120529 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 138542 120529 603 41 0 138501 0
vsize: 554168
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 127786 0 0 0 39606 394 0 0 25 0 1 0 482139315 568774656 120865 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 138861 120865 603 41 0 138820 0
vsize: 555444
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 128062 0 0 0 40604 396 0 0 25 0 1 0 482139315 570085376 121141 4294967295 134512640 134672761 3221224544 3221222752 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 139181 121141 603 41 0 139140 0
vsize: 556724
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 128423 0 0 0 41602 398 0 0 25 0 1 0 482139315 571719680 121502 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 139580 121502 603 41 0 139539 0
vsize: 558320
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 128699 0 0 0 42600 400 0 0 25 0 1 0 482139315 573030400 121778 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 139900 121778 603 41 0 139859 0
vsize: 559600
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 128880 0 0 0 43599 402 0 0 25 0 1 0 482139315 573714432 121959 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 140067 121959 603 41 0 140026 0
vsize: 560268
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 129141 0 0 0 44597 404 0 0 25 0 1 0 482139315 574959616 122220 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 140371 122220 603 41 0 140330 0
vsize: 561484
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 129604 0 0 0 45595 405 0 0 25 0 1 0 482139315 577347584 122683 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 140954 122683 603 41 0 140913 0
vsize: 563816
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 130032 0 0 0 46594 407 0 0 25 0 1 0 482139315 579702784 123111 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 141529 123111 603 41 0 141488 0
vsize: 566116
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 130379 0 0 0 47591 410 0 0 25 0 1 0 482139315 581505024 123458 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 141969 123458 603 41 0 141928 0
vsize: 567876
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 130797 0 0 0 48589 413 0 0 25 0 1 0 482139315 583991296 123876 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 142576 123876 603 41 0 142535 0
vsize: 570304
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 131178 0 0 0 49586 416 0 0 25 0 1 0 482139315 586084352 124257 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143087 124257 603 41 0 143046 0
vsize: 572348
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 131468 0 0 0 50584 418 0 0 25 0 1 0 482139315 587632640 124547 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143465 124547 603 41 0 143424 0
vsize: 573860
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 131941 0 0 0 51583 419 0 0 25 0 1 0 482139315 589832192 125020 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144002 125020 603 41 0 143961 0
vsize: 576008
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 133202 0 0 0 52574 428 0 0 25 0 1 0 482139315 594931712 126281 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 145247 126281 603 41 0 145206 0
vsize: 580988
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 134750 0 0 0 53567 436 0 0 25 0 1 0 482139315 601538560 127829 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 146860 127829 603 41 0 146819 0
vsize: 587440
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 135720 0 0 0 54560 443 0 0 25 0 1 0 482139315 605958144 128799 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 147939 128799 603 41 0 147898 0
vsize: 591756
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 136737 0 0 0 55555 448 0 0 25 0 1 0 482139315 610545664 129816 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 149059 129816 603 41 0 149018 0
vsize: 596236
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 137551 0 0 0 56551 453 0 0 25 0 1 0 482139315 614092800 130630 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 149925 130630 603 41 0 149884 0
vsize: 599700
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 138149 0 0 0 57546 458 0 0 25 0 1 0 482139315 616574976 131228 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 150531 131228 603 41 0 150490 0
vsize: 602124
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 139069 0 0 0 58542 462 0 0 25 0 1 0 482139315 620179456 132148 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 151411 132148 603 41 0 151370 0
vsize: 605644
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 139925 0 0 0 59537 467 0 0 25 0 1 0 482139315 624132096 133004 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 152376 133004 603 41 0 152335 0
vsize: 609504
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 140698 0 0 0 60534 470 0 0 25 0 1 0 482139315 627486720 133777 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 153195 133777 603 41 0 153154 0
vsize: 612780
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 141501 0 0 0 61531 473 0 0 25 0 1 0 482139315 630890496 134580 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 154026 134580 603 41 0 153985 0
vsize: 616104
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 142255 0 0 0 62528 477 0 0 25 0 1 0 482139315 633860096 135334 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 154751 135334 603 41 0 154710 0
vsize: 619004
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 142860 0 0 0 63525 480 0 0 25 0 1 0 482139315 636149760 135939 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 155310 135939 603 41 0 155269 0
vsize: 621240
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 143407 0 0 0 64522 483 0 0 25 0 1 0 482139315 638406656 136486 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 155861 136486 603 41 0 155820 0
vsize: 623444
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 144001 0 0 0 65520 485 0 0 25 0 1 0 482139315 640987136 137080 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 156491 137080 603 41 0 156450 0
vsize: 625964
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 144547 0 0 0 66518 488 0 0 25 0 1 0 482139315 643174400 137626 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 157025 137626 603 41 0 156984 0
vsize: 628100
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 144933 0 0 0 67515 491 0 0 25 0 1 0 482139315 644796416 138012 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 157421 138012 603 41 0 157380 0
vsize: 629684
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 145432 0 0 0 68510 496 0 0 25 0 1 0 482139315 646852608 138511 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 157923 138511 603 41 0 157882 0
vsize: 631692
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 145932 0 0 0 69508 499 0 0 25 0 1 0 482139315 649125888 139011 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 158478 139011 603 41 0 158437 0
vsize: 633912
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 146742 0 0 0 70504 502 0 0 25 0 1 0 482139315 652627968 139821 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 159333 139821 603 41 0 159292 0
vsize: 637332
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 147515 0 0 0 71501 506 0 0 25 0 1 0 482139315 656056320 140594 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 160170 140594 603 41 0 160129 0
vsize: 640680
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 148290 0 0 0 72498 508 0 0 25 0 1 0 482139315 659632128 141369 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 161043 141369 603 41 0 161002 0
vsize: 644172
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 149078 0 0 0 73495 512 0 0 25 0 1 0 482139315 664051712 142157 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 162122 142157 603 41 0 162081 0
vsize: 648488
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 149499 0 0 0 74491 516 0 0 25 0 1 0 482139315 665886720 142578 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 162570 142578 603 41 0 162529 0
vsize: 650280
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 149838 0 0 0 75488 519 0 0 25 0 1 0 482139315 667521024 142917 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 162969 142917 603 41 0 162928 0
vsize: 651876
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 150371 0 0 0 76485 523 0 0 25 0 1 0 482139315 669790208 143450 4294967295 134512640 134672761 3221224544 3221222728 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 163523 143450 603 41 0 163482 0
vsize: 654092
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 151075 0 0 0 77482 526 0 0 25 0 1 0 482139315 672989184 144154 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 164304 144154 603 41 0 164263 0
vsize: 657216
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 151587 0 0 0 78478 530 0 0 25 0 1 0 482139315 675639296 144666 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 164951 144666 603 41 0 164910 0
vsize: 659804
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 152094 0 0 0 79474 534 0 0 25 0 1 0 482139315 677814272 145173 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 165482 145173 603 41 0 165441 0
vsize: 661928
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 152882 0 0 0 80471 537 0 0 25 0 1 0 482139315 681037824 145961 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166269 145961 603 41 0 166228 0
vsize: 665076
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 153744 0 0 0 81468 541 0 0 25 0 1 0 482139315 685039616 146823 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 167246 146823 603 41 0 167205 0
vsize: 668984
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 154420 0 0 0 82464 545 0 0 25 0 1 0 482139315 687747072 147499 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 167907 147499 603 41 0 167866 0
vsize: 671628
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 155048 0 0 0 83462 547 0 0 25 0 1 0 482139315 690139136 148127 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 168491 148127 603 41 0 168450 0
vsize: 673964
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 155679 0 0 0 84460 549 0 0 25 0 1 0 482139315 692822016 148758 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 169146 148758 603 41 0 169105 0
vsize: 676584
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 156254 0 0 0 85458 551 0 0 25 0 1 0 482139315 694939648 149333 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 169663 149333 603 41 0 169622 0
vsize: 678652
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 156764 0 0 0 86456 553 0 0 25 0 1 0 482139315 696881152 149843 4294967295 134512640 134672761 3221224544 3221222960 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170137 149843 603 41 0 170096 0
vsize: 680548
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 157228 0 0 0 87454 555 0 0 25 0 1 0 482139315 698843136 150307 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170616 150307 603 41 0 170575 0
vsize: 682464
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 157697 0 0 0 88452 558 0 0 25 0 1 0 482139315 700874752 150776 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171112 150776 603 41 0 171071 0
vsize: 684448
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 158181 0 0 0 89450 560 0 0 25 0 1 0 482139315 703037440 151260 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171640 151260 603 41 0 171599 0
vsize: 686560
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 158684 0 0 0 90449 562 0 0 25 0 1 0 482139315 704987136 151763 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 172116 151763 603 41 0 172075 0
vsize: 688464
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 159137 0 0 0 91446 565 0 0 25 0 1 0 482139315 706650112 152216 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 172522 152216 603 41 0 172481 0
vsize: 690088
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 159574 0 0 0 92444 567 0 0 25 0 1 0 482139315 708300800 152653 4294967295 134512640 134672761 3221224544 3221222832 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 172925 152658 603 41 0 172884 0
vsize: 691700
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 160070 0 0 0 93442 569 0 0 25 0 1 0 482139315 710668288 153149 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 173503 153149 603 41 0 173462 0
vsize: 694012
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 160646 0 0 0 94439 573 0 0 25 0 1 0 482139315 713072640 153725 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174090 153725 603 41 0 174049 0
vsize: 696360
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 161017 0 0 0 95435 577 0 0 25 0 1 0 482139315 714772480 154096 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174505 154096 603 41 0 174464 0
vsize: 698020
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 161271 0 0 0 96433 580 0 0 25 0 1 0 482139315 716017664 154350 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174809 154350 603 41 0 174768 0
vsize: 699236
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 161808 0 0 0 97430 583 0 0 25 0 1 0 482139315 718954496 154887 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 175526 154887 603 41 0 175485 0
vsize: 702104
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 162608 0 0 0 98427 586 0 0 25 0 1 0 482139315 722833408 155687 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 176473 155687 603 41 0 176432 0
vsize: 705892
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 163345 0 0 0 99423 590 0 0 25 0 1 0 482139315 726368256 156424 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 177336 156424 603 41 0 177295 0
vsize: 709344
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 164058 0 0 0 100420 593 0 0 25 0 1 0 482139315 729513984 157137 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 178104 157137 603 41 0 178063 0
vsize: 712416
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 164751 0 0 0 101416 597 0 0 25 0 1 0 482139315 732827648 157830 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 178913 157830 603 41 0 178872 0
vsize: 715652
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 165216 0 0 0 102414 600 0 0 25 0 1 0 482139315 735178752 158295 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 179487 158295 603 41 0 179446 0
vsize: 717948
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 165566 0 0 0 103411 603 0 0 25 0 1 0 482139315 737144832 158645 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 179967 158645 603 41 0 179926 0
vsize: 719868
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 165871 0 0 0 104410 606 0 0 25 0 1 0 482139315 738910208 158950 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 180398 158950 603 41 0 180357 0
vsize: 721592
[startup+1060.05 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 166100 0 0 0 105408 607 0 0 25 0 1 0 482139315 739893248 159179 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 180638 159179 603 41 0 180597 0
vsize: 722552
[startup+1070.05 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 166326 0 0 0 106406 610 0 0 25 0 1 0 482139315 741072896 159405 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 180926 159405 603 41 0 180885 0
vsize: 723704
[startup+1080.06 s]
Raw data (loadavg): 1.05 0.99 0.92 3/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 166591 0 0 0 107405 612 0 0 25 0 1 0 482139315 742449152 159670 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 181262 159670 603 41 0 181221 0
vsize: 725048
[startup+1090.06 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 166808 0 0 0 108403 614 0 0 25 0 1 0 482139315 743624704 159887 4294967295 134512640 134672761 3221224544 3221222192 134566554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 181549 159887 603 41 0 181508 0
vsize: 726196
[startup+1100.07 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 167105 0 0 0 109403 616 0 0 25 0 1 0 482139315 745119744 160184 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 181914 160184 603 41 0 181873 0
vsize: 727656
[startup+1110.07 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 167506 0 0 0 110401 618 0 0 25 0 1 0 482139315 747352064 160585 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 182459 160585 603 41 0 182418 0
vsize: 729836
[startup+1120.07 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 167906 0 0 0 111400 620 0 0 25 0 1 0 482139315 749367296 160985 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 182951 160985 603 41 0 182910 0
vsize: 731804
[startup+1130.07 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 168317 0 0 0 112398 622 0 0 25 0 1 0 482139315 751435776 161396 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 183456 161396 603 41 0 183415 0
vsize: 733824
[startup+1140.07 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 168730 0 0 0 113396 624 0 0 25 0 1 0 482139315 753586176 161809 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 183981 161809 603 41 0 183940 0
vsize: 735924
[startup+1150.07 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 169137 0 0 0 114394 626 0 0 25 0 1 0 482139315 755642368 162216 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 184483 162216 603 41 0 184442 0
vsize: 737932
[startup+1160.07 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 169527 0 0 0 115392 628 0 0 25 0 1 0 482139315 757706752 162606 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 184987 162606 603 41 0 184946 0
vsize: 739948
[startup+1170.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 169853 0 0 0 116392 629 0 0 25 0 1 0 482139315 759410688 162932 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 185403 162932 603 41 0 185362 0
vsize: 741612
[startup+1180.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 170082 0 0 0 117390 631 0 0 25 0 1 0 482139315 760459264 163161 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 185659 163161 603 41 0 185618 0
vsize: 742636
[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 170394 0 0 0 118389 632 0 0 25 0 1 0 482139315 762064896 163473 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 186051 163473 603 41 0 186010 0
vsize: 744204
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19854
Raw data (stat): 19854 (minisat+) R 19853 25347 25346 0 -1 0 170710 0 0 0 119388 633 0 0 25 0 1 0 482139315 763699200 163789 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 186450 163789 603 41 0 186409 0
vsize: 745800
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.53 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 19854
Raw data (stat): 19854 (minisat+) Z 19853 25347 25346 0 -1 12 170710 0 0 0 119388 675 0 0 25 0 1 0 482139315 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.53
CPU time (s): 1200.64
CPU user time (s): 1193.89
CPU system time (s): 6.75597
CPU usage (%): 100.009
Max. virtual memory (Kb): 745800
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####