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 14257

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-20 23:20:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20259 boxname=wulflinc26 idbench=1559 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  9565d6b3010c78b37c39352cc9731cb7  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-sp98ar.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-sp98ar.opb
IDLAUNCH: 20259
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        471848 kB
Buffers:         37840 kB
Cached:         483652 kB
SwapCached:          0 kB
Active:         236444 kB
Inactive:       287944 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        471596 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6964 kB
Slab:            32748 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:40:49 (client local time) WITH STATUS 0 IN 1200.39 SECONDS
stats: 20259 7 1200.39 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 | 1777845  6002235 |  592615       0        0     nan |  0.000 % |
c |       101 | 1777845  6002235 |  651876     101      459     4.5 |  0.218 % |
c |       251 | 1777845  6002235 |  717064     251     1530     6.1 |  0.218 % |
c |       476 | 1777835  6002207 |  788770     472     2460     5.2 |  0.218 % |
c |       813 | 1777835  6002207 |  867647     809     4480     5.5 |  0.218 % |
c |      1319 | 1777785  6002061 |  954412    1295     6907     5.3 |  0.221 % |
c |      2078 | 1777777  6002037 | 1049853    2047    11034     5.4 |  0.221 % |
c |      3217 | 1777626  6001604 | 1154838    3079    18141     5.9 |  0.228 % |
c |      4925 | 1777470  6001146 | 1270322    4743    29622     6.2 |  0.235 % |
c |      7487 | 1777250  6000416 | 1397355    7259    47300     6.5 |  0.240 % |
c |     11331 | 1777240  6000386 | 1537090   11099   149202    13.4 |  0.241 % |
c |     17097 | 1776649  5998585 | 1690799   16738   208091    12.4 |  0.263 % |
c |     25746 | 1775548  5995152 | 1859879   25098   277850    11.1 |  0.305 % |
c |     38720 | 1773964  5990312 | 2045867   37044   375587    10.1 |  0.376 % |
c |     58182 | 1772211  5984665 | 2250454   55726   533174     9.6 |  0.436 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.86 0.97 0.91 2/54 19820
Raw data (stat): 19820 (runsolver) R 19819 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540359487 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 14260 0 0 0 960 39 0 0 25 0 1 0 540359487 56315904 11694 4294967295 134512640 134672761 3221224624 3221184576 134523140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13749 11694 603 41 0 13708 0
vsize: 54996
[startup+20.0014 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 54257 0 0 0 1859 140 0 0 25 0 1 0 540359487 246751232 50223 4294967295 134512640 134672761 3221224624 3221220120 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60242 50223 603 41 0 60201 0
vsize: 240968
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 56130 0 0 0 2853 145 0 0 25 0 1 0 540359487 254312448 52096 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62088 52096 603 41 0 62047 0
vsize: 248352
[startup+40.0025 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 57124 0 0 0 3852 147 0 0 25 0 1 0 540359487 258232320 53090 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63045 53090 603 41 0 63004 0
vsize: 252180
[startup+50.0031 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 57391 0 0 0 4851 148 0 0 25 0 1 0 540359487 259313664 53357 4294967295 134512640 134672761 3221224624 3221223812 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63309 53357 603 41 0 63268 0
vsize: 253236
[startup+60.0028 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 57485 0 0 0 5851 148 0 0 25 0 1 0 540359487 259719168 53451 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63408 53451 603 41 0 63367 0
vsize: 253632
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 57560 0 0 0 6851 148 0 0 25 0 1 0 540359487 260018176 53526 4294967295 134512640 134672761 3221224624 3221223748 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63481 53526 603 41 0 63440 0
vsize: 253924
[startup+80.0045 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 57833 0 0 0 7850 149 0 0 25 0 1 0 540359487 261091328 53799 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63743 53799 603 41 0 63702 0
vsize: 254972
[startup+90.0049 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 57872 0 0 0 8850 150 0 0 25 0 1 0 540359487 261226496 53838 4294967295 134512640 134672761 3221224624 3221223748 134566151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63776 53838 603 41 0 63735 0
vsize: 255104
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58007 0 0 0 9849 151 0 0 25 0 1 0 540359487 261767168 53973 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63908 53973 603 41 0 63867 0
vsize: 255632
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58110 0 0 0 10848 152 0 0 25 0 1 0 540359487 262172672 54076 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64007 54076 603 41 0 63966 0
vsize: 256028
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58179 0 0 0 11848 152 0 0 25 0 1 0 540359487 262443008 54145 4294967295 134512640 134672761 3221224624 3221223816 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64073 54145 603 41 0 64032 0
vsize: 256292
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58265 0 0 0 12848 153 0 0 25 0 1 0 540359487 262848512 54231 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64172 54231 603 41 0 64131 0
vsize: 256688
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58478 0 0 0 13847 154 0 0 25 0 1 0 540359487 263659520 54444 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64370 54444 603 41 0 64329 0
vsize: 257480
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58513 0 0 0 14846 155 0 0 25 0 1 0 540359487 263794688 54479 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64403 54479 603 41 0 64362 0
vsize: 257612
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58722 0 0 0 15846 155 0 0 25 0 1 0 540359487 264409088 54688 4294967295 134512640 134672761 3221224624 3221223748 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64553 54688 603 41 0 64512 0
vsize: 258212
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58853 0 0 0 16845 156 0 0 25 0 1 0 540359487 264941568 54819 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64683 54819 603 41 0 64642 0
vsize: 258732
[startup+180.007 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58911 0 0 0 17845 156 0 0 25 0 1 0 540359487 265211904 54877 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64749 54877 603 41 0 64708 0
vsize: 258996
[startup+190.008 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58925 0 0 0 18845 156 0 0 25 0 1 0 540359487 265211904 54891 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64749 54891 603 41 0 64708 0
vsize: 258996
[startup+200.008 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58943 0 0 0 19845 157 0 0 25 0 1 0 540359487 265347072 54909 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64782 54909 603 41 0 64741 0
vsize: 259128
[startup+210.007 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58965 0 0 0 20845 157 0 0 25 0 1 0 540359487 265347072 54931 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64782 54931 603 41 0 64741 0
vsize: 259128
[startup+220.008 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 58999 0 0 0 21845 157 0 0 25 0 1 0 540359487 265482240 54965 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64815 54965 603 41 0 64774 0
vsize: 259260
[startup+230.007 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59005 0 0 0 22845 157 0 0 25 0 1 0 540359487 265617408 54971 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64848 54971 603 41 0 64807 0
vsize: 259392
[startup+240.008 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59068 0 0 0 23844 158 0 0 25 0 1 0 540359487 265752576 55034 4294967295 134512640 134672761 3221224624 3221223792 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64881 55034 603 41 0 64840 0
vsize: 259524
[startup+250.009 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59083 0 0 0 24844 158 0 0 25 0 1 0 540359487 265752576 55049 4294967295 134512640 134672761 3221224624 3221223788 134564531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64881 55049 603 41 0 64840 0
vsize: 259524
[startup+260.031 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59129 0 0 0 25846 159 0 0 25 0 1 0 540359487 266022912 55095 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64947 55095 603 41 0 64906 0
vsize: 259788
[startup+270.031 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59161 0 0 0 26846 159 0 0 25 0 1 0 540359487 266158080 55127 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64980 55127 603 41 0 64939 0
vsize: 259920
[startup+280.031 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59171 0 0 0 27846 159 0 0 25 0 1 0 540359487 266158080 55137 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64980 55137 603 41 0 64939 0
vsize: 259920
[startup+290.032 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59226 0 0 0 28845 160 0 0 25 0 1 0 540359487 266293248 55192 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65013 55192 603 41 0 64972 0
vsize: 260052
[startup+300.031 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59239 0 0 0 29845 160 0 0 25 0 1 0 540359487 266293248 55205 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65013 55205 603 41 0 64972 0
vsize: 260052
[startup+310.031 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59259 0 0 0 30845 160 0 0 25 0 1 0 540359487 266428416 55225 4294967295 134512640 134672761 3221224624 3221223776 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65046 55225 603 41 0 65005 0
vsize: 260184
[startup+320.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59276 0 0 0 31845 161 0 0 25 0 1 0 540359487 266428416 55242 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65046 55242 603 41 0 65005 0
vsize: 260184
[startup+330.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59286 0 0 0 32845 161 0 0 25 0 1 0 540359487 266428416 55252 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65046 55252 603 41 0 65005 0
vsize: 260184
[startup+340.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59300 0 0 0 33844 162 0 0 25 0 1 0 540359487 266563584 55266 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65079 55266 603 41 0 65038 0
vsize: 260316
[startup+350.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59306 0 0 0 34844 162 0 0 25 0 1 0 540359487 266563584 55272 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65079 55272 603 41 0 65038 0
vsize: 260316
[startup+360.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59311 0 0 0 35845 162 0 0 25 0 1 0 540359487 266563584 55277 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65079 55277 603 41 0 65038 0
vsize: 260316
[startup+370.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59316 0 0 0 36845 162 0 0 25 0 1 0 540359487 266563584 55282 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65079 55282 603 41 0 65038 0
vsize: 260316
[startup+380.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59329 0 0 0 37844 163 0 0 25 0 1 0 540359487 266698752 55295 4294967295 134512640 134672761 3221224624 3221223748 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65112 55295 603 41 0 65071 0
vsize: 260448
[startup+390.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59383 0 0 0 38844 163 0 0 25 0 1 0 540359487 266698752 55349 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65112 55349 603 41 0 65071 0
vsize: 260448
[startup+400.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59391 0 0 0 39844 163 0 0 25 0 1 0 540359487 266698752 55357 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65112 55357 603 41 0 65071 0
vsize: 260448
[startup+410.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59401 0 0 0 40844 164 0 0 25 0 1 0 540359487 266698752 55367 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65112 55367 603 41 0 65071 0
vsize: 260448
[startup+420.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59407 0 0 0 41844 164 0 0 25 0 1 0 540359487 266698752 55373 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65112 55373 603 41 0 65071 0
vsize: 260448
[startup+430.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59426 0 0 0 42844 164 0 0 25 0 1 0 540359487 266833920 55392 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65145 55392 603 41 0 65104 0
vsize: 260580
[startup+440.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59439 0 0 0 43844 165 0 0 25 0 1 0 540359487 266833920 55405 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65145 55405 603 41 0 65104 0
vsize: 260580
[startup+450.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59514 0 0 0 44843 165 0 0 25 0 1 0 540359487 267231232 55480 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65242 55480 603 41 0 65201 0
vsize: 260968
[startup+460.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59514 0 0 0 45843 166 0 0 25 0 1 0 540359487 267231232 55480 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65242 55480 603 41 0 65201 0
vsize: 260968
[startup+470.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59515 0 0 0 46843 166 0 0 25 0 1 0 540359487 267231232 55481 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65242 55481 603 41 0 65201 0
vsize: 260968
[startup+480.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59534 0 0 0 47842 167 0 0 25 0 1 0 540359487 267231232 55500 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65242 55500 603 41 0 65201 0
vsize: 260968
[startup+490.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59544 0 0 0 48842 167 0 0 25 0 1 0 540359487 267231232 55510 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65242 55510 603 41 0 65201 0
vsize: 260968
[startup+500.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59552 0 0 0 49842 167 0 0 25 0 1 0 540359487 267366400 55518 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65275 55518 603 41 0 65234 0
vsize: 261100
[startup+510.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59570 0 0 0 50842 168 0 0 25 0 1 0 540359487 267366400 55536 4294967295 134512640 134672761 3221224624 3221223832 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65275 55536 603 41 0 65234 0
vsize: 261100
[startup+520.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59572 0 0 0 51842 168 0 0 25 0 1 0 540359487 267366400 55538 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65275 55538 603 41 0 65234 0
vsize: 261100
[startup+530.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59577 0 0 0 52842 169 0 0 25 0 1 0 540359487 267366400 55543 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65275 55543 603 41 0 65234 0
vsize: 261100
[startup+540.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59582 0 0 0 53842 169 0 0 25 0 1 0 540359487 267366400 55548 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65275 55548 603 41 0 65234 0
vsize: 261100
[startup+550.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59590 0 0 0 54841 169 0 0 25 0 1 0 540359487 267366400 55556 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65275 55556 603 41 0 65234 0
vsize: 261100
[startup+560.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59602 0 0 0 55841 169 0 0 25 0 1 0 540359487 267501568 55568 4294967295 134512640 134672761 3221224624 3221223792 134564577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65308 55568 603 41 0 65267 0
vsize: 261232
[startup+570.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59615 0 0 0 56841 170 0 0 25 0 1 0 540359487 267501568 55581 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65308 55581 603 41 0 65267 0
vsize: 261232
[startup+580.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59624 0 0 0 57841 170 0 0 25 0 1 0 540359487 267501568 55590 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65308 55590 603 41 0 65267 0
vsize: 261232
[startup+590.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59629 0 0 0 58841 170 0 0 25 0 1 0 540359487 267636736 55595 4294967295 134512640 134672761 3221224624 3221223796 134556658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65341 55595 603 41 0 65300 0
vsize: 261364
[startup+600.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59642 0 0 0 59841 171 0 0 25 0 1 0 540359487 267636736 55608 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65341 55608 603 41 0 65300 0
vsize: 261364
[startup+610.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59657 0 0 0 60840 171 0 0 25 0 1 0 540359487 267636736 55623 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65341 55623 603 41 0 65300 0
vsize: 261364
[startup+620.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59665 0 0 0 61840 171 0 0 25 0 1 0 540359487 267771904 55631 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65374 55631 603 41 0 65333 0
vsize: 261496
[startup+630.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59667 0 0 0 62840 172 0 0 25 0 1 0 540359487 267771904 55633 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65374 55633 603 41 0 65333 0
vsize: 261496
[startup+640.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59679 0 0 0 63840 172 0 0 25 0 1 0 540359487 267771904 55645 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65374 55645 603 41 0 65333 0
vsize: 261496
[startup+650.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59685 0 0 0 64840 172 0 0 25 0 1 0 540359487 267771904 55651 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65374 55651 603 41 0 65333 0
vsize: 261496
[startup+660.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59696 0 0 0 65840 172 0 0 25 0 1 0 540359487 267771904 55662 4294967295 134512640 134672761 3221224624 3221223792 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65374 55662 603 41 0 65333 0
vsize: 261496
[startup+670.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59708 0 0 0 66840 173 0 0 25 0 1 0 540359487 267907072 55674 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65407 55674 603 41 0 65366 0
vsize: 261628
[startup+680.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59720 0 0 0 67839 173 0 0 25 0 1 0 540359487 267907072 55686 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65407 55686 603 41 0 65366 0
vsize: 261628
[startup+690.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59733 0 0 0 68839 174 0 0 25 0 1 0 540359487 268042240 55699 4294967295 134512640 134672761 3221224624 3221223792 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65440 55699 603 41 0 65399 0
vsize: 261760
[startup+700.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59740 0 0 0 69839 174 0 0 25 0 1 0 540359487 268042240 55706 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65440 55706 603 41 0 65399 0
vsize: 261760
[startup+710.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59751 0 0 0 70838 175 0 0 25 0 1 0 540359487 268042240 55717 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65440 55717 603 41 0 65399 0
vsize: 261760
[startup+720.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59764 0 0 0 71838 175 0 0 25 0 1 0 540359487 268042240 55730 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65440 55730 603 41 0 65399 0
vsize: 261760
[startup+730.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59780 0 0 0 72838 175 0 0 25 0 1 0 540359487 268177408 55746 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65473 55746 603 41 0 65432 0
vsize: 261892
[startup+740.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59787 0 0 0 73838 176 0 0 25 0 1 0 540359487 268177408 55753 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65473 55753 603 41 0 65432 0
vsize: 261892
[startup+750.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59795 0 0 0 74838 176 0 0 25 0 1 0 540359487 268177408 55761 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65473 55761 603 41 0 65432 0
vsize: 261892
[startup+760.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59801 0 0 0 75838 176 0 0 25 0 1 0 540359487 268177408 55767 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65473 55767 603 41 0 65432 0
vsize: 261892
[startup+770.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59807 0 0 0 76838 177 0 0 25 0 1 0 540359487 268312576 55773 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65506 55773 603 41 0 65465 0
vsize: 262024
[startup+780.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59820 0 0 0 77837 177 0 0 25 0 1 0 540359487 268312576 55786 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65506 55786 603 41 0 65465 0
vsize: 262024
[startup+790.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59825 0 0 0 78837 177 0 0 25 0 1 0 540359487 268312576 55791 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65506 55791 603 41 0 65465 0
vsize: 262024
[startup+800.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59835 0 0 0 79837 177 0 0 25 0 1 0 540359487 268312576 55801 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65506 55801 603 41 0 65465 0
vsize: 262024
[startup+810.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59865 0 0 0 80837 178 0 0 25 0 1 0 540359487 268312576 55831 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65506 55831 603 41 0 65465 0
vsize: 262024
[startup+820.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59877 0 0 0 81837 178 0 0 25 0 1 0 540359487 268447744 55843 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65539 55843 603 41 0 65498 0
vsize: 262156
[startup+830.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59891 0 0 0 82837 178 0 0 25 0 1 0 540359487 268447744 55857 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65539 55857 603 41 0 65498 0
vsize: 262156
[startup+840.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59902 0 0 0 83837 178 0 0 25 0 1 0 540359487 268447744 55868 4294967295 134512640 134672761 3221224624 3221223748 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65539 55868 603 41 0 65498 0
vsize: 262156
[startup+850.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59908 0 0 0 84837 179 0 0 25 0 1 0 540359487 268582912 55874 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65572 55874 603 41 0 65531 0
vsize: 262288
[startup+860.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59920 0 0 0 85837 179 0 0 25 0 1 0 540359487 268582912 55886 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65572 55886 603 41 0 65531 0
vsize: 262288
[startup+870.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59926 0 0 0 86837 179 0 0 25 0 1 0 540359487 268582912 55892 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65572 55892 603 41 0 65531 0
vsize: 262288
[startup+880.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59937 0 0 0 87837 180 0 0 25 0 1 0 540359487 268582912 55903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65572 55903 603 41 0 65531 0
vsize: 262288
[startup+890.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59947 0 0 0 88837 180 0 0 25 0 1 0 540359487 268582912 55913 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65572 55913 603 41 0 65531 0
vsize: 262288
[startup+900.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59955 0 0 0 89836 180 0 0 25 0 1 0 540359487 268718080 55921 4294967295 134512640 134672761 3221224624 3221223792 134553616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65605 55921 603 41 0 65564 0
vsize: 262420
[startup+910.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59963 0 0 0 90836 180 0 0 25 0 1 0 540359487 268718080 55929 4294967295 134512640 134672761 3221224624 3221223776 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65605 55929 603 41 0 65564 0
vsize: 262420
[startup+920.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59977 0 0 0 91836 181 0 0 25 0 1 0 540359487 268718080 55943 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65605 55943 603 41 0 65564 0
vsize: 262420
[startup+930.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 59986 0 0 0 92836 181 0 0 25 0 1 0 540359487 268853248 55952 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65638 55952 603 41 0 65597 0
vsize: 262552
[startup+940.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60001 0 0 0 93836 181 0 0 25 0 1 0 540359487 268853248 55967 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65638 55967 603 41 0 65597 0
vsize: 262552
[startup+950.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60020 0 0 0 94836 182 0 0 25 0 1 0 540359487 268853248 55986 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65638 55986 603 41 0 65597 0
vsize: 262552
[startup+960.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60032 0 0 0 95837 182 0 0 25 0 1 0 540359487 268988416 55998 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65671 55998 603 41 0 65630 0
vsize: 262684
[startup+970.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60052 0 0 0 96837 183 0 0 25 0 1 0 540359487 268988416 56018 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65671 56018 603 41 0 65630 0
vsize: 262684
[startup+980.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60059 0 0 0 97837 183 0 0 25 0 1 0 540359487 269123584 56025 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65704 56025 603 41 0 65663 0
vsize: 262816
[startup+990.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60082 0 0 0 98837 184 0 0 25 0 1 0 540359487 269123584 56048 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65704 56048 603 41 0 65663 0
vsize: 262816
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60093 0 0 0 99836 184 0 0 25 0 1 0 540359487 269123584 56059 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65704 56059 603 41 0 65663 0
vsize: 262816
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60108 0 0 0 100836 185 0 0 25 0 1 0 540359487 269258752 56074 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65737 56074 603 41 0 65696 0
vsize: 262948
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60118 0 0 0 101836 185 0 0 25 0 1 0 540359487 269258752 56084 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65737 56084 603 41 0 65696 0
vsize: 262948
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60128 0 0 0 102836 185 0 0 25 0 1 0 540359487 269258752 56094 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65737 56094 603 41 0 65696 0
vsize: 262948
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60131 0 0 0 103836 185 0 0 25 0 1 0 540359487 269258752 56097 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65737 56097 603 41 0 65696 0
vsize: 262948
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60138 0 0 0 104836 185 0 0 25 0 1 0 540359487 269258752 56104 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65737 56104 603 41 0 65696 0
vsize: 262948
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60147 0 0 0 105836 186 0 0 25 0 1 0 540359487 269393920 56113 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65770 56113 603 41 0 65729 0
vsize: 263080
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60158 0 0 0 106836 186 0 0 25 0 1 0 540359487 269656064 56124 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65834 56124 603 41 0 65793 0
vsize: 263336
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60169 0 0 0 107836 186 0 0 25 0 1 0 540359487 269656064 56135 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65834 56135 603 41 0 65793 0
vsize: 263336
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60179 0 0 0 108836 186 0 0 25 0 1 0 540359487 269791232 56145 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65867 56145 603 41 0 65826 0
vsize: 263468
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60191 0 0 0 109835 187 0 0 25 0 1 0 540359487 269791232 56157 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65867 56157 603 41 0 65826 0
vsize: 263468
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60228 0 0 0 110835 188 0 0 25 0 1 0 540359487 269926400 56194 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65900 56194 603 41 0 65859 0
vsize: 263600
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60256 0 0 0 111835 188 0 0 25 0 1 0 540359487 270061568 56222 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65933 56222 603 41 0 65892 0
vsize: 263732
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60273 0 0 0 112835 188 0 0 25 0 1 0 540359487 270061568 56239 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65933 56239 603 41 0 65892 0
vsize: 263732
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60284 0 0 0 113834 189 0 0 25 0 1 0 540359487 270196736 56250 4294967295 134512640 134672761 3221224624 3221223824 134557959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65966 56250 603 41 0 65925 0
vsize: 263864
[startup+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60309 0 0 0 114834 189 0 0 25 0 1 0 540359487 270196736 56275 4294967295 134512640 134672761 3221224624 3221223760 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65966 56275 603 41 0 65925 0
vsize: 263864
[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60324 0 0 0 115834 190 0 0 25 0 1 0 540359487 270331904 56290 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65999 56290 603 41 0 65958 0
vsize: 263996
[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60345 0 0 0 116834 190 0 0 25 0 1 0 540359487 270331904 56311 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65999 56311 603 41 0 65958 0
vsize: 263996
[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60369 0 0 0 117833 191 0 0 25 0 1 0 540359487 270467072 56335 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66032 56335 603 41 0 65991 0
vsize: 264128
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60380 0 0 0 118834 192 0 0 25 0 1 0 540359487 270467072 56346 4294967295 134512640 134672761 3221224624 3221223808 134557994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66032 56346 603 41 0 65991 0
vsize: 264128
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 19820
Raw data (stat): 19820 (minisat+) R 19819 22612 22611 0 -1 0 60386 0 0 0 119835 192 0 0 25 0 1 0 540359487 270467072 56352 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66032 56352 603 41 0 65991 0
vsize: 264128
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 19820
Raw data (stat): 19820 (minisat+) Z 19819 22612 22611 0 -1 12 60388 0 0 0 119835 203 0 0 25 0 1 0 540359487 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.22
CPU time (s): 1200.39
CPU user time (s): 1198.36
CPU system time (s): 2.03469
CPU usage (%): 100.015
Max. virtual memory (Kb): 264128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####