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 13278

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-20 20:23:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15254 boxname=wulflinc9 idbench=1174 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  9565d6b3010c78b37c39352cc9731cb7  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-sp98ar.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-sp98ar.opb
IDLAUNCH: 15254
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        831044 kB
Buffers:         34332 kB
Cached:         146744 kB
SwapCached:          8 kB
Active:          91532 kB
Inactive:        92340 kB
HighTotal:      131008 kB
HighFree:         8652 kB
LowTotal:       903652 kB
LowFree:        822392 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            14080 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 20:43:38 (client local time) WITH STATUS 0 IN 1200.66 SECONDS
stats: 15254 7 1200.66 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.15 0.03 0.01 2/54 26584
Raw data (stat): 26584 (runsolver) R 26583 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481069921 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0082 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 14260 0 0 0 963 36 0 0 25 0 1 0 481069921 56315904 11694 4294967295 134512640 134672761 3221224624 3221123616 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13749 11694 603 41 0 13708 0
vsize: 54996
[startup+20.0113 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 54100 0 0 0 1871 129 0 0 25 0 1 0 481069921 246210560 50066 4294967295 134512640 134672761 3221224624 3221220048 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60110 50066 603 41 0 60069 0
vsize: 240440
[startup+30.0111 s]
Raw data (loadavg): 0.48 0.12 0.04 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 56130 0 0 0 2863 134 0 0 25 0 1 0 481069921 254312448 52096 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62088 52096 603 41 0 62047 0
vsize: 248352
[startup+40.0108 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 57124 0 0 0 3861 136 0 0 25 0 1 0 481069921 258232320 53090 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63045 53090 603 41 0 63004 0
vsize: 252180
[startup+50.0115 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 57392 0 0 0 4861 136 0 0 25 0 1 0 481069921 259313664 53358 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63309 53358 603 41 0 63268 0
vsize: 253236
[startup+60.0112 s]
Raw data (loadavg): 0.69 0.20 0.07 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 57485 0 0 0 5861 137 0 0 25 0 1 0 481069921 259719168 53451 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63408 53451 603 41 0 63367 0
vsize: 253632
[startup+70.0113 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 57561 0 0 0 6860 137 0 0 25 0 1 0 481069921 260018176 53527 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63481 53527 603 41 0 63440 0
vsize: 253924
[startup+80.0116 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 57833 0 0 0 7860 138 0 0 25 0 1 0 481069921 261091328 53799 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63743 53799 603 41 0 63702 0
vsize: 254972
[startup+90.0223 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 57872 0 0 0 8861 138 0 0 25 0 1 0 481069921 261226496 53838 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63776 53838 603 41 0 63735 0
vsize: 255104
[startup+100.022 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58021 0 0 0 9859 139 0 0 25 0 1 0 481069921 261902336 53987 4294967295 134512640 134672761 3221224624 3221223808 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63941 53987 603 41 0 63900 0
vsize: 255764
[startup+110.022 s]
Raw data (loadavg): 0.86 0.33 0.11 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58111 0 0 0 10859 139 0 0 25 0 1 0 481069921 262172672 54077 4294967295 134512640 134672761 3221224624 3221223792 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64007 54077 603 41 0 63966 0
vsize: 256028
[startup+120.022 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58179 0 0 0 11859 139 0 0 25 0 1 0 481069921 262443008 54145 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64073 54145 603 41 0 64032 0
vsize: 256292
[startup+130.027 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58290 0 0 0 12859 140 0 0 25 0 1 0 481069921 262983680 54256 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64205 54256 603 41 0 64164 0
vsize: 256820
[startup+140.026 s]
Raw data (loadavg): 0.91 0.39 0.14 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58478 0 0 0 13859 141 0 0 25 0 1 0 481069921 263659520 54444 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64370 54444 603 41 0 64329 0
vsize: 257480
[startup+150.04 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58513 0 0 0 14860 141 0 0 25 0 1 0 481069921 263794688 54479 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64403 54479 603 41 0 64362 0
vsize: 257612
[startup+160.039 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58722 0 0 0 15860 141 0 0 25 0 1 0 481069921 264409088 54688 4294967295 134512640 134672761 3221224624 3221223788 134564515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64553 54688 603 41 0 64512 0
vsize: 258212
[startup+170.04 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58860 0 0 0 16860 142 0 0 25 0 1 0 481069921 265076736 54826 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64716 54826 603 41 0 64675 0
vsize: 258864
[startup+180.04 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58912 0 0 0 17859 142 0 0 25 0 1 0 481069921 265211904 54878 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64749 54878 603 41 0 64708 0
vsize: 258996
[startup+190.04 s]
Raw data (loadavg): 1.04 0.50 0.19 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58925 0 0 0 18859 142 0 0 25 0 1 0 481069921 265211904 54891 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64749 54891 603 41 0 64708 0
vsize: 258996
[startup+200.04 s]
Raw data (loadavg): 1.03 0.51 0.20 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58943 0 0 0 19860 142 0 0 25 0 1 0 481069921 265347072 54909 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64782 54909 603 41 0 64741 0
vsize: 259128
[startup+210.04 s]
Raw data (loadavg): 1.02 0.53 0.21 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58965 0 0 0 20860 142 0 0 25 0 1 0 481069921 265347072 54931 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64782 54931 603 41 0 64741 0
vsize: 259128
[startup+220.041 s]
Raw data (loadavg): 1.02 0.54 0.21 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 58999 0 0 0 21860 142 0 0 25 0 1 0 481069921 265482240 54965 4294967295 134512640 134672761 3221224624 3221223808 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64815 54965 603 41 0 64774 0
vsize: 259260
[startup+230.04 s]
Raw data (loadavg): 1.02 0.56 0.22 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59006 0 0 0 22860 142 0 0 25 0 1 0 481069921 265617408 54972 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64848 54972 603 41 0 64807 0
vsize: 259392
[startup+240.04 s]
Raw data (loadavg): 1.01 0.57 0.23 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59068 0 0 0 23860 142 0 0 25 0 1 0 481069921 265752576 55034 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64881 55034 603 41 0 64840 0
vsize: 259524
[startup+250.04 s]
Raw data (loadavg): 1.01 0.59 0.24 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59083 0 0 0 24860 142 0 0 25 0 1 0 481069921 265752576 55049 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64881 55049 603 41 0 64840 0
vsize: 259524
[startup+260.041 s]
Raw data (loadavg): 1.01 0.60 0.24 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59134 0 0 0 25860 143 0 0 25 0 1 0 481069921 266022912 55100 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64947 55100 603 41 0 64906 0
vsize: 259788
[startup+270.041 s]
Raw data (loadavg): 1.01 0.61 0.25 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59161 0 0 0 26860 143 0 0 25 0 1 0 481069921 266158080 55127 4294967295 134512640 134672761 3221224624 3221223812 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64980 55127 603 41 0 64939 0
vsize: 259920
[startup+280.041 s]
Raw data (loadavg): 1.01 0.62 0.26 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59171 0 0 0 27860 143 0 0 25 0 1 0 481069921 266158080 55137 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64980 55137 603 41 0 64939 0
vsize: 259920
[startup+290.044 s]
Raw data (loadavg): 1.00 0.64 0.27 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59228 0 0 0 28861 143 0 0 25 0 1 0 481069921 266293248 55194 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65013 55194 603 41 0 64972 0
vsize: 260052
[startup+300.043 s]
Raw data (loadavg): 1.00 0.65 0.28 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59239 0 0 0 29861 143 0 0 25 0 1 0 481069921 266293248 55205 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65013 55205 603 41 0 64972 0
vsize: 260052
[startup+310.043 s]
Raw data (loadavg): 1.00 0.66 0.28 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59260 0 0 0 30861 143 0 0 25 0 1 0 481069921 266428416 55226 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65046 55226 603 41 0 65005 0
vsize: 260184
[startup+320.044 s]
Raw data (loadavg): 1.00 0.67 0.29 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59276 0 0 0 31860 144 0 0 25 0 1 0 481069921 266428416 55242 4294967295 134512640 134672761 3221224624 3221223796 134556651 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.045 s]
Raw data (loadavg): 1.00 0.68 0.30 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59287 0 0 0 32860 144 0 0 25 0 1 0 481069921 266428416 55253 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65046 55253 603 41 0 65005 0
vsize: 260184
[startup+340.044 s]
Raw data (loadavg): 1.00 0.69 0.30 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59301 0 0 0 33860 144 0 0 25 0 1 0 481069921 266563584 55267 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65079 55267 603 41 0 65038 0
vsize: 260316
[startup+350.044 s]
Raw data (loadavg): 1.00 0.70 0.31 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59307 0 0 0 34861 144 0 0 25 0 1 0 481069921 266563584 55273 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65079 55273 603 41 0 65038 0
vsize: 260316
[startup+360.045 s]
Raw data (loadavg): 1.00 0.71 0.32 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59311 0 0 0 35861 144 0 0 25 0 1 0 481069921 266563584 55277 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65079 55277 603 41 0 65038 0
vsize: 260316
[startup+370.045 s]
Raw data (loadavg): 1.00 0.72 0.32 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59317 0 0 0 36861 144 0 0 25 0 1 0 481069921 266563584 55283 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65079 55283 603 41 0 65038 0
vsize: 260316
[startup+380.044 s]
Raw data (loadavg): 1.00 0.73 0.33 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59331 0 0 0 37861 144 0 0 25 0 1 0 481069921 266698752 55297 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65112 55297 603 41 0 65071 0
vsize: 260448
[startup+390.044 s]
Raw data (loadavg): 1.00 0.74 0.34 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59383 0 0 0 38861 144 0 0 25 0 1 0 481069921 266698752 55349 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65112 55349 603 41 0 65071 0
vsize: 260448
[startup+400.045 s]
Raw data (loadavg): 1.00 0.74 0.34 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59393 0 0 0 39861 144 0 0 25 0 1 0 481069921 266698752 55359 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65112 55359 603 41 0 65071 0
vsize: 260448
[startup+410.044 s]
Raw data (loadavg): 1.00 0.75 0.35 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59401 0 0 0 40861 144 0 0 25 0 1 0 481069921 266698752 55367 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65112 55367 603 41 0 65071 0
vsize: 260448
[startup+420.044 s]
Raw data (loadavg): 1.00 0.76 0.36 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59410 0 0 0 41861 144 0 0 25 0 1 0 481069921 266698752 55376 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65112 55376 603 41 0 65071 0
vsize: 260448
[startup+430.045 s]
Raw data (loadavg): 1.00 0.77 0.36 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59429 0 0 0 42861 144 0 0 25 0 1 0 481069921 266833920 55395 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65145 55395 603 41 0 65104 0
vsize: 260580
[startup+440.044 s]
Raw data (loadavg): 1.00 0.77 0.37 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59439 0 0 0 43861 144 0 0 25 0 1 0 481069921 266833920 55405 4294967295 134512640 134672761 3221224624 3221223792 134553610 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65145 55405 603 41 0 65104 0
vsize: 260580
[startup+450.044 s]
Raw data (loadavg): 1.00 0.78 0.38 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59514 0 0 0 44861 145 0 0 25 0 1 0 481069921 267231232 55480 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65242 55480 603 41 0 65201 0
vsize: 260968
[startup+460.044 s]
Raw data (loadavg): 1.00 0.79 0.38 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59514 0 0 0 45861 145 0 0 25 0 1 0 481069921 267231232 55480 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65242 55480 603 41 0 65201 0
vsize: 260968
[startup+470.044 s]
Raw data (loadavg): 1.00 0.79 0.39 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59515 0 0 0 46862 145 0 0 25 0 1 0 481069921 267231232 55481 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65242 55481 603 41 0 65201 0
vsize: 260968
[startup+480.044 s]
Raw data (loadavg): 1.00 0.80 0.39 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59534 0 0 0 47862 145 0 0 25 0 1 0 481069921 267231232 55500 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65242 55500 603 41 0 65201 0
vsize: 260968
[startup+490.044 s]
Raw data (loadavg): 1.00 0.81 0.40 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59546 0 0 0 48862 145 0 0 25 0 1 0 481069921 267231232 55512 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65242 55512 603 41 0 65201 0
vsize: 260968
[startup+500.045 s]
Raw data (loadavg): 1.00 0.81 0.41 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59553 0 0 0 49862 145 0 0 25 0 1 0 481069921 267366400 55519 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65275 55519 603 41 0 65234 0
vsize: 261100
[startup+510.044 s]
Raw data (loadavg): 1.00 0.82 0.41 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59571 0 0 0 50862 145 0 0 25 0 1 0 481069921 267366400 55537 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65275 55537 603 41 0 65234 0
vsize: 261100
[startup+520.044 s]
Raw data (loadavg): 1.00 0.82 0.42 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59573 0 0 0 51862 145 0 0 25 0 1 0 481069921 267366400 55539 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65275 55539 603 41 0 65234 0
vsize: 261100
[startup+530.045 s]
Raw data (loadavg): 1.00 0.83 0.42 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59577 0 0 0 52862 145 0 0 25 0 1 0 481069921 267366400 55543 4294967295 134512640 134672761 3221224624 3221223808 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65275 55543 603 41 0 65234 0
vsize: 261100
[startup+540.044 s]
Raw data (loadavg): 1.00 0.83 0.43 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59582 0 0 0 53862 145 0 0 25 0 1 0 481069921 267366400 55548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65275 55548 603 41 0 65234 0
vsize: 261100
[startup+550.044 s]
Raw data (loadavg): 1.00 0.84 0.43 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59590 0 0 0 54862 145 0 0 25 0 1 0 481069921 267366400 55556 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65275 55556 603 41 0 65234 0
vsize: 261100
[startup+560.045 s]
Raw data (loadavg): 1.00 0.84 0.44 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59604 0 0 0 55862 145 0 0 25 0 1 0 481069921 267501568 55570 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65308 55570 603 41 0 65267 0
vsize: 261232
[startup+570.045 s]
Raw data (loadavg): 1.00 0.85 0.45 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59616 0 0 0 56863 145 0 0 25 0 1 0 481069921 267501568 55582 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65308 55582 603 41 0 65267 0
vsize: 261232
[startup+580.044 s]
Raw data (loadavg): 1.00 0.85 0.45 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59625 0 0 0 57863 145 0 0 25 0 1 0 481069921 267501568 55591 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65308 55591 603 41 0 65267 0
vsize: 261232
[startup+590.044 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59630 0 0 0 58863 145 0 0 25 0 1 0 481069921 267636736 55596 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65341 55596 603 41 0 65300 0
vsize: 261364
[startup+600.049 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59643 0 0 0 59863 145 0 0 25 0 1 0 481069921 267636736 55609 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65341 55609 603 41 0 65300 0
vsize: 261364
[startup+610.049 s]
Raw data (loadavg): 1.00 0.86 0.47 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59660 0 0 0 60863 145 0 0 25 0 1 0 481069921 267636736 55626 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65341 55626 603 41 0 65300 0
vsize: 261364
[startup+620.049 s]
Raw data (loadavg): 1.00 0.87 0.47 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59666 0 0 0 61864 145 0 0 25 0 1 0 481069921 267771904 55632 4294967295 134512640 134672761 3221224624 3221223808 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65374 55632 603 41 0 65333 0
vsize: 261496
[startup+630.05 s]
Raw data (loadavg): 1.00 0.87 0.48 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59669 0 0 0 62864 145 0 0 25 0 1 0 481069921 267771904 55635 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65374 55635 603 41 0 65333 0
vsize: 261496
[startup+640.05 s]
Raw data (loadavg): 1.00 0.88 0.48 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59680 0 0 0 63864 145 0 0 25 0 1 0 481069921 267771904 55646 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65374 55646 603 41 0 65333 0
vsize: 261496
[startup+650.049 s]
Raw data (loadavg): 1.00 0.88 0.49 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59687 0 0 0 64864 145 0 0 25 0 1 0 481069921 267771904 55653 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65374 55653 603 41 0 65333 0
vsize: 261496
[startup+660.05 s]
Raw data (loadavg): 1.00 0.88 0.49 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59697 0 0 0 65864 146 0 0 25 0 1 0 481069921 267771904 55663 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65374 55663 603 41 0 65333 0
vsize: 261496
[startup+670.05 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59708 0 0 0 66864 146 0 0 25 0 1 0 481069921 267907072 55674 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65407 55674 603 41 0 65366 0
vsize: 261628
[startup+680.049 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59723 0 0 0 67864 146 0 0 25 0 1 0 481069921 267907072 55689 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65407 55689 603 41 0 65366 0
vsize: 261628
[startup+690.049 s]
Raw data (loadavg): 1.00 0.89 0.51 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59734 0 0 0 68865 146 0 0 25 0 1 0 481069921 268042240 55700 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65440 55700 603 41 0 65399 0
vsize: 261760
[startup+700.05 s]
Raw data (loadavg): 1.00 0.90 0.51 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59742 0 0 0 69865 146 0 0 25 0 1 0 481069921 268042240 55708 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65440 55708 603 41 0 65399 0
vsize: 261760
[startup+710.054 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59754 0 0 0 70865 146 0 0 25 0 1 0 481069921 268042240 55720 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65440 55720 603 41 0 65399 0
vsize: 261760
[startup+720.054 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59765 0 0 0 71866 146 0 0 25 0 1 0 481069921 268042240 55731 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65440 55731 603 41 0 65399 0
vsize: 261760
[startup+730.063 s]
Raw data (loadavg): 1.00 0.90 0.53 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59781 0 0 0 72867 146 0 0 25 0 1 0 481069921 268177408 55747 4294967295 134512640 134672761 3221224624 3221223840 134561994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65473 55747 603 41 0 65432 0
vsize: 261892
[startup+740.062 s]
Raw data (loadavg): 1.00 0.91 0.53 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59789 0 0 0 73866 146 0 0 25 0 1 0 481069921 268177408 55755 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65473 55755 603 41 0 65432 0
vsize: 261892
[startup+750.068 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59796 0 0 0 74867 146 0 0 25 0 1 0 481069921 268177408 55762 4294967295 134512640 134672761 3221224624 3221223748 134566125 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65473 55762 603 41 0 65432 0
vsize: 261892
[startup+760.068 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59801 0 0 0 75867 146 0 0 25 0 1 0 481069921 268177408 55767 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65473 55767 603 41 0 65432 0
vsize: 261892
[startup+770.076 s]
Raw data (loadavg): 1.00 0.91 0.55 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59807 0 0 0 76868 146 0 0 25 0 1 0 481069921 268312576 55773 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65506 55773 603 41 0 65465 0
vsize: 262024
[startup+780.076 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59820 0 0 0 77868 146 0 0 25 0 1 0 481069921 268312576 55786 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65506 55786 603 41 0 65465 0
vsize: 262024
[startup+790.083 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59827 0 0 0 78869 146 0 0 25 0 1 0 481069921 268312576 55793 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65506 55793 603 41 0 65465 0
vsize: 262024
[startup+800.09 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59835 0 0 0 79870 146 0 0 25 0 1 0 481069921 268312576 55801 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65506 55801 603 41 0 65465 0
vsize: 262024
[startup+810.095 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59867 0 0 0 80871 146 0 0 25 0 1 0 481069921 268312576 55833 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65506 55833 603 41 0 65465 0
vsize: 262024
[startup+820.095 s]
Raw data (loadavg): 1.00 0.92 0.57 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59883 0 0 0 81871 147 0 0 25 0 1 0 481069921 268447744 55849 4294967295 134512640 134672761 3221224624 3221223860 134564645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65539 55849 603 41 0 65498 0
vsize: 262156
[startup+830.095 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59892 0 0 0 82871 147 0 0 25 0 1 0 481069921 268447744 55858 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65539 55858 603 41 0 65498 0
vsize: 262156
[startup+840.098 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59903 0 0 0 83871 147 0 0 25 0 1 0 481069921 268447744 55869 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65539 55869 603 41 0 65498 0
vsize: 262156
[startup+850.099 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59913 0 0 0 84871 147 0 0 25 0 1 0 481069921 268582912 55879 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65572 55879 603 41 0 65531 0
vsize: 262288
[startup+860.099 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59921 0 0 0 85871 147 0 0 25 0 1 0 481069921 268582912 55887 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65572 55887 603 41 0 65531 0
vsize: 262288
[startup+870.099 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59927 0 0 0 86871 147 0 0 25 0 1 0 481069921 268582912 55893 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65572 55893 603 41 0 65531 0
vsize: 262288
[startup+880.099 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59939 0 0 0 87872 147 0 0 25 0 1 0 481069921 268582912 55905 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65572 55905 603 41 0 65531 0
vsize: 262288
[startup+890.102 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59950 0 0 0 88872 147 0 0 25 0 1 0 481069921 268718080 55916 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65605 55916 603 41 0 65564 0
vsize: 262420
[startup+900.102 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59956 0 0 0 89872 147 0 0 25 0 1 0 481069921 268718080 55922 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65605 55922 603 41 0 65564 0
vsize: 262420
[startup+910.103 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59969 0 0 0 90871 148 0 0 25 0 1 0 481069921 268718080 55935 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65605 55935 603 41 0 65564 0
vsize: 262420
[startup+920.104 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59979 0 0 0 91871 148 0 0 25 0 1 0 481069921 268718080 55945 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65605 55945 603 41 0 65564 0
vsize: 262420
[startup+930.103 s]
Raw data (loadavg): 1.00 0.94 0.61 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 59989 0 0 0 92871 148 0 0 25 0 1 0 481069921 268853248 55955 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65638 55955 603 41 0 65597 0
vsize: 262552
[startup+940.206 s]
Raw data (loadavg): 1.00 0.94 0.61 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60002 0 0 0 93882 148 0 0 25 0 1 0 481069921 268853248 55968 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65638 55968 603 41 0 65597 0
vsize: 262552
[startup+950.207 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60023 0 0 0 94882 148 0 0 25 0 1 0 481069921 268988416 55989 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65671 55989 603 41 0 65630 0
vsize: 262684
[startup+960.207 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60042 0 0 0 95882 148 0 0 25 0 1 0 481069921 268988416 56008 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65671 56008 603 41 0 65630 0
vsize: 262684
[startup+970.213 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60052 0 0 0 96883 148 0 0 25 0 1 0 481069921 268988416 56018 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65671 56018 603 41 0 65630 0
vsize: 262684
[startup+980.213 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60074 0 0 0 97883 148 0 0 25 0 1 0 481069921 269123584 56040 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65704 56040 603 41 0 65663 0
vsize: 262816
[startup+990.213 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60084 0 0 0 98883 148 0 0 25 0 1 0 481069921 269123584 56050 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65704 56050 603 41 0 65663 0
vsize: 262816
[startup+1000.22 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60099 0 0 0 99884 148 0 0 25 0 1 0 481069921 269123584 56065 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65704 56065 603 41 0 65663 0
vsize: 262816
[startup+1010.23 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60110 0 0 0 100885 148 0 0 25 0 1 0 481069921 269258752 56076 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65737 56076 603 41 0 65696 0
vsize: 262948
[startup+1020.23 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60122 0 0 0 101885 148 0 0 25 0 1 0 481069921 269258752 56088 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65737 56088 603 41 0 65696 0
vsize: 262948
[startup+1030.24 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60130 0 0 0 102886 148 0 0 25 0 1 0 481069921 269258752 56096 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65737 56096 603 41 0 65696 0
vsize: 262948
[startup+1040.24 s]
Raw data (loadavg): 1.00 0.95 0.65 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60132 0 0 0 103886 148 0 0 25 0 1 0 481069921 269258752 56098 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65737 56098 603 41 0 65696 0
vsize: 262948
[startup+1050.24 s]
Raw data (loadavg): 1.00 0.96 0.65 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60140 0 0 0 104886 148 0 0 25 0 1 0 481069921 269258752 56106 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65737 56106 603 41 0 65696 0
vsize: 262948
[startup+1060.24 s]
Raw data (loadavg): 1.00 0.96 0.65 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60152 0 0 0 105887 148 0 0 25 0 1 0 481069921 269656064 56118 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65834 56118 603 41 0 65793 0
vsize: 263336
[startup+1070.25 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60159 0 0 0 106887 148 0 0 25 0 1 0 481069921 269656064 56125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65834 56125 603 41 0 65793 0
vsize: 263336
[startup+1080.35 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60171 0 0 0 107898 148 0 0 25 0 1 0 481069921 269656064 56137 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65834 56137 603 41 0 65793 0
vsize: 263336
[startup+1090.37 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60184 0 0 0 108900 148 0 0 25 0 1 0 481069921 269791232 56150 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65867 56150 603 41 0 65826 0
vsize: 263468
[startup+1100.37 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60196 0 0 0 109900 148 0 0 25 0 1 0 481069921 269791232 56162 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65867 56162 603 41 0 65826 0
vsize: 263468
[startup+1110.38 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60239 0 0 0 110901 149 0 0 25 0 1 0 481069921 269926400 56205 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65900 56205 603 41 0 65859 0
vsize: 263600
[startup+1120.38 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60260 0 0 0 111901 149 0 0 25 0 1 0 481069921 270061568 56226 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65933 56226 603 41 0 65892 0
vsize: 263732
[startup+1130.38 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60277 0 0 0 112902 149 0 0 25 0 1 0 481069921 270061568 56243 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65933 56243 603 41 0 65892 0
vsize: 263732
[startup+1140.38 s]
Raw data (loadavg): 1.00 0.96 0.68 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60290 0 0 0 113902 149 0 0 25 0 1 0 481069921 270196736 56256 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65966 56256 603 41 0 65925 0
vsize: 263864
[startup+1150.38 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60315 0 0 0 114902 149 0 0 25 0 1 0 481069921 270196736 56281 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65966 56281 603 41 0 65925 0
vsize: 263864
[startup+1160.38 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60330 0 0 0 115902 149 0 0 25 0 1 0 481069921 270331904 56296 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65999 56296 603 41 0 65958 0
vsize: 263996
[startup+1170.38 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60348 0 0 0 116902 149 0 0 25 0 1 0 481069921 270331904 56314 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65999 56314 603 41 0 65958 0
vsize: 263996
[startup+1180.4 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60374 0 0 0 117904 149 0 0 25 0 1 0 481069921 270467072 56340 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66032 56340 603 41 0 65991 0
vsize: 264128
[startup+1190.4 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60381 0 0 0 118905 149 0 0 25 0 1 0 481069921 270467072 56347 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66032 56347 603 41 0 65991 0
vsize: 264128
[startup+1200.4 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 26584
Raw data (stat): 26584 (minisat+) R 26583 30854 30853 0 -1 0 60386 0 0 0 119905 149 0 0 25 0 1 0 481069921 270467072 56352 4294967295 134512640 134672761 3221224624 3221223792 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66032 56352 603 41 0 65991 0
vsize: 264128
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.52 s]
Raw data (loadavg): 1.00 0.97 0.69 1/54 26584
Raw data (stat): 26584 (minisat+) Z 26583 30854 30853 0 -1 12 60388 0 0 0 119905 160 0 0 25 0 1 0 481069921 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.52
CPU time (s): 1200.66
CPU user time (s): 1199.06
CPU system time (s): 1.60576
CPU usage (%): 100.012
Max. virtual memory (Kb): 264128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####