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 14715

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        614024 kB
Buffers:         34368 kB
Cached:         354680 kB
SwapCached:        388 kB
Active:         131972 kB
Inactive:       259596 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        613772 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6224 kB
Slab:            23380 kB
Committed_AS:    63812 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:13:34 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 20267 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]---> 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3100110  9537700 | 1033370       0        0     nan |  0.000 % |
c |       100 | 3100110  9537700 | 1136707     100      334     3.3 |  0.218 % |
c |       250 | 3099955  9537235 | 1250377     193      727     3.8 |  0.223 % |
c |       475 | 3099825  9536845 | 1375415     354     1707     4.8 |  0.227 % |
c |       812 | 3099475  9535795 | 1512957     523     2453     4.7 |  0.239 % |
c |      1319 | 3099120  9534730 | 1664252     869     4195     4.8 |  0.251 % |
c |      2078 | 3098620  9533230 | 1830677    1387     7417     5.3 |  0.267 % |
c |      3217 | 3097382  9529516 | 2013745    1973    12487     6.3 |  0.308 % |
c |      4925 | 3096085  9525637 | 2215120    3132    23837     7.6 |  0.351 % |
c |      7487 | 3093428  9517640 | 2436632    4580    33832     7.4 |  0.435 % |
#### 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.96 0.97 0.91 2/55 14838
Raw data (stat): 14838 (runsolver) R 14837 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540902388 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 14243 0 0 0 960 38 0 0 25 0 1 0 540902388 56315904 11691 4294967295 134512640 134672761 3221224544 3221139488 134592275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13749 11691 603 41 0 13708 0
vsize: 54996
[startup+20.0006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 51848 0 0 0 1871 128 0 0 25 0 1 0 540902388 218009600 47831 4294967295 134512640 134672761 3221224544 3221168672 1075350373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53225 47832 603 41 0 53184 0
vsize: 212900
[startup+30.0011 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 66861 0 0 0 2835 163 0 0 25 0 1 0 540902388 298770432 62844 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72942 62844 603 41 0 72901 0
vsize: 291768
[startup+40.0011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 66946 0 0 0 3835 164 0 0 25 0 1 0 540902388 298770432 62929 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72942 62929 603 41 0 72901 0
vsize: 291768
[startup+50.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67026 0 0 0 4834 165 0 0 25 0 1 0 540902388 298905600 63009 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72975 63009 603 41 0 72934 0
vsize: 291900
[startup+60.0039 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67027 0 0 0 5833 166 0 0 25 0 1 0 540902388 298905600 63010 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72975 63010 603 41 0 72934 0
vsize: 291900
[startup+70.0038 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67028 0 0 0 6833 166 0 0 25 0 1 0 540902388 298905600 63011 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72975 63011 603 41 0 72934 0
vsize: 291900
[startup+80.0051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67068 0 0 0 7833 167 0 0 25 0 1 0 540902388 299040768 63051 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73008 63051 603 41 0 72967 0
vsize: 292032
[startup+90.0046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67069 0 0 0 8832 167 0 0 25 0 1 0 540902388 299040768 63052 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73008 63052 603 41 0 72967 0
vsize: 292032
[startup+100.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67094 0 0 0 9832 167 0 0 25 0 1 0 540902388 299040768 63077 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73008 63077 603 41 0 72967 0
vsize: 292032
[startup+110.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67094 0 0 0 10832 168 0 0 25 0 1 0 540902388 299040768 63077 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73008 63077 603 41 0 72967 0
vsize: 292032
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67117 0 0 0 11831 168 0 0 25 0 1 0 540902388 299040768 63100 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73008 63100 603 41 0 72967 0
vsize: 292032
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14838
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67139 0 0 0 12831 168 0 0 25 0 1 0 540902388 299175936 63122 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73041 63122 603 41 0 73000 0
vsize: 292164
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67143 0 0 0 13831 168 0 0 25 0 1 0 540902388 299175936 63126 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73041 63126 603 41 0 73000 0
vsize: 292164
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67154 0 0 0 14831 168 0 0 25 0 1 0 540902388 299175936 63137 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73041 63137 603 41 0 73000 0
vsize: 292164
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67155 0 0 0 15831 169 0 0 25 0 1 0 540902388 299175936 63138 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73041 63138 603 41 0 73000 0
vsize: 292164
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67198 0 0 0 16831 169 0 0 25 0 1 0 540902388 299175936 63181 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73041 63181 603 41 0 73000 0
vsize: 292164
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67208 0 0 0 17831 169 0 0 25 0 1 0 540902388 299175936 63191 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73041 63191 603 41 0 73000 0
vsize: 292164
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67214 0 0 0 18832 169 0 0 25 0 1 0 540902388 299315200 63197 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63197 603 41 0 73034 0
vsize: 292300
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67219 0 0 0 19832 169 0 0 25 0 1 0 540902388 299315200 63202 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63202 603 41 0 73034 0
vsize: 292300
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67221 0 0 0 20832 169 0 0 25 0 1 0 540902388 299315200 63204 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63204 603 41 0 73034 0
vsize: 292300
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67221 0 0 0 21832 169 0 0 25 0 1 0 540902388 299315200 63204 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63204 603 41 0 73034 0
vsize: 292300
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67222 0 0 0 22832 169 0 0 25 0 1 0 540902388 299315200 63205 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63205 603 41 0 73034 0
vsize: 292300
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67243 0 0 0 23832 169 0 0 25 0 1 0 540902388 299315200 63226 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63226 603 41 0 73034 0
vsize: 292300
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67246 0 0 0 24832 169 0 0 25 0 1 0 540902388 299315200 63229 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73075 63229 603 41 0 73034 0
vsize: 292300
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67247 0 0 0 25831 170 0 0 25 0 1 0 540902388 299315200 63230 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73075 63230 603 41 0 73034 0
vsize: 292300
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67275 0 0 0 26831 170 0 0 25 0 1 0 540902388 299450368 63258 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63258 603 41 0 73067 0
vsize: 292432
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67279 0 0 0 27831 170 0 0 25 0 1 0 540902388 299450368 63262 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63262 603 41 0 73067 0
vsize: 292432
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67279 0 0 0 28831 170 0 0 25 0 1 0 540902388 299450368 63262 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63262 603 41 0 73067 0
vsize: 292432
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67279 0 0 0 29832 170 0 0 25 0 1 0 540902388 299450368 63262 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63262 603 41 0 73067 0
vsize: 292432
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67280 0 0 0 30832 170 0 0 25 0 1 0 540902388 299450368 63263 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63263 603 41 0 73067 0
vsize: 292432
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67281 0 0 0 31832 170 0 0 25 0 1 0 540902388 299450368 63264 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63264 603 41 0 73067 0
vsize: 292432
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67282 0 0 0 32832 170 0 0 25 0 1 0 540902388 299450368 63265 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63265 603 41 0 73067 0
vsize: 292432
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67283 0 0 0 33832 170 0 0 25 0 1 0 540902388 299450368 63266 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63266 603 41 0 73067 0
vsize: 292432
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67284 0 0 0 34832 170 0 0 25 0 1 0 540902388 299450368 63267 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63267 603 41 0 73067 0
vsize: 292432
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67347 0 0 0 35833 170 0 0 25 0 1 0 540902388 299606016 63330 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63330 603 41 0 73105 0
vsize: 292584
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67347 0 0 0 36833 170 0 0 25 0 1 0 540902388 299606016 63330 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63330 603 41 0 73105 0
vsize: 292584
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67350 0 0 0 37833 170 0 0 25 0 1 0 540902388 299606016 63333 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63333 603 41 0 73105 0
vsize: 292584
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14840
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67352 0 0 0 38833 171 0 0 25 0 1 0 540902388 299606016 63335 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63335 603 41 0 73105 0
vsize: 292584
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14893
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67352 0 0 0 39833 171 0 0 25 0 1 0 540902388 299606016 63335 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63335 603 41 0 73105 0
vsize: 292584
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14893
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67353 0 0 0 40833 171 0 0 25 0 1 0 540902388 299606016 63336 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63336 603 41 0 73105 0
vsize: 292584
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14893
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67353 0 0 0 41833 171 0 0 25 0 1 0 540902388 299606016 63336 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63336 603 41 0 73105 0
vsize: 292584
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14893
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67355 0 0 0 42833 171 0 0 25 0 1 0 540902388 299606016 63338 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63338 603 41 0 73105 0
vsize: 292584
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14895
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67355 0 0 0 43833 171 0 0 25 0 1 0 540902388 299606016 63338 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63338 603 41 0 73105 0
vsize: 292584
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14895
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67356 0 0 0 44833 171 0 0 25 0 1 0 540902388 299606016 63339 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63339 603 41 0 73105 0
vsize: 292584
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14895
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67358 0 0 0 45833 171 0 0 25 0 1 0 540902388 299606016 63341 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63341 603 41 0 73105 0
vsize: 292584
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67360 0 0 0 46833 171 0 0 25 0 1 0 540902388 299606016 63343 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63343 603 41 0 73105 0
vsize: 292584
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67365 0 0 0 47833 171 0 0 25 0 1 0 540902388 299745280 63348 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63348 603 41 0 73139 0
vsize: 292720
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67365 0 0 0 48833 171 0 0 25 0 1 0 540902388 299745280 63348 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63348 603 41 0 73139 0
vsize: 292720
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67366 0 0 0 49833 171 0 0 25 0 1 0 540902388 299745280 63349 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63349 603 41 0 73139 0
vsize: 292720
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67367 0 0 0 50833 172 0 0 25 0 1 0 540902388 299745280 63350 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63350 603 41 0 73139 0
vsize: 292720
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67367 0 0 0 51833 172 0 0 25 0 1 0 540902388 299745280 63350 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63350 603 41 0 73139 0
vsize: 292720
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67367 0 0 0 52833 172 0 0 25 0 1 0 540902388 299745280 63350 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63350 603 41 0 73139 0
vsize: 292720
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67377 0 0 0 53834 172 0 0 25 0 1 0 540902388 299745280 63360 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63360 603 41 0 73139 0
vsize: 292720
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67455 0 0 0 54833 172 0 0 25 0 1 0 540902388 299880448 63438 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73213 63438 603 41 0 73172 0
vsize: 292852
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67455 0 0 0 55834 172 0 0 25 0 1 0 540902388 299880448 63438 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73213 63438 603 41 0 73172 0
vsize: 292852
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67497 0 0 0 56834 172 0 0 25 0 1 0 540902388 299880448 63480 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73213 63480 603 41 0 73172 0
vsize: 292852
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67499 0 0 0 57834 173 0 0 25 0 1 0 540902388 300015616 63482 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73246 63482 603 41 0 73205 0
vsize: 292984
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67505 0 0 0 58834 173 0 0 25 0 1 0 540902388 300015616 63488 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73246 63488 603 41 0 73205 0
vsize: 292984
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67505 0 0 0 59834 173 0 0 25 0 1 0 540902388 300015616 63488 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73246 63488 603 41 0 73205 0
vsize: 292984
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67534 0 0 0 60834 173 0 0 25 0 1 0 540902388 300015616 63517 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73246 63517 603 41 0 73205 0
vsize: 292984
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67551 0 0 0 61834 173 0 0 25 0 1 0 540902388 300150784 63534 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63534 603 41 0 73238 0
vsize: 293116
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67552 0 0 0 62835 173 0 0 25 0 1 0 540902388 300150784 63535 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63535 603 41 0 73238 0
vsize: 293116
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67553 0 0 0 63835 173 0 0 25 0 1 0 540902388 300150784 63536 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63536 603 41 0 73238 0
vsize: 293116
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67561 0 0 0 64835 173 0 0 25 0 1 0 540902388 300150784 63544 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63544 603 41 0 73238 0
vsize: 293116
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67577 0 0 0 65835 173 0 0 25 0 1 0 540902388 300150784 63560 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63560 603 41 0 73238 0
vsize: 293116
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67577 0 0 0 66835 174 0 0 25 0 1 0 540902388 300150784 63560 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63560 603 41 0 73238 0
vsize: 293116
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67577 0 0 0 67835 174 0 0 25 0 1 0 540902388 300150784 63560 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63560 603 41 0 73238 0
vsize: 293116
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67578 0 0 0 68835 174 0 0 25 0 1 0 540902388 300150784 63561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63561 603 41 0 73238 0
vsize: 293116
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67580 0 0 0 69835 174 0 0 25 0 1 0 540902388 300150784 63563 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63563 603 41 0 73238 0
vsize: 293116
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67581 0 0 0 70836 174 0 0 25 0 1 0 540902388 300150784 63564 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63564 603 41 0 73238 0
vsize: 293116
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67590 0 0 0 71835 174 0 0 25 0 1 0 540902388 300285952 63573 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63573 603 41 0 73271 0
vsize: 293248
[startup+730.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14897
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67599 0 0 0 72835 174 0 0 25 0 1 0 540902388 300285952 63582 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63582 603 41 0 73271 0
vsize: 293248
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14899
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67602 0 0 0 73835 174 0 0 25 0 1 0 540902388 300285952 63585 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63585 603 41 0 73271 0
vsize: 293248
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67603 0 0 0 74835 174 0 0 25 0 1 0 540902388 300285952 63586 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63586 603 41 0 73271 0
vsize: 293248
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67605 0 0 0 75835 174 0 0 25 0 1 0 540902388 300285952 63588 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63588 603 41 0 73271 0
vsize: 293248
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67606 0 0 0 76835 174 0 0 25 0 1 0 540902388 300285952 63589 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63589 603 41 0 73271 0
vsize: 293248
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67607 0 0 0 77835 174 0 0 25 0 1 0 540902388 300285952 63590 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63590 603 41 0 73271 0
vsize: 293248
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67608 0 0 0 78836 174 0 0 25 0 1 0 540902388 300285952 63591 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63591 603 41 0 73271 0
vsize: 293248
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67640 0 0 0 79836 174 0 0 25 0 1 0 540902388 300285952 63623 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63623 603 41 0 73271 0
vsize: 293248
[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67641 0 0 0 80836 175 0 0 25 0 1 0 540902388 300285952 63624 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63624 603 41 0 73271 0
vsize: 293248
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67641 0 0 0 81836 175 0 0 25 0 1 0 540902388 300285952 63624 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73312 63624 603 41 0 73271 0
vsize: 293248
[startup+830.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67661 0 0 0 82838 175 0 0 25 0 1 0 540902388 300421120 63644 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73345 63644 603 41 0 73304 0
vsize: 293380
[startup+840.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67661 0 0 0 83838 175 0 0 25 0 1 0 540902388 300421120 63644 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73345 63644 603 41 0 73304 0
vsize: 293380
[startup+850.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67662 0 0 0 84838 175 0 0 25 0 1 0 540902388 300421120 63645 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73345 63645 603 41 0 73304 0
vsize: 293380
[startup+860.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67667 0 0 0 85838 175 0 0 25 0 1 0 540902388 300421120 63650 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73345 63650 603 41 0 73304 0
vsize: 293380
[startup+870.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67668 0 0 0 86838 175 0 0 25 0 1 0 540902388 300421120 63651 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73345 63651 603 41 0 73304 0
vsize: 293380
[startup+880.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67683 0 0 0 87839 175 0 0 25 0 1 0 540902388 300421120 63666 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73345 63666 603 41 0 73304 0
vsize: 293380
[startup+890.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67698 0 0 0 88839 175 0 0 25 0 1 0 540902388 300556288 63681 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63681 603 41 0 73337 0
vsize: 293512
[startup+900.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67702 0 0 0 89839 175 0 0 25 0 1 0 540902388 300556288 63685 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63685 603 41 0 73337 0
vsize: 293512
[startup+910.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67705 0 0 0 90839 176 0 0 25 0 1 0 540902388 300556288 63688 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63688 603 41 0 73337 0
vsize: 293512
[startup+920.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67705 0 0 0 91839 176 0 0 25 0 1 0 540902388 300556288 63688 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63688 603 41 0 73337 0
vsize: 293512
[startup+930.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67705 0 0 0 92839 176 0 0 25 0 1 0 540902388 300556288 63688 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63688 603 41 0 73337 0
vsize: 293512
[startup+940.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67706 0 0 0 93839 176 0 0 25 0 1 0 540902388 300556288 63689 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+950.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67706 0 0 0 94839 176 0 0 25 0 1 0 540902388 300556288 63689 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+960.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67706 0 0 0 95839 176 0 0 25 0 1 0 540902388 300556288 63689 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+970.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67706 0 0 0 96839 176 0 0 25 0 1 0 540902388 300556288 63689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+980.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67715 0 0 0 97840 176 0 0 25 0 1 0 540902388 300556288 63698 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63698 603 41 0 73337 0
vsize: 293512
[startup+990.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67723 0 0 0 98840 176 0 0 25 0 1 0 540902388 300556288 63706 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63706 603 41 0 73337 0
vsize: 293512
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67726 0 0 0 99840 176 0 0 25 0 1 0 540902388 300556288 63709 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73378 63709 603 41 0 73337 0
vsize: 293512
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67728 0 0 0 100840 176 0 0 25 0 1 0 540902388 300691456 63711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63711 603 41 0 73370 0
vsize: 293644
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67730 0 0 0 101840 176 0 0 25 0 1 0 540902388 300691456 63713 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63713 603 41 0 73370 0
vsize: 293644
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14901
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67732 0 0 0 102840 176 0 0 25 0 1 0 540902388 300691456 63715 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63715 603 41 0 73370 0
vsize: 293644
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67742 0 0 0 103840 176 0 0 25 0 1 0 540902388 300691456 63725 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63725 603 41 0 73370 0
vsize: 293644
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67745 0 0 0 104840 177 0 0 25 0 1 0 540902388 300691456 63728 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63728 603 41 0 73370 0
vsize: 293644
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67745 0 0 0 105841 177 0 0 25 0 1 0 540902388 300691456 63728 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63728 603 41 0 73370 0
vsize: 293644
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67752 0 0 0 106841 177 0 0 25 0 1 0 540902388 300691456 63735 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63735 603 41 0 73370 0
vsize: 293644
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67753 0 0 0 107841 177 0 0 25 0 1 0 540902388 300691456 63736 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63736 603 41 0 73370 0
vsize: 293644
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67756 0 0 0 108841 177 0 0 25 0 1 0 540902388 300691456 63739 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63739 603 41 0 73370 0
vsize: 293644
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67756 0 0 0 109841 177 0 0 25 0 1 0 540902388 300691456 63739 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63739 603 41 0 73370 0
vsize: 293644
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67757 0 0 0 110841 177 0 0 25 0 1 0 540902388 300691456 63740 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63740 603 41 0 73370 0
vsize: 293644
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67757 0 0 0 111841 177 0 0 25 0 1 0 540902388 300691456 63740 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63740 603 41 0 73370 0
vsize: 293644
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67759 0 0 0 112842 177 0 0 25 0 1 0 540902388 300691456 63742 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63742 603 41 0 73370 0
vsize: 293644
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67760 0 0 0 113842 177 0 0 25 0 1 0 540902388 300691456 63743 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73411 63743 603 41 0 73370 0
vsize: 293644
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67763 0 0 0 114842 177 0 0 25 0 1 0 540902388 300822528 63746 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73443 63746 603 41 0 73402 0
vsize: 293772
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67765 0 0 0 115843 177 0 0 25 0 1 0 540902388 300822528 63748 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73443 63748 603 41 0 73402 0
vsize: 293772
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67765 0 0 0 116843 177 0 0 25 0 1 0 540902388 300822528 63748 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73443 63748 603 41 0 73402 0
vsize: 293772
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67766 0 0 0 117843 177 0 0 25 0 1 0 540902388 300822528 63749 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73443 63749 603 41 0 73402 0
vsize: 293772
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67767 0 0 0 118845 177 0 0 25 0 1 0 540902388 300822528 63750 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73443 63750 603 41 0 73402 0
vsize: 293772
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14903
Raw data (stat): 14838 (minisat+) R 14837 20024 20023 0 -1 0 67769 0 0 0 119845 178 0 0 25 0 1 0 540902388 300822528 63752 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73443 63752 603 41 0 73402 0
vsize: 293772
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.26 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 14903
Raw data (stat): 14838 (minisat+) Z 14837 20024 20023 0 -1 12 67771 0 0 0 119845 190 0 0 22 0 1 0 540902388 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.26
CPU time (s): 1200.36
CPU user time (s): 1198.45
CPU system time (s): 1.90571
CPU usage (%): 100.008
Max. virtual memory (Kb): 293772
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####