PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        645984 kB
Buffers:         38528 kB
Cached:         325040 kB
SwapCached:       2272 kB
Active:         175020 kB
Inactive:       193688 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        645732 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14352 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 20:42:01 (client local time) WITH STATUS 0 IN 1200.64 SECONDS
stats: 15262 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 ==================================[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.15 0.03 0.01 1/54 9089
Raw data (stat): 9089 (runsolver) D 9088 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 481060292 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.004 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 14243 0 0 0 962 36 0 0 25 0 1 0 481060292 56315904 11691 4294967295 134512640 134672761 3221224544 3221215520 134592548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13749 11691 603 41 0 13708 0
vsize: 54996
[startup+20.0169 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 51117 0 0 0 1871 128 0 0 25 0 1 0 481060292 215576576 47100 4294967295 134512640 134672761 3221224544 3221179008 1075349707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52631 47100 603 41 0 52590 0
vsize: 210524
[startup+30.0246 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 66861 0 0 0 2834 167 0 0 25 0 1 0 481060292 298770432 62844 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72942 62844 603 41 0 72901 0
vsize: 291768
[startup+40.038 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 66869 0 0 0 3834 167 0 0 25 0 1 0 481060292 298770432 62852 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72942 62852 603 41 0 72901 0
vsize: 291768
[startup+50.0428 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67026 0 0 0 4834 168 0 0 25 0 1 0 481060292 298905600 63009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72975 63009 603 41 0 72934 0
vsize: 291900
[startup+60.0429 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67027 0 0 0 5832 169 0 0 25 0 1 0 481060292 298905600 63010 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72975 63010 603 41 0 72934 0
vsize: 291900
[startup+70.0432 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67028 0 0 0 6831 169 0 0 25 0 1 0 481060292 298905600 63011 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72975 63011 603 41 0 72934 0
vsize: 291900
[startup+80.0435 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67068 0 0 0 7831 169 0 0 25 0 1 0 481060292 299040768 63051 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73008 63051 603 41 0 72967 0
vsize: 292032
[startup+90.0601 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67069 0 0 0 8833 169 0 0 25 0 1 0 481060292 299040768 63052 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73008 63052 603 41 0 72967 0
vsize: 292032
[startup+100.063 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67094 0 0 0 9833 170 0 0 25 0 1 0 481060292 299040768 63077 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73008 63077 603 41 0 72967 0
vsize: 292032
[startup+110.071 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67094 0 0 0 10833 170 0 0 25 0 1 0 481060292 299040768 63077 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73008 63077 603 41 0 72967 0
vsize: 292032
[startup+120.076 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67114 0 0 0 11833 171 0 0 25 0 1 0 481060292 299040768 63097 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73008 63097 603 41 0 72967 0
vsize: 292032
[startup+130.077 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67136 0 0 0 12833 171 0 0 25 0 1 0 481060292 299040768 63119 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73008 63119 603 41 0 72967 0
vsize: 292032
[startup+140.078 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67143 0 0 0 13833 172 0 0 25 0 1 0 481060292 299175936 63126 4294967295 134512640 134672761 3221224544 3221223716 134556632 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.078 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67154 0 0 0 14833 172 0 0 25 0 1 0 481060292 299175936 63137 4294967295 134512640 134672761 3221224544 3221223716 134556627 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.08 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67155 0 0 0 15832 172 0 0 25 0 1 0 481060292 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.08 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67177 0 0 0 16832 172 0 0 25 0 1 0 481060292 299175936 63160 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73041 63160 603 41 0 73000 0
vsize: 292164
[startup+180.081 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67200 0 0 0 17832 173 0 0 25 0 1 0 481060292 299175936 63183 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73041 63183 603 41 0 73000 0
vsize: 292164
[startup+190.086 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67214 0 0 0 18832 174 0 0 25 0 1 0 481060292 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.19 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67219 0 0 0 19842 174 0 0 25 0 1 0 481060292 299315200 63202 4294967295 134512640 134672761 3221224544 3221223680 134560688 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.189 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67221 0 0 0 20842 174 0 0 25 0 1 0 481060292 299315200 63204 4294967295 134512640 134672761 3221224544 3221223752 134561960 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.19 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67221 0 0 0 21842 174 0 0 25 0 1 0 481060292 299315200 63204 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.19 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67222 0 0 0 22842 175 0 0 25 0 1 0 481060292 299315200 63205 4294967295 134512640 134672761 3221224544 3221223712 134560822 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.191 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67243 0 0 0 23842 175 0 0 25 0 1 0 481060292 299315200 63226 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.191 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67246 0 0 0 24840 175 0 0 25 0 1 0 481060292 299315200 63229 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63229 603 41 0 73034 0
vsize: 292300
[startup+260.204 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67247 0 0 0 25841 175 0 0 25 0 1 0 481060292 299315200 63230 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73075 63230 603 41 0 73034 0
vsize: 292300
[startup+270.211 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67266 0 0 0 26842 176 0 0 25 0 1 0 481060292 299450368 63249 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63249 603 41 0 73067 0
vsize: 292432
[startup+280.211 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67275 0 0 0 27841 176 0 0 25 0 1 0 481060292 299450368 63258 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63258 603 41 0 73067 0
vsize: 292432
[startup+290.212 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67279 0 0 0 28841 176 0 0 25 0 1 0 481060292 299450368 63262 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.212 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67279 0 0 0 29841 177 0 0 25 0 1 0 481060292 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+310.213 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67280 0 0 0 30841 177 0 0 25 0 1 0 481060292 299450368 63263 4294967295 134512640 134672761 3221224544 3221223716 134556660 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.214 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67280 0 0 0 31841 177 0 0 25 0 1 0 481060292 299450368 63263 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73108 63263 603 41 0 73067 0
vsize: 292432
[startup+330.215 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67282 0 0 0 32841 177 0 0 25 0 1 0 481060292 299450368 63265 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.216 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67283 0 0 0 33841 177 0 0 25 0 1 0 481060292 299450368 63266 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.217 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67284 0 0 0 34841 177 0 0 25 0 1 0 481060292 299450368 63267 4294967295 134512640 134672761 3221224544 3221223716 134556658 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.217 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67347 0 0 0 35841 178 0 0 25 0 1 0 481060292 299606016 63330 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.217 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67347 0 0 0 36841 178 0 0 25 0 1 0 481060292 299606016 63330 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.217 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67350 0 0 0 37841 179 0 0 25 0 1 0 481060292 299606016 63333 4294967295 134512640 134672761 3221224544 3221223760 134561979 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.217 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67352 0 0 0 38840 179 0 0 25 0 1 0 481060292 299606016 63335 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.219 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67352 0 0 0 39840 179 0 0 25 0 1 0 481060292 299606016 63335 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.219 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67353 0 0 0 40840 179 0 0 25 0 1 0 481060292 299606016 63336 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.219 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67353 0 0 0 41840 180 0 0 25 0 1 0 481060292 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+430.22 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67355 0 0 0 42840 180 0 0 25 0 1 0 481060292 299606016 63338 4294967295 134512640 134672761 3221224544 3221223760 134561999 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.22 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67355 0 0 0 43840 180 0 0 25 0 1 0 481060292 299606016 63338 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.221 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67356 0 0 0 44840 180 0 0 25 0 1 0 481060292 299606016 63339 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.221 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67358 0 0 0 45840 180 0 0 25 0 1 0 481060292 299606016 63341 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.222 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67358 0 0 0 46840 181 0 0 25 0 1 0 481060292 299606016 63341 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73146 63341 603 41 0 73105 0
vsize: 292584
[startup+480.222 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67365 0 0 0 47840 181 0 0 25 0 1 0 481060292 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.227 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67365 0 0 0 48840 181 0 0 25 0 1 0 481060292 299745280 63348 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.228 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67366 0 0 0 49840 182 0 0 25 0 1 0 481060292 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.227 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67366 0 0 0 50839 182 0 0 25 0 1 0 481060292 299745280 63349 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63349 603 41 0 73139 0
vsize: 292720
[startup+520.228 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67367 0 0 0 51839 182 0 0 25 0 1 0 481060292 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+530.228 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67367 0 0 0 52839 182 0 0 25 0 1 0 481060292 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+540.23 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67368 0 0 0 53839 183 0 0 25 0 1 0 481060292 299745280 63351 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73180 63351 603 41 0 73139 0
vsize: 292720
[startup+550.23 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67455 0 0 0 54839 183 0 0 25 0 1 0 481060292 299880448 63438 4294967295 134512640 134672761 3221224544 3221223760 134561979 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.23 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67455 0 0 0 55839 183 0 0 25 0 1 0 481060292 299880448 63438 4294967295 134512640 134672761 3221224544 3221223716 134556632 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.231 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67497 0 0 0 56839 184 0 0 25 0 1 0 481060292 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.231 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67498 0 0 0 57838 184 0 0 25 0 1 0 481060292 300015616 63481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73246 63481 603 41 0 73205 0
vsize: 292984
[startup+590.232 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67499 0 0 0 58838 184 0 0 25 0 1 0 481060292 300015616 63482 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73246 63482 603 41 0 73205 0
vsize: 292984
[startup+600.232 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67505 0 0 0 59838 185 0 0 25 0 1 0 481060292 300015616 63488 4294967295 134512640 134672761 3221224544 3221223760 134561948 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.233 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67505 0 0 0 60838 185 0 0 25 0 1 0 481060292 300015616 63488 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73246 63488 603 41 0 73205 0
vsize: 292984
[startup+620.233 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67551 0 0 0 61838 185 0 0 25 0 1 0 481060292 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.233 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67552 0 0 0 62838 185 0 0 25 0 1 0 481060292 300150784 63535 4294967295 134512640 134672761 3221224544 3221223716 134556682 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.234 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67553 0 0 0 63837 186 0 0 25 0 1 0 481060292 300150784 63536 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.235 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67561 0 0 0 64837 186 0 0 25 0 1 0 481060292 300150784 63544 4294967295 134512640 134672761 3221224544 3221223752 134561960 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.235 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67561 0 0 0 65837 186 0 0 25 0 1 0 481060292 300150784 63544 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63544 603 41 0 73238 0
vsize: 293116
[startup+670.246 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67577 0 0 0 66838 186 0 0 25 0 1 0 481060292 300150784 63560 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.257 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67577 0 0 0 67839 187 0 0 25 0 1 0 481060292 300150784 63560 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.259 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67577 0 0 0 68839 187 0 0 25 0 1 0 481060292 300150784 63560 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63560 603 41 0 73238 0
vsize: 293116
[startup+700.261 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67579 0 0 0 69839 187 0 0 25 0 1 0 481060292 300150784 63562 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63562 603 41 0 73238 0
vsize: 293116
[startup+710.264 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67580 0 0 0 70839 187 0 0 25 0 1 0 481060292 300150784 63563 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73279 63563 603 41 0 73238 0
vsize: 293116
[startup+720.265 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67590 0 0 0 71840 187 0 0 25 0 1 0 481060292 300285952 63573 4294967295 134512640 134672761 3221224544 3221223744 134561972 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.266 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67599 0 0 0 72839 188 0 0 25 0 1 0 481060292 300285952 63582 4294967295 134512640 134672761 3221224544 3221223740 134556584 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.267 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67602 0 0 0 73838 188 0 0 25 0 1 0 481060292 300285952 63585 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.271 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67603 0 0 0 74838 189 0 0 25 0 1 0 481060292 300285952 63586 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63586 603 41 0 73271 0
vsize: 293248
[startup+760.277 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67604 0 0 0 75839 189 0 0 25 0 1 0 481060292 300285952 63587 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63587 603 41 0 73271 0
vsize: 293248
[startup+770.277 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67606 0 0 0 76839 189 0 0 25 0 1 0 481060292 300285952 63589 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63589 603 41 0 73271 0
vsize: 293248
[startup+780.285 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67607 0 0 0 77840 189 0 0 25 0 1 0 481060292 300285952 63590 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63590 603 41 0 73271 0
vsize: 293248
[startup+790.286 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67608 0 0 0 78841 189 0 0 25 0 1 0 481060292 300285952 63591 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63591 603 41 0 73271 0
vsize: 293248
[startup+800.29 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67640 0 0 0 79841 189 0 0 25 0 1 0 481060292 300285952 63623 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63623 603 41 0 73271 0
vsize: 293248
[startup+810.29 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67641 0 0 0 80841 189 0 0 25 0 1 0 481060292 300285952 63624 4294967295 134512640 134672761 3221224544 3221223760 134561950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63624 603 41 0 73271 0
vsize: 293248
[startup+820.298 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67641 0 0 0 81842 189 0 0 25 0 1 0 481060292 300285952 63624 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73312 63624 603 41 0 73271 0
vsize: 293248
[startup+830.311 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67661 0 0 0 82844 189 0 0 25 0 1 0 481060292 300421120 63644 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73345 63644 603 41 0 73304 0
vsize: 293380
[startup+840.311 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67661 0 0 0 83844 189 0 0 25 0 1 0 481060292 300421120 63644 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73345 63644 603 41 0 73304 0
vsize: 293380
[startup+850.312 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67662 0 0 0 84844 189 0 0 25 0 1 0 481060292 300421120 63645 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73345 63645 603 41 0 73304 0
vsize: 293380
[startup+860.318 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67667 0 0 0 85845 189 0 0 25 0 1 0 481060292 300421120 63650 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73345 63650 603 41 0 73304 0
vsize: 293380
[startup+870.318 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67668 0 0 0 86845 189 0 0 25 0 1 0 481060292 300421120 63651 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73345 63651 603 41 0 73304 0
vsize: 293380
[startup+880.318 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67683 0 0 0 87845 189 0 0 25 0 1 0 481060292 300421120 63666 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73345 63666 603 41 0 73304 0
vsize: 293380
[startup+890.319 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67698 0 0 0 88845 189 0 0 25 0 1 0 481060292 300556288 63681 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63681 603 41 0 73337 0
vsize: 293512
[startup+900.328 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67702 0 0 0 89846 189 0 0 25 0 1 0 481060292 300556288 63685 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63685 603 41 0 73337 0
vsize: 293512
[startup+910.327 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67705 0 0 0 90846 189 0 0 25 0 1 0 481060292 300556288 63688 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63688 603 41 0 73337 0
vsize: 293512
[startup+920.328 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67705 0 0 0 91847 189 0 0 25 0 1 0 481060292 300556288 63688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63688 603 41 0 73337 0
vsize: 293512
[startup+930.333 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67705 0 0 0 92847 189 0 0 25 0 1 0 481060292 300556288 63688 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63688 603 41 0 73337 0
vsize: 293512
[startup+940.338 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67706 0 0 0 93848 189 0 0 25 0 1 0 481060292 300556288 63689 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+950.349 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67706 0 0 0 94849 189 0 0 25 0 1 0 481060292 300556288 63689 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+960.351 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67706 0 0 0 95850 189 0 0 25 0 1 0 481060292 300556288 63689 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+970.351 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67706 0 0 0 96850 189 0 0 25 0 1 0 481060292 300556288 63689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63689 603 41 0 73337 0
vsize: 293512
[startup+980.35 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67715 0 0 0 97850 189 0 0 25 0 1 0 481060292 300556288 63698 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63698 603 41 0 73337 0
vsize: 293512
[startup+990.356 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67723 0 0 0 98851 189 0 0 25 0 1 0 481060292 300556288 63706 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63706 603 41 0 73337 0
vsize: 293512
[startup+1000.36 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67726 0 0 0 99851 189 0 0 25 0 1 0 481060292 300556288 63709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73378 63709 603 41 0 73337 0
vsize: 293512
[startup+1010.36 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67728 0 0 0 100851 189 0 0 25 0 1 0 481060292 300691456 63711 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63711 603 41 0 73370 0
vsize: 293644
[startup+1020.36 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67730 0 0 0 101852 189 0 0 25 0 1 0 481060292 300691456 63713 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63713 603 41 0 73370 0
vsize: 293644
[startup+1030.37 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67732 0 0 0 102853 189 0 0 25 0 1 0 481060292 300691456 63715 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63715 603 41 0 73370 0
vsize: 293644
[startup+1040.37 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67742 0 0 0 103853 189 0 0 25 0 1 0 481060292 300691456 63725 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63725 603 41 0 73370 0
vsize: 293644
[startup+1050.37 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67745 0 0 0 104853 189 0 0 25 0 1 0 481060292 300691456 63728 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63728 603 41 0 73370 0
vsize: 293644
[startup+1060.37 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67745 0 0 0 105854 189 0 0 25 0 1 0 481060292 300691456 63728 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63728 603 41 0 73370 0
vsize: 293644
[startup+1070.39 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67752 0 0 0 106855 189 0 0 25 0 1 0 481060292 300691456 63735 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63735 603 41 0 73370 0
vsize: 293644
[startup+1080.39 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67753 0 0 0 107855 189 0 0 25 0 1 0 481060292 300691456 63736 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63736 603 41 0 73370 0
vsize: 293644
[startup+1090.39 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67756 0 0 0 108856 189 0 0 25 0 1 0 481060292 300691456 63739 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63739 603 41 0 73370 0
vsize: 293644
[startup+1100.39 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67756 0 0 0 109856 189 0 0 25 0 1 0 481060292 300691456 63739 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63739 603 41 0 73370 0
vsize: 293644
[startup+1110.39 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67757 0 0 0 110856 189 0 0 25 0 1 0 481060292 300691456 63740 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63740 603 41 0 73370 0
vsize: 293644
[startup+1120.39 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67757 0 0 0 111856 189 0 0 25 0 1 0 481060292 300691456 63740 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63740 603 41 0 73370 0
vsize: 293644
[startup+1130.4 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67759 0 0 0 112858 189 0 0 25 0 1 0 481060292 300691456 63742 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73411 63742 603 41 0 73370 0
vsize: 293644
[startup+1140.41 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67763 0 0 0 113859 189 0 0 25 0 1 0 481060292 300822528 63746 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73443 63746 603 41 0 73402 0
vsize: 293772
[startup+1150.41 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67763 0 0 0 114859 189 0 0 25 0 1 0 481060292 300822528 63746 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73443 63746 603 41 0 73402 0
vsize: 293772
[startup+1160.42 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67765 0 0 0 115860 189 0 0 25 0 1 0 481060292 300822528 63748 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73443 63748 603 41 0 73402 0
vsize: 293772
[startup+1170.42 s]
Raw data (loadavg): 1.06 0.98 0.69 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67765 0 0 0 116860 189 0 0 25 0 1 0 481060292 300822528 63748 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73443 63748 603 41 0 73402 0
vsize: 293772
[startup+1180.42 s]
Raw data (loadavg): 1.05 0.98 0.69 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67766 0 0 0 117860 189 0 0 25 0 1 0 481060292 300822528 63749 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73443 63749 603 41 0 73402 0
vsize: 293772
[startup+1190.43 s]
Raw data (loadavg): 1.04 0.98 0.70 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67767 0 0 0 118861 189 0 0 25 0 1 0 481060292 300822528 63750 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73443 63750 603 41 0 73402 0
vsize: 293772
[startup+1200.43 s]
Raw data (loadavg): 1.04 0.98 0.70 2/54 9089
Raw data (stat): 9089 (minisat+) R 9088 24215 24214 0 -1 0 67769 0 0 0 119861 189 0 0 25 0 1 0 481060292 300822528 63752 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73443 63752 603 41 0 73402 0
vsize: 293772
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.59 s]
Raw data (loadavg): 1.04 0.98 0.70 1/54 9089
Raw data (stat): 9089 (minisat+) Z 9088 24215 24214 0 -1 12 67771 0 0 0 119861 202 0 0 23 0 1 0 481060292 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.59
CPU time (s): 1200.64
CPU user time (s): 1198.62
CPU system time (s): 2.02469
CPU usage (%): 100.005
Max. virtual memory (Kb): 293772
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####