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 13816

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        667484 kB
Buffers:         32164 kB
Cached:         298232 kB
SwapCached:        628 kB
Active:          46180 kB
Inactive:       286444 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        667232 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            28876 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:12:09 (client local time) WITH STATUS 1 IN 409.98 SECONDS
stats: 20266 7 409.98 1
#### 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]---> BDD-cost: 3266
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]---> BDD-cost: 5975
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]---> BDD-cost: 2088
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]---> BDD-cost: 2333
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:  733
c ---[1302]---> BDD-cost:14325
c ---[1301]---> BDD-cost:26487
c ---[1300]---> BDD-cost: 9694
c ---[1296]---> BDD-cost:21513
c ---[1275]---> BDD-cost:18365
c ---[1253]---> BDD-cost:19611
c ---[1242]---> BDD-cost:48097
c ---[1214]---> BDD-cost:10350
c ---[1189]---> BDD-cost:   27
c ---[1184]---> BDD-cost:   27
c ---[1176]---> BDD-cost: 8498
c ---[1164]---> BDD-cost:28152
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:   23
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:   27
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]---> BDD-cost: 8974
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: 4654
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: 3439
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]---> BDD-cost:40125
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]---> BDD-cost:37359
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: 9412
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]---> BDD-cost: 8881
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]---> BDD-cost:11301
c ---[ 245]---> BDD-cost: 5002
c ---[ 244]---> BDD-cost: 2612
c ---[ 243]---> BDD-cost: 1538
c ---[ 242]---> BDD-cost: 1609
c ---[ 241]---> BDD-cost: 5452
c ---[ 240]---> BDD-cost: 7723
c ---[ 239]---> BDD-cost:  735
c ---[ 238]---> BDD-cost:  386
c ---[ 237]---> BDD-cost: 5541
c ---[ 236]---> BDD-cost: 1174
c ---[ 235]---> BDD-cost:29184
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]---> BDD-cost: 2359
c ---[ 226]---> BDD-cost: 9944
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: 1537
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:  883
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:  524
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]---> BDD-cost: 6583
c ---[ 131]---> BDD-cost: 4779
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: 2489
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: 3248
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]---> BDD-cost:10690
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]---> BDD-cost: 9350
c ---[  31]---> BDD-cost:27669
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]---> BDD-cost: 3994
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]---> BDD-cost:22531
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 | 1999785  6281497 |  666595       0        0     nan |  0.000 % |
c |       100 | 1999669  6281193 |  733254      58      186     3.2 |  0.148 % |
c |       250 | 1999669  6281193 |  806579     208     1004     4.8 |  0.148 % |
c |       477 | 1999549  6280857 |  887237     396     2372     6.0 |  0.152 % |
c |       814 | 1999150  6279660 |  975961     446     2352     5.3 |  0.167 % |
c |      1324 | 1998833  6278772 | 1073557     861    18534    21.5 |  0.178 % |
c |      2084 | 1998711  6278406 | 1180913    1568    37253    23.8 |  0.181 % |
c |      3224 | 1997229  6274014 | 1299005    2238    45344    20.3 |  0.237 % |
c |      4934 | 1996390  6271511 | 1428905    3082    52256    17.0 |  0.269 % |
c |      7497 | 1995776  6269673 | 1571796    4492    64087    14.3 |  0.291 % |
c |     11341 | 1993813  6263816 | 1728975    6485    68448    10.6 |  0.364 % |
ERROR! Too large constants encountered in constraint.
c ==============================================================================
c [1mFound solution: 290127003[0m
#### 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 23024
Raw data (stat): 23024 (runsolver) R 23023 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539901067 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 29444 0 0 0 926 73 0 0 25 0 1 0 539901067 108904448 24453 4294967295 134512640 134672761 3221224544 3220804128 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26588 24453 603 41 0 26547 0
vsize: 106352
[startup+20.0008 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 72317 0 0 0 1824 175 0 0 25 0 1 0 539901067 294551552 67326 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71912 67326 603 41 0 71871 0
vsize: 287648
[startup+30.0004 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 72834 0 0 0 2822 176 0 0 25 0 1 0 539901067 296579072 67843 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72407 67843 603 41 0 72366 0
vsize: 289628
[startup+40.001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 72969 0 0 0 3823 176 0 0 25 0 1 0 539901067 297119744 67978 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72539 67978 603 41 0 72498 0
vsize: 290156
[startup+50.0016 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 72969 0 0 0 4823 176 0 0 25 0 1 0 539901067 297119744 67978 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72539 67978 603 41 0 72498 0
vsize: 290156
[startup+60.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 73956 0 0 0 5821 178 0 0 25 0 1 0 539901067 301293568 68965 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73558 68965 603 41 0 73517 0
vsize: 294232
[startup+70.0041 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 73962 0 0 0 6821 178 0 0 25 0 1 0 539901067 301293568 68971 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73558 68971 603 41 0 73517 0
vsize: 294232
[startup+80.0045 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 74225 0 0 0 7821 178 0 0 25 0 1 0 539901067 302379008 69234 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73823 69234 603 41 0 73782 0
vsize: 295292
[startup+90.0041 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 74281 0 0 0 8821 179 0 0 25 0 1 0 539901067 302649344 69290 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73889 69290 603 41 0 73848 0
vsize: 295556
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 74508 0 0 0 9821 179 0 0 25 0 1 0 539901067 303325184 69517 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74054 69517 603 41 0 74013 0
vsize: 296216
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 74822 0 0 0 10820 180 0 0 25 0 1 0 539901067 304676864 69831 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74384 69831 603 41 0 74343 0
vsize: 297536
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 74968 0 0 0 11820 180 0 0 25 0 1 0 539901067 305217536 69977 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74516 69977 603 41 0 74475 0
vsize: 298064
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75040 0 0 0 12820 180 0 0 25 0 1 0 539901067 305487872 70049 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74582 70049 603 41 0 74541 0
vsize: 298328
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75149 0 0 0 13820 181 0 0 25 0 1 0 539901067 306028544 70158 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74714 70158 603 41 0 74673 0
vsize: 298856
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75220 0 0 0 14820 181 0 0 25 0 1 0 539901067 306298880 70229 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74780 70229 603 41 0 74739 0
vsize: 299120
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75231 0 0 0 15820 181 0 0 25 0 1 0 539901067 306298880 70240 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74780 70240 603 41 0 74739 0
vsize: 299120
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75240 0 0 0 16820 181 0 0 25 0 1 0 539901067 306450432 70249 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74817 70249 603 41 0 74776 0
vsize: 299268
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75402 0 0 0 17820 182 0 0 25 0 1 0 539901067 306991104 70411 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74949 70411 603 41 0 74908 0
vsize: 299796
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75590 0 0 0 18820 182 0 0 25 0 1 0 539901067 307802112 70599 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75147 70599 603 41 0 75106 0
vsize: 300588
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75594 0 0 0 19820 182 0 0 25 0 1 0 539901067 307802112 70603 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75147 70603 603 41 0 75106 0
vsize: 300588
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 75854 0 0 0 20820 182 0 0 25 0 1 0 539901067 308748288 70863 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75378 70863 603 41 0 75337 0
vsize: 301512
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76050 0 0 0 21820 183 0 0 25 0 1 0 539901067 309559296 71059 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75576 71059 603 41 0 75535 0
vsize: 302304
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76214 0 0 0 22820 183 0 0 25 0 1 0 539901067 310235136 71223 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75741 71223 603 41 0 75700 0
vsize: 302964
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76214 0 0 0 23820 183 0 0 25 0 1 0 539901067 310235136 71223 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75741 71223 603 41 0 75700 0
vsize: 302964
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76251 0 0 0 24821 183 0 0 25 0 1 0 539901067 310370304 71260 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75774 71260 603 41 0 75733 0
vsize: 303096
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76430 0 0 0 25820 184 0 0 25 0 1 0 539901067 311046144 71439 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75939 71439 603 41 0 75898 0
vsize: 303756
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76484 0 0 0 26820 184 0 0 25 0 1 0 539901067 311181312 71493 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75972 71493 603 41 0 75931 0
vsize: 303888
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76485 0 0 0 27821 184 0 0 25 0 1 0 539901067 311181312 71494 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75972 71494 603 41 0 75931 0
vsize: 303888
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76670 0 0 0 28820 184 0 0 25 0 1 0 539901067 311586816 71679 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76071 71679 603 41 0 76030 0
vsize: 304284
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 76963 0 0 0 29819 185 0 0 25 0 1 0 539901067 312397824 71972 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76269 71972 603 41 0 76228 0
vsize: 305076
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 77002 0 0 0 30819 186 0 0 25 0 1 0 539901067 312532992 72011 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76302 72011 603 41 0 76261 0
vsize: 305208
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 77096 0 0 0 31819 186 0 0 25 0 1 0 539901067 312803328 72105 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76368 72105 603 41 0 76327 0
vsize: 305472
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 77107 0 0 0 32819 186 0 0 25 0 1 0 539901067 312803328 72116 4294967295 134512640 134672761 3221224544 3221223716 134553588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76368 72116 603 41 0 76327 0
vsize: 305472
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 77288 0 0 0 33819 186 0 0 25 0 1 0 539901067 313344000 72297 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76500 72297 603 41 0 76459 0
vsize: 306000
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 77320 0 0 0 34819 186 0 0 25 0 1 0 539901067 313479168 72329 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76533 72329 603 41 0 76492 0
vsize: 306132
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 77401 0 0 0 35819 187 0 0 25 0 1 0 539901067 313749504 72410 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76599 72410 603 41 0 76558 0
vsize: 306396
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 77982 0 0 0 36817 188 0 0 25 0 1 0 539901067 315203584 72991 4294967295 134512640 134672761 3221224544 3221223780 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76954 72991 603 41 0 76913 0
vsize: 307816
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 78058 0 0 0 37817 188 0 0 25 0 1 0 539901067 315609088 73067 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77053 73067 603 41 0 77012 0
vsize: 308212
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 78089 0 0 0 38817 188 0 0 25 0 1 0 539901067 315744256 73098 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77086 73098 603 41 0 77045 0
vsize: 308344
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 78105 0 0 0 39818 188 0 0 25 0 1 0 539901067 315744256 73114 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77086 73114 603 41 0 77045 0
vsize: 308344
[startup+409.924 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 23024
Raw data (stat): 23024 (minisat+) R 23023 3260 3259 0 -1 0 78105 0 0 0 39818 188 0 0 25 0 1 0 539901067 315744256 73114 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77086 73114 603 41 0 77045 0
vsize: 0

Child status: 1
Real time (s): 409.923
CPU time (s): 409.98
CPU user time (s): 407.915
CPU system time (s): 2.06469
CPU usage (%): 100.014
Max. virtual memory (Kb): 308344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####