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-berlin_5_8_0.opb
MD5SUM	96d7d5bfca5320061ed7cb61443916ee
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	7936
Optimality of the best value was proved	NO
Number of terms in the objective function	68
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1054719
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	128000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	268497406
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.04
Number of variables	8590
Total number of constraints	2614
Number of constraints which are clauses	309
Number of constraints which are cardinality constraints (but not clauses)	794
Number of constraints which are nor clauses,nor cardinality constraints	1511
Minimum length of a constraint	1
Maximum length of a constraint	55
Trace number 31323

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-05-26 00:08:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22717 boxname=wulflinc11 idbench=1533 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  96d7d5bfca5320061ed7cb61443916ee  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-berlin_5_8_0.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-berlin_5_8_0.opb
IDLAUNCH: 22717
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        838428 kB
Buffers:          6720 kB
Cached:         169920 kB
SwapCached:        908 kB
Active:          28352 kB
Inactive:       150388 kB
HighTotal:      131008 kB
HighFree:        11200 kB
LowTotal:       903652 kB
LowFree:        827228 kB
SwapTotal:     2097136 kB
SwapFree:      2095388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5032 kB
Slab:            11728 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:29:11 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22717 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1821 PB-constraints to clauses...
c   -- Unit propagations: pppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.....................................................................................................................................................................................................................................................................................................................
c ---[1815]---> BDD-cost:  113
c ---[1814]---> BDD-cost:  140
c ---[1813]---> BDD-cost:  118
c ---[1812]---> BDD-cost:  130
c ---[1811]---> BDD-cost:  122
c ---[1810]---> BDD-cost:  137
c ---[1809]---> BDD-cost:  125
c ---[1808]---> BDD-cost:  124
c ---[1807]---> BDD-cost:  128
c ---[1806]---> BDD-cost:  140
c ---[1804]---> BDD-cost:  128
c ---[1803]---> BDD-cost:  134
c ---[1802]---> BDD-cost:  128
c ---[1801]---> BDD-cost:  127
c ---[1800]---> BDD-cost:  128
c ---[1799]---> BDD-cost:  140
c ---[1798]---> BDD-cost:  128
c ---[1797]---> BDD-cost:  140
c ---[1796]---> BDD-cost:  120
c ---[1795]---> BDD-cost:  140
c ---[1793]---> BDD-cost:  128
c ---[1792]---> BDD-cost:  135
c ---[1791]---> BDD-cost:  113
c ---[1790]---> BDD-cost:  123
c ---[1789]---> BDD-cost:  120
c ---[1788]---> BDD-cost:  140
c ---[1787]---> BDD-cost:  128
c ---[1786]---> BDD-cost:  135
c ---[1785]---> BDD-cost:  128
c ---[1784]---> BDD-cost:  131
c ---[1782]---> BDD-cost:  131
c ---[1781]---> BDD-cost:  131
c ---[1780]---> BDD-cost:  105
c ---[1779]---> BDD-cost:  105
c ---[1778]---> BDD-cost:  131
c ---[1777]---> BDD-cost:  131
c ---[1776]---> BDD-cost:  140
c ---[1775]---> BDD-cost:  140
c ---[1774]---> BDD-cost:  128
c ---[1773]---> BDD-cost:  105
c ---[1771]---> BDD-cost:  128
c ---[1770]---> BDD-cost:  132
c ---[1769]---> BDD-cost:  113
c ---[1768]---> BDD-cost:  132
c ---[1767]---> BDD-cost:  128
c ---[1766]---> BDD-cost:  137
c ---[1765]---> BDD-cost:  113
c ---[1764]---> BDD-cost:  140
c ---[1763]---> BDD-cost:  115
c ---[1762]---> BDD-cost:  137
c ---[1760]---> BDD-cost:  128
c ---[1759]---> BDD-cost:  135
c ---[1758]---> BDD-cost:  122
c ---[1757]---> BDD-cost:  134
c ---[1756]---> BDD-cost:  128
c ---[1755]---> BDD-cost:  135
c ---[1754]---> BDD-cost:  123
c ---[1753]---> BDD-cost:  140
c ---[1752]---> BDD-cost:  118
c ---[1751]---> BDD-cost:  132
c ---[1749]---> BDD-cost:  113
c ---[1748]---> BDD-cost:  137
c ---[1747]---> BDD-cost:  128
c ---[1746]---> BDD-cost:  134
c ---[1745]---> BDD-cost:  113
c ---[1744]---> BDD-cost:  119
c ---[1743]---> BDD-cost:  122
c ---[1742]---> BDD-cost:  127
c ---[1741]---> BDD-cost:  123
c ---[1740]---> BDD-cost:  137
c ---[1738]---> BDD-cost:  128
c ---[1737]---> BDD-cost:  122
c ---[1736]---> BDD-cost:  122
c ---[1735]---> BDD-cost:  134
c ---[1734]---> BDD-cost:  117
c ---[1733]---> BDD-cost:  135
c ---[1732]---> BDD-cost:  131
c ---[1731]---> BDD-cost:  131
c ---[1730]---> BDD-cost:  140
c ---[1729]---> BDD-cost:  131
c ---[1727]---> BDD-cost:  131
c ---[1726]---> BDD-cost:  140
c ---[1725]---> BDD-cost:  113
c ---[1724]---> BDD-cost:  127
c ---[1723]---> BDD-cost:  120
c ---[1722]---> BDD-cost:  137
c ---[1721]---> BDD-cost:  123
c ---[1720]---> BDD-cost:  132
c ---[1719]---> BDD-cost:  128
c ---[1718]---> BDD-cost:  132
c ---[1716]---> BDD-cost:  125
c ---[1715]---> BDD-cost:  111
c ---[1714]---> BDD-cost:  123
c ---[1713]---> BDD-cost:  134
c ---[1712]---> BDD-cost:  122
c ---[1711]---> BDD-cost:  137
c ---[1710]---> BDD-cost:  120
c ---[1709]---> BDD-cost:  114
c ---[1708]---> BDD-cost:  120
c ---[1707]---> BDD-cost:  134
c ---[1704]---> BDD-cost:  123
c ---[1703]---> BDD-cost:  140
c ---[1702]---> BDD-cost:  123
c ---[1701]---> BDD-cost:  140
c ---[1700]---> BDD-cost:  125
c ---[1699]---> BDD-cost:  127
c ---[1698]---> BDD-cost:  122
c ---[1697]---> BDD-cost:  140
c ---[1696]---> BDD-cost:  131
c ---[1695]---> BDD-cost:  131
c ---[1693]---> BDD-cost:  135
c ---[1692]---> BDD-cost:  135
c ---[1691]---> BDD-cost:  115
c ---[1690]---> BDD-cost:  137
c ---[1689]---> BDD-cost:  118
c ---[1688]---> BDD-cost:  135
c ---[1687]---> BDD-cost:  115
c ---[1686]---> BDD-cost:  122
c ---[1685]---> BDD-cost:  131
c ---[1684]---> BDD-cost:  131
c ---[1682]---> BDD-cost:  137
c ---[1681]---> BDD-cost:  120
c ---[1680]---> BDD-cost:  140
c ---[1679]---> BDD-cost:  115
c ---[1678]---> BDD-cost:  122
c ---[1677]---> BDD-cost:  115
c ---[1676]---> BDD-cost:  140
c ---[1675]---> BDD-cost:  123
c ---[1674]---> BDD-cost:  140
c ---[1673]---> BDD-cost:  120
c ---[1671]---> BDD-cost:  137
c ---[1670]---> BDD-cost:  128
c ---[1669]---> BDD-cost:  127
c ---[1668]---> BDD-cost:  125
c ---[1667]---> BDD-cost:  125
c ---[1666]---> BDD-cost:  128
c ---[1665]---> BDD-cost:  130
c ---[1664]---> BDD-cost:  111
c ---[1663]---> BDD-cost:  137
c ---[1662]---> BDD-cost:  123
c ---[1660]---> BDD-cost:  124
c ---[1659]---> BDD-cost:  120
c ---[1658]---> BDD-cost:  134
c ---[1657]---> BDD-cost:  128
c ---[1656]---> BDD-cost:  131
c ---[1655]---> BDD-cost:  125
c ---[1654]---> BDD-cost:  122
c ---[1653]---> BDD-cost:  122
c ---[1652]---> BDD-cost:  137
c ---[1651]---> BDD-cost:  122
c ---[1649]---> BDD-cost:  140
c ---[1648]---> BDD-cost:  120
c ---[1647]---> BDD-cost:  124
c ---[1646]---> BDD-cost:  128
c ---[1645]---> BDD-cost:  140
c ---[1644]---> BDD-cost:  117
c ---[1643]---> BDD-cost:  125
c ---[1642]---> BDD-cost:  131
c ---[1641]---> BDD-cost:  131
c ---[1640]---> BDD-cost:  128
c ---[1638]---> BDD-cost:  128
c ---[1637]---> BDD-cost:  131
c ---[1636]---> BDD-cost:  128
c ---[1635]---> BDD-cost:  134
c ---[1634]---> BDD-cost:  128
c ---[1633]---> BDD-cost:  122
c ---[1632]---> BDD-cost:  122
c ---[1631]---> BDD-cost:  129
c ---[1630]---> BDD-cost:  122
c ---[1629]---> BDD-cost:  131
c ---[1627]---> BDD-cost:  128
c ---[1626]---> BDD-cost:  127
c ---[1625]---> BDD-cost:  122
c ---[1624]---> BDD-cost:  124
c ---[1623]---> BDD-cost:  128
c ---[1622]---> BDD-cost:  137
c ---[1621]---> BDD-cost:  128
c ---[1620]---> BDD-cost:  121
c ---[1619]---> BDD-cost:  125
c ---[1618]---> BDD-cost:  134
c ---[1616]---> BDD-cost:  125
c ---[1615]---> BDD-cost:  119
c ---[1614]---> BDD-cost:  128
c ---[1613]---> BDD-cost:  134
c ---[1612]---> BDD-cost:  115
c ---[1611]---> BDD-cost:  132
c ---[1610]---> BDD-cost:  128
c ---[1609]---> BDD-cost:  137
c ---[1608]---> BDD-cost:  117
c ---[1607]---> BDD-cost:  137
c ---[1605]---> BDD-cost:  117
c ---[1604]---> BDD-cost:  131
c ---[1603]---> BDD-cost:  128
c ---[1602]---> BDD-cost:  140
c ---[1601]---> BDD-cost:  117
c ---[1600]---> BDD-cost:  135
c ---[1599]---> BDD-cost:  125
c ---[1598]---> BDD-cost:  130
c ---[1597]---> BDD-cost:  118
c ---[1596]---> BDD-cost:  137
c ---[1593]---> BDD-cost:  117
c ---[1592]---> BDD-cost:  135
c ---[1591]---> BDD-cost:  128
c ---[1590]---> BDD-cost:  140
c ---[1589]---> BDD-cost:  128
c ---[1588]---> BDD-cost:  135
c ---[1587]---> BDD-cost:  115
c ---[1586]---> BDD-cost:  137
c ---[1585]---> BDD-cost:  118
c ---[1584]---> BDD-cost:  134
c ---[1582]---> BDD-cost:  118
c ---[1581]---> BDD-cost:  130
c ---[1580]---> BDD-cost:  125
c ---[1579]---> BDD-cost:  137
c ---[1578]---> BDD-cost:  125
c ---[1577]---> BDD-cost:  130
c ---[1576]---> BDD-cost:  128
c ---[1575]---> BDD-cost:  140
c ---[1574]---> BDD-cost:  125
c ---[1573]---> BDD-cost:  140
c ---[1571]---> BDD-cost:  131
c ---[1570]---> BDD-cost:  131
c ---[1569]---> BDD-cost:  135
c ---[1568]---> BDD-cost:  135
c ---[1567]---> BDD-cost:  117
c ---[1566]---> BDD-cost:  129
c ---[1565]---> BDD-cost:  125
c ---[1564]---> BDD-cost:  135
c ---[1563]---> BDD-cost:  131
c ---[1562]---> BDD-cost:  131
c ---[1560]---> BDD-cost:  134
c ---[1559]---> BDD-cost:  128
c ---[1558]---> BDD-cost:  125
c ---[1557]---> BDD-cost:  128
c ---[1556]---> BDD-cost:  140
c ---[1555]---> BDD-cost:  128
c ---[1554]---> BDD-cost:  125
c ---[1553]---> BDD-cost:  131
c ---[1552]---> BDD-cost:  131
c ---[1551]---> BDD-cost:  121
c ---[1549]---> BDD-cost:  128
c ---[1548]---> BDD-cost:  137
c ---[1547]---> BDD-cost:  131
c ---[1546]---> BDD-cost:  131
c ---[1545]---> BDD-cost:  134
c ---[1544]---> BDD-cost:  123
c ---[1543]---> BDD-cost:  137
c ---[1542]---> BDD-cost:  125
c ---[1541]---> BDD-cost:  132
c ---[1540]---> BDD-cost:  118
c ---[1538]---> BDD-cost:  129
c ---[1537]---> BDD-cost:  123
c ---[1536]---> BDD-cost:  137
c ---[1535]---> BDD-cost:  128
c ---[1534]---> BDD-cost:  129
c ---[1533]---> BDD-cost:  125
c ---[1532]---> BDD-cost:  134
c ---[1531]---> BDD-cost:  128
c ---[1530]---> BDD-cost:  119
c ---[1529]---> BDD-cost:  128
c ---[1527]---> BDD-cost:  134
c ---[1526]---> BDD-cost:  128
c ---[1525]---> BDD-cost:  119
c ---[1524]---> BDD-cost:  128
c ---[1523]---> BDD-cost:  135
c ---[1522]---> BDD-cost:  131
c ---[1521]---> BDD-cost:  131
c ---[1520]---> BDD-cost:  132
c ---[1519]---> BDD-cost:  132
c ---[1518]---> BDD-cost:  123
c ---[1516]---> BDD-cost:  135
c ---[1515]---> BDD-cost:  125
c ---[1514]---> BDD-cost:  140
c ---[1513]---> BDD-cost:  123
c ---[1512]---> BDD-cost:  135
c ---[1511]---> BDD-cost:  128
c ---[1510]---> BDD-cost:  137
c ---[1509]---> BDD-cost:  128
c ---[1508]---> BDD-cost:  137
c ---[1507]---> BDD-cost:  128
c ---[1505]---> BDD-cost:  117
c ---[1504]---> BDD-cost:  128
c ---[1503]---> BDD-cost:  137
c ---[1502]---> BDD-cost:  118
c ---[1501]---> BDD-cost:  137
c ---[1500]---> BDD-cost:  118
c ---[1499]---> BDD-cost:  132
c ---[1498]---> BDD-cost:  128
c ---[1497]---> BDD-cost:  122
c ---[1496]---> BDD-cost:  111
c ---[1494]---> BDD-cost:  131
c ---[1493]---> BDD-cost:  125
c ---[1492]---> BDD-cost:  137
c ---[1491]---> BDD-cost:  128
c ---[1490]---> BDD-cost:  124
c ---[1489]---> BDD-cost:  111
c ---[1488]---> BDD-cost:  132
c ---[1487]---> BDD-cost:  131
c ---[1486]---> BDD-cost:  131
c ---[1485]---> BDD-cost:  140
c ---[1482]---> BDD-cost:  113
c ---[1481]---> BDD-cost:  115
c ---[1480]---> BDD-cost:  120
c ---[1479]---> BDD-cost:  140
c ---[1478]---> BDD-cost:  123
c ---[1477]---> BDD-cost:  135
c ---[1476]---> BDD-cost:  128
c ---[1475]---> BDD-cost:  132
c ---[1474]---> BDD-cost:  125
c ---[1473]---> BDD-cost:  124
c ---[1471]---> BDD-cost:  123
c ---[1470]---> BDD-cost:  137
c ---[1469]---> BDD-cost:  122
c ---[1468]---> BDD-cost:  137
c ---[1467]---> BDD-cost:  128
c ---[1466]---> BDD-cost:  140
c ---[1465]---> BDD-cost:  117
c ---[1464]---> BDD-cost:  140
c ---[1463]---> BDD-cost:  140
c ---[1462]---> BDD-cost:  128
c ---[1460]---> BDD-cost:  135
c ---[1459]---> BDD-cost:  115
c ---[1458]---> BDD-cost:  129
c ---[1457]---> BDD-cost:  117
c ---[1456]---> BDD-cost:  140
c ---[1455]---> BDD-cost:  140
c ---[1454]---> BDD-cost:  125
c ---[1453]---> BDD-cost:  125
c ---[1452]---> BDD-cost:  128
c ---[1451]---> BDD-cost:  137
c ---[1449]---> BDD-cost:  128
c ---[1448]---> BDD-cost:  120
c ---[1447]---> BDD-cost:  128
c ---[1446]---> BDD-cost:  140
c ---[1445]---> BDD-cost:  131
c ---[1444]---> BDD-cost:  131
c ---[1443]---> BDD-cost:  135
c ---[1442]---> BDD-cost:  135
c ---[1441]---> BDD-cost:  123
c ---[1440]---> BDD-cost:  140
c ---[1438]---> BDD-cost:  125
c ---[1437]---> BDD-cost:  135
c ---[1436]---> BDD-cost:  118
c ---[1435]---> BDD-cost:  120
c ---[1434]---> BDD-cost:  123
c ---[1433]---> BDD-cost:  140
c ---[1432]---> BDD-cost:  128
c ---[1431]---> BDD-cost:  130
c ---[1430]---> BDD-cost:  125
c ---[1429]---> BDD-cost:  128
c ---[1427]---> BDD-cost:  128
c ---[1426]---> BDD-cost:  122
c ---[1425]---> BDD-cost:  128
c ---[1424]---> BDD-cost:  140
c ---[1423]---> BDD-cost:  128
c ---[1422]---> BDD-cost:  132
c ---[1421]---> BDD-cost:  125
c ---[1420]---> BDD-cost:  132
c ---[1419]---> BDD-cost:  123
c ---[1418]---> BDD-cost:  129
c ---[1416]---> BDD-cost:  123
c ---[1415]---> BDD-cost:  137
c ---[1414]---> BDD-cost:  122
c ---[1413]---> BDD-cost:  132
c ---[1412]---> BDD-cost:  123
c ---[1411]---> BDD-cost:  140
c ---[1410]---> BDD-cost:  123
c ---[1409]---> BDD-cost:  134
c ---[1408]---> BDD-cost:  120
c ---[1407]---> BDD-cost:  134
c ---[1405]---> BDD-cost:  113
c ---[1404]---> BDD-cost:  135
c ---[1403]---> BDD-cost:  125
c ---[1402]---> BDD-cost:  137
c ---[1401]---> BDD-cost:  120
c ---[1400]---> BDD-cost:  131
c ---[1399]---> BDD-cost:  113
c ---[1398]---> BDD-cost:  125
c ---[1397]---> BDD-cost:  120
c ---[1396]---> BDD-cost:  140
c ---[1394]---> BDD-cost:  123
c ---[1393]---> BDD-cost:  120
c ---[1392]---> BDD-cost:  128
c ---[1391]---> BDD-cost:  122
c ---[1390]---> BDD-cost:  125
c ---[1389]---> BDD-cost:  129
c ---[1388]---> BDD-cost:  123
c ---[1387]---> BDD-cost:  137
c ---[1386]---> BDD-cost:  122
c ---[1385]---> BDD-cost:  137
c ---[1383]---> BDD-cost:  128
c ---[1382]---> BDD-cost:  122
c ---[1381]---> BDD-cost:  125
c ---[1380]---> BDD-cost:  137
c ---[1379]---> BDD-cost:  123
c ---[1378]---> BDD-cost:  137
c ---[1377]---> BDD-cost:  111
c ---[1376]---> BDD-cost:  122
c ---[1375]---> BDD-cost:  125
c ---[1374]---> BDD-cost:  129
c ---[1371]---> BDD-cost:  120
c ---[1370]---> BDD-cost:  127
c ---[1369]---> BDD-cost:  128
c ---[1368]---> BDD-cost:  126
c ---[1367]---> BDD-cost:  131
c ---[1366]---> BDD-cost:  131
c ---[1365]---> BDD-cost:  140
c ---[1364]---> BDD-cost:  140
c ---[1363]---> BDD-cost:  118
c ---[1362]---> BDD-cost:  120
c ---[1360]---> BDD-cost:  120
c ---[1359]---> BDD-cost:  125
c ---[1358]---> BDD-cost:  120
c ---[1357]---> BDD-cost:  140
c ---[1356]---> BDD-cost:  120
c ---[1355]---> BDD-cost:  130
c ---[1354]---> BDD-cost:  120
c ---[1353]---> BDD-cost:  132
c ---[1352]---> BDD-cost:  117
c ---[1351]---> BDD-cost:  135
c ---[1349]---> BDD-cost:  135
c ---[1348]---> BDD-cost:  122
c ---[1347]---> BDD-cost:  135
c ---[1346]---> BDD-cost:  113
c ---[1345]---> BDD-cost:  135
c ---[1344]---> BDD-cost:  111
c ---[1343]---> BDD-cost:  132
c ---[1342]---> BDD-cost:  122
c ---[1341]---> BDD-cost:  140
c ---[1340]---> BDD-cost:  113
c ---[1338]---> BDD-cost:  131
c ---[1337]---> BDD-cost:  115
c ---[1336]---> BDD-cost:  132
c ---[1335]---> BDD-cost:  118
c ---[1334]---> BDD-cost:  140
c ---[1333]---> BDD-cost:  115
c ---[1332]---> BDD-cost:  137
c ---[1331]---> BDD-cost:  131
c ---[1330]---> BDD-cost:  131
c ---[1329]---> BDD-cost:  127
c ---[1327]---> BDD-cost:  120
c ---[1326]---> BDD-cost:  135
c ---[1325]---> BDD-cost:  115
c ---[1324]---> BDD-cost:  130
c ---[1323]---> BDD-cost:  117
c ---[1322]---> BDD-cost:  131
c ---[1321]---> BDD-cost:  125
c ---[1320]---> BDD-cost:  140
c ---[1319]---> BDD-cost:  131
c ---[1318]---> BDD-cost:  131
c ---[1316]---> BDD-cost:  119
c ---[1315]---> BDD-cost:  128
c ---[1314]---> BDD-cost:  140
c ---[1313]---> BDD-cost:  128
c ---[1312]---> BDD-cost:  135
c ---[1311]---> BDD-cost:  128
c ---[1310]---> BDD-cost:  140
c ---[1309]---> BDD-cost:  115
c ---[1308]---> BDD-cost:  137
c ---[1307]---> BDD-cost:  115
c ---[1305]---> BDD-cost:  134
c ---[1304]---> BDD-cost:  128
c ---[1303]---> BDD-cost:  137
c ---[1302]---> BDD-cost:  131
c ---[1301]---> BDD-cost:  131
c ---[1300]---> BDD-cost:  137
c ---[1299]---> BDD-cost:  128
c ---[1298]---> BDD-cost:  137
c ---[1297]---> BDD-cost:  118
c ---[1296]---> BDD-cost:  122
c ---[1294]---> BDD-cost:  128
c ---[1293]---> BDD-cost:  126
c ---[1292]---> BDD-cost:  117
c ---[1291]---> BDD-cost:  122
c ---[1290]---> BDD-cost:  117
c ---[1289]---> BDD-cost:  137
c ---[1288]---> BDD-cost:  113
c ---[1287]---> BDD-cost:  123
c ---[1286]---> BDD-cost:  115
c ---[1285]---> BDD-cost:  131
c ---[1283]---> BDD-cost:  115
c ---[1282]---> BDD-cost:  140
c ---[1281]---> BDD-cost:  118
c ---[1280]---> BDD-cost:  120
c ---[1279]---> BDD-cost:  120
c ---[1278]---> BDD-cost:  125
c ---[1277]---> BDD-cost:  120
c ---[1276]---> BDD-cost:  140
c ---[1275]---> BDD-cost:  120
c ---[1274]---> BDD-cost:  130
c ---[1272]---> BDD-cost:  120
c ---[1271]---> BDD-cost:  132
c ---[1270]---> BDD-cost:  117
c ---[1269]---> BDD-cost:  135
c ---[1268]---> BDD-cost:  135
c ---[1267]---> BDD-cost:  125
c ---[1266]---> BDD-cost:  113
c ---[1265]---> BDD-cost:  128
c ---[1264]---> BDD-cost:  137
c ---[1263]---> BDD-cost:  128
c ---[1260]---> BDD-cost:  132
c ---[1259]---> BDD-cost:  125
c ---[1258]---> BDD-cost:  137
c ---[1257]---> BDD-cost:  117
c ---[1256]---> BDD-cost:  140
c ---[1255]---> BDD-cost:  115
c ---[1254]---> BDD-cost:  127
c ---[1253]---> BDD-cost:  120
c ---[1252]---> BDD-cost:  137
c ---[1251]---> BDD-cost:  115
c ---[1249]---> BDD-cost:  131
c ---[1248]---> BDD-cost:  115
c ---[1247]---> BDD-cost:  140
c ---[1246]---> BDD-cost:  128
c ---[1245]---> BDD-cost:  120
c ---[1244]---> BDD-cost:  128
c ---[1243]---> BDD-cost:  131
c ---[1242]---> BDD-cost:  128
c ---[1241]---> BDD-cost:  120
c ---[1240]---> BDD-cost:  128
c ---[1238]---> BDD-cost:  140
c ---[1237]---> BDD-cost:  131
c ---[1236]---> BDD-cost:  131
c ---[1235]---> BDD-cost:  127
c ---[1234]---> BDD-cost:  127
c ---[1233]---> BDD-cost:  128
c ---[1232]---> BDD-cost:  137
c ---[1231]---> BDD-cost:  128
c ---[1230]---> BDD-cost:  127
c ---[1229]---> BDD-cost:  131
c ---[1227]---> BDD-cost:  131
c ---[1226]---> BDD-cost:  137
c ---[1051]---> BDD-cost:  110
c ---[1050]---> BDD-cost:  110
c ---[1049]---> BDD-cost:   79
c ---[1048]---> BDD-cost:   79
c ---[1047]---> BDD-cost:   79
c ---[1046]---> BDD-cost:   79
c ---[1045]---> BDD-cost:  110
c ---[1044]---> BDD-cost:  110
c ---[1043]---> BDD-cost:   79
c ---[1042]---> BDD-cost:   79
c ---[1040]---> BDD-cost:   79
c ---[1039]---> BDD-cost:   79
c ---[1038]---> BDD-cost:  116
c ---[1037]---> BDD-cost:  110
c ---[1036]---> BDD-cost:   79
c ---[1035]---> BDD-cost:   79
c ---[1034]---> BDD-cost:   79
c ---[1033]---> BDD-cost:   79
c ---[1032]---> BDD-cost:  104
c ---[1031]---> BDD-cost:  110
c ---[1029]---> BDD-cost:   79
c ---[1028]---> BDD-cost:   79
c ---[1027]---> BDD-cost:   79
c ---[1026]---> BDD-cost:   79
c ---[1025]---> BDD-cost:  110
c ---[1024]---> BDD-cost:  110
c ---[1023]---> BDD-cost:   79
c ---[1022]---> BDD-cost:   79
c ---[1021]---> BDD-cost:   79
c ---[1020]---> BDD-cost:   79
c ---[1018]---> BDD-cost:  112
c ---[1017]---> BDD-cost:  110
c ---[1016]---> BDD-cost:   79
c ---[1015]---> BDD-cost:   79
c ---[1014]---> BDD-cost:   79
c ---[1013]---> BDD-cost:   79
c ---[1012]---> BDD-cost:  116
c ---[1011]---> BDD-cost:  110
c ---[1010]---> BDD-cost:   79
c ---[1009]---> BDD-cost:   79
c ---[1007]---> BDD-cost:   79
c ---[1006]---> BDD-cost:   79
c ---[1005]---> BDD-cost:  116
c ---[1004]---> BDD-cost:  110
c ---[1003]---> BDD-cost:   79
c ---[1002]---> BDD-cost:   79
c ---[1001]---> BDD-cost:   79
c ---[1000]---> BDD-cost:   79
c ---[ 999]---> BDD-cost:  106
c ---[ 998]---> BDD-cost:  110
c ---[ 996]---> BDD-cost:   79
c ---[ 995]---> BDD-cost:   79
c ---[ 994]---> BDD-cost:   79
c ---[ 993]---> BDD-cost:   79
c ---[ 992]---> BDD-cost:  114
c ---[ 991]---> BDD-cost:  110
c ---[ 990]---> BDD-cost:   79
c ---[ 989]---> BDD-cost:   79
c ---[ 988]---> BDD-cost:   79
c ---[ 987]---> BDD-cost:   79
c ---[ 985]---> BDD-cost:  116
c ---[ 984]---> BDD-cost:  110
c ---[ 983]---> BDD-cost:   79
c ---[ 982]---> BDD-cost:   79
c ---[ 981]---> BDD-cost:   79
c ---[ 980]---> BDD-cost:   79
c ---[ 979]---> BDD-cost:  114
c ---[ 978]---> BDD-cost:  110
c ---[ 977]---> BDD-cost:   79
c ---[ 976]---> BDD-cost:   79
c ---[ 974]---> BDD-cost:   79
c ---[ 973]---> BDD-cost:   79
c ---[ 972]---> BDD-cost:  114
c ---[ 971]---> BDD-cost:  110
c ---[ 970]---> BDD-cost:   79
c ---[ 969]---> BDD-cost:   79
c ---[ 968]---> BDD-cost:   79
c ---[ 967]---> BDD-cost:   79
c ---[ 966]---> BDD-cost:  108
c ---[ 965]---> BDD-cost:  110
c ---[ 963]---> BDD-cost:   79
c ---[ 962]---> BDD-cost:   79
c ---[ 961]---> BDD-cost:   79
c ---[ 960]---> BDD-cost:   79
c ---[ 959]---> BDD-cost:  116
c ---[ 958]---> BDD-cost:  110
c ---[ 957]---> BDD-cost:   79
c ---[ 956]---> BDD-cost:   79
c ---[ 955]---> BDD-cost:   79
c ---[ 954]---> BDD-cost:   79
c ---[ 951]---> BDD-cost:  116
c ---[ 950]---> BDD-cost:  110
c ---[ 949]---> BDD-cost:   79
c ---[ 948]---> BDD-cost:   79
c ---[ 947]---> BDD-cost:   79
c ---[ 946]---> BDD-cost:   79
c ---[ 945]---> BDD-cost:  110
c ---[ 944]---> BDD-cost:  110
c ---[ 943]---> BDD-cost:   79
c ---[ 942]---> BDD-cost:   79
c ---[ 940]---> BDD-cost:   79
c ---[ 939]---> BDD-cost:   79
c ---[ 938]---> BDD-cost:  116
c ---[ 937]---> BDD-cost:  110
c ---[ 936]---> BDD-cost:   79
c ---[ 935]---> BDD-cost:   79
c ---[ 934]---> BDD-cost:   79
c ---[ 933]---> BDD-cost:   79
c ---[ 932]---> BDD-cost:  116
c ---[ 931]---> BDD-cost:  110
c ---[ 929]---> BDD-cost:   79
c ---[ 928]---> BDD-cost:   79
c ---[ 927]---> BDD-cost:   79
c ---[ 926]---> BDD-cost:   79
c ---[ 925]---> BDD-cost:  114
c ---[ 924]---> BDD-cost:  110
c ---[ 923]---> BDD-cost:   79
c ---[ 922]---> BDD-cost:   79
c ---[ 921]---> BDD-cost:   79
c ---[ 920]---> BDD-cost:   79
c ---[ 918]---> BDD-cost:  116
c ---[ 917]---> BDD-cost:  110
c ---[ 916]---> BDD-cost:   79
c ---[ 915]---> BDD-cost:   79
c ---[ 914]---> BDD-cost:   79
c ---[ 913]---> BDD-cost:   79
c ---[ 912]---> BDD-cost:  110
c ---[ 911]---> BDD-cost:  110
c ---[ 910]---> BDD-cost:   79
c ---[ 909]---> BDD-cost:   79
c ---[ 907]---> BDD-cost:   79
c ---[ 906]---> BDD-cost:   79
c ---[ 905]---> BDD-cost:  116
c ---[ 904]---> BDD-cost:  110
c ---[ 903]---> BDD-cost:   79
c ---[ 902]---> BDD-cost:   79
c ---[ 901]---> BDD-cost:   79
c ---[ 900]---> BDD-cost:   79
c ---[ 899]---> BDD-cost:  116
c ---[ 898]---> BDD-cost:  110
c ---[ 896]---> BDD-cost:   79
c ---[ 895]---> BDD-cost:   79
c ---[ 894]---> BDD-cost:   79
c ---[ 893]---> BDD-cost:   79
c ---[ 892]---> BDD-cost:  112
c ---[ 891]---> BDD-cost:  110
c ---[ 890]---> BDD-cost:   79
c ---[ 889]---> BDD-cost:   79
c ---[ 888]---> BDD-cost:   79
c ---[ 887]---> BDD-cost:   79
c ---[ 885]---> BDD-cost:  116
c ---[ 884]---> BDD-cost:  110
c ---[ 883]---> BDD-cost:   79
c ---[ 882]---> BDD-cost:   79
c ---[ 881]---> BDD-cost:   79
c ---[ 880]---> BDD-cost:   79
c ---[ 879]---> BDD-cost:  116
c ---[ 878]---> BDD-cost:  110
c ---[ 877]---> BDD-cost:   79
c ---[ 876]---> BDD-cost:   79
c ---[ 874]---> BDD-cost:   79
c ---[ 873]---> BDD-cost:   79
c ---[ 872]---> BDD-cost:  116
c ---[ 871]---> BDD-cost:  110
c ---[ 870]---> BDD-cost:   79
c ---[ 869]---> BDD-cost:   79
c ---[ 868]---> BDD-cost:   79
c ---[ 867]---> BDD-cost:   79
c ---[ 866]---> BDD-cost:  116
c ---[ 865]---> BDD-cost:  110
c ---[ 863]---> BDD-cost:   79
c ---[ 862]---> BDD-cost:   79
c ---[ 861]---> BDD-cost:   79
c ---[ 860]---> BDD-cost:   79
c ---[ 859]---> BDD-cost:  116
c ---[ 858]---> BDD-cost:  110
c ---[ 857]---> BDD-cost:   79
c ---[ 856]---> BDD-cost:   79
c ---[ 855]---> BDD-cost:   79
c ---[ 854]---> BDD-cost:   79
c ---[ 852]---> BDD-cost:  116
c ---[ 851]---> BDD-cost:  110
c ---[ 850]---> BDD-cost:   79
c ---[ 849]---> BDD-cost:   79
c ---[ 848]---> BDD-cost:   79
c ---[ 847]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:  108
c ---[ 845]---> BDD-cost:  110
c ---[ 844]---> BDD-cost:   79
c ---[ 843]---> BDD-cost:   79
c ---[ 840]---> BDD-cost:   79
c ---[ 839]---> BDD-cost:   79
c ---[ 838]---> BDD-cost:  116
c ---[ 837]---> BDD-cost:  110
c ---[ 836]---> BDD-cost:   79
c ---[ 835]---> BDD-cost:   79
c ---[ 834]---> BDD-cost:   79
c ---[ 833]---> BDD-cost:   79
c ---[ 832]---> BDD-cost:  116
c ---[ 831]---> BDD-cost:  110
c ---[ 829]---> BDD-cost:   79
c ---[ 828]---> BDD-cost:   79
c ---[ 827]---> BDD-cost:   79
c ---[ 826]---> BDD-cost:   79
c ---[ 825]---> BDD-cost:  114
c ---[ 824]---> BDD-cost:  110
c ---[ 823]---> BDD-cost:   79
c ---[ 822]---> BDD-cost:   79
c ---[ 821]---> BDD-cost:   79
c ---[ 820]---> BDD-cost:   79
c ---[ 818]---> BDD-cost:  116
c ---[ 817]---> BDD-cost:  110
c ---[ 816]---> BDD-cost:   79
c ---[ 815]---> BDD-cost:   79
c ---[ 814]---> BDD-cost:   79
c ---[ 813]---> BDD-cost:   79
c ---[ 812]---> BDD-cost:  116
c ---[ 811]---> BDD-cost:  110
c ---[ 810]---> BDD-cost:   79
c ---[ 809]---> BDD-cost:   79
c ---[ 807]---> BDD-cost:   79
c ---[ 806]---> BDD-cost:   79
c ---[ 805]---> BDD-cost:  110
c ---[ 804]---> BDD-cost:  110
c ---[ 803]---> BDD-cost:   79
c ---[ 802]---> BDD-cost:   79
c ---[ 801]---> BDD-cost:   79
c ---[ 800]---> BDD-cost:   79
c ---[ 799]---> BDD-cost:  116
c ---[ 798]---> BDD-cost:  110
c ---[ 796]---> BDD-cost:   79
c ---[ 795]---> BDD-cost:   79
c ---[ 794]---> BDD-cost:   79
c ---[ 793]---> BDD-cost:   79
c ---[ 792]---> BDD-cost:  116
c ---[ 791]---> BDD-cost:  110
c ---[ 790]---> BDD-cost:   79
c ---[ 789]---> BDD-cost:   79
c ---[ 788]---> BDD-cost:   79
c ---[ 787]---> BDD-cost:   79
c ---[ 785]---> BDD-cost:  116
c ---[ 784]---> BDD-cost:  110
c ---[ 783]---> BDD-cost:   79
c ---[ 782]---> BDD-cost:   79
c ---[ 781]---> BDD-cost:   79
c ---[ 780]---> BDD-cost:   79
c ---[ 779]---> BDD-cost:  116
c ---[ 778]---> BDD-cost:  110
c ---[ 777]---> BDD-cost:   79
c ---[ 776]---> BDD-cost:   79
c ---[ 774]---> BDD-cost:   79
c ---[ 773]---> BDD-cost:   79
c ---[ 772]---> BDD-cost:  112
c ---[ 771]---> BDD-cost:  110
c ---[ 770]---> BDD-cost:   79
c ---[ 769]---> BDD-cost:   79
c ---[ 768]---> BDD-cost:   79
c ---[ 767]---> BDD-cost:   79
c ---[ 766]---> BDD-cost:  116
c ---[ 765]---> BDD-cost:  110
c ---[ 763]---> BDD-cost:   79
c ---[ 762]---> BDD-cost:   79
c ---[ 761]---> BDD-cost:   79
c ---[ 760]---> BDD-cost:   79
c ---[ 759]---> BDD-cost:  108
c ---[ 758]---> BDD-cost:  110
c ---[ 757]---> BDD-cost:   79
c ---[ 756]---> BDD-cost:   79
c ---[ 755]---> BDD-cost:   79
c ---[ 754]---> BDD-cost:   79
c ---[ 752]---> BDD-cost:  116
c ---[ 751]---> BDD-cost:  110
c ---[ 750]---> BDD-cost:   79
c ---[ 749]---> BDD-cost:   79
c ---[ 748]---> BDD-cost:   79
c ---[ 747]---> BDD-cost:   79
c ---[ 746]---> BDD-cost:  114
c ---[ 745]---> BDD-cost:  110
c ---[ 744]---> BDD-cost:   79
c ---[ 743]---> BDD-cost:   79
c ---[ 741]---> BDD-cost:   79
c ---[ 740]---> BDD-cost:   79
c ---[ 739]---> BDD-cost:  116
c ---[ 738]---> BDD-cost:  110
c ---[ 737]---> BDD-cost:   79
c ---[ 736]---> BDD-cost:   79
c ---[ 735]---> BDD-cost:   79
c ---[ 734]---> BDD-cost:   79
c ---[ 732]---> BDD-cost:  114
c ---[ 728]---> BDD-cost:  116
c ---[ 726]---> BDD-cost:  112
c ---[ 724]---> BDD-cost:   79
c ---[ 722]---> BDD-cost:  116
c ---[ 720]---> BDD-cost:   79
c ---[ 717]---> BDD-cost:  114
c ---[ 715]---> BDD-cost:   79
c ---[ 713]---> BDD-cost:   79
c ---[ 711]---> BDD-cost:   79
c ---[ 709]---> BDD-cost:  116
c ---[ 706]---> BDD-cost:   79
c ---[ 704]---> BDD-cost:   79
c ---[ 702]---> BDD-cost:  114
c ---[ 700]---> BDD-cost:   79
c ---[ 698]---> BDD-cost:  112
c ---[ 695]---> BDD-cost:  114
c ---[ 693]---> BDD-cost:  116
c ---[ 691]---> BDD-cost:  116
c ---[ 689]---> BDD-cost:  116
c ---[ 687]---> BDD-cost:  116
c ---[ 684]---> BDD-cost:  116
c ---[ 682]---> BDD-cost:  116
c ---[ 680]---> BDD-cost:  112
c ---[ 678]---> BDD-cost:  116
c ---[ 676]---> BDD-cost:  114
c ---[ 673]---> BDD-cost:  116
c ---[ 671]---> BDD-cost:  114
c ---[ 669]---> BDD-cost:  116
c ---[ 667]---> BDD-cost:  114
c ---[ 665]---> BDD-cost:   79
c ---[ 662]---> BDD-cost:  108
c ---[ 660]---> BDD-cost:  112
c ---[ 658]---> BDD-cost:  116
c ---[ 656]---> BDD-cost:  116
c ---[ 654]---> BDD-cost:  114
c ---[ 651]---> BDD-cost:  116
c ---[ 649]---> BDD-cost:  112
c ---[ 647]---> BDD-cost:  108
c ---[ 645]---> BDD-cost:  116
c ---[ 643]---> BDD-cost:  116
c ---[ 640]---> BDD-cost:  114
c ---[ 638]---> BDD-cost:  112
c ---[ 636]---> BDD-cost:  116
c ---[ 634]---> BDD-cost:  116
c ---[ 632]---> BDD-cost:  114
c ---[ 629]---> BDD-cost:  116
c ---[ 627]---> BDD-cost:  116
c ---[ 625]---> BDD-cost:  116
c ---[ 623]---> BDD-cost:  114
c ---[ 621]---> BDD-cost:  112
c ---[ 617]---> BDD-cost:  116
c ---[ 615]---> BDD-cost:   79
c ---[ 613]---> BDD-cost:  116
c ---[ 611]---> BDD-cost:  112
c ---[ 609]---> BDD-cost:  112
c ---[ 606]---> BDD-cost:  116
c ---[ 604]---> BDD-cost:  116
c ---[ 602]---> BDD-cost:  116
c ---[ 600]---> BDD-cost:  114
c ---[ 598]---> BDD-cost:  112
c ---[ 595]---> BDD-cost:  114
c ---[ 593]---> BDD-cost:   79
c ---[ 591]---> BDD-cost:   79
c ---[ 589]---> BDD-cost:  116
c ---[ 587]---> BDD-cost:  114
c ---[ 584]---> BDD-cost:   79
c ---[ 582]---> BDD-cost:   79
c ---[ 580]---> BDD-cost:  114
c ---[ 578]---> BDD-cost:  116
c ---[ 576]---> BDD-cost:   79
c ---[ 573]---> BDD-cost:  114
c ---[ 571]---> BDD-cost:   79
c ---[ 569]---> BDD-cost:   79
c ---[ 567]---> BDD-cost:  116
c ---[ 565]---> BDD-cost:   79
c ---[ 562]---> BDD-cost:  114
c ---[ 560]---> BDD-cost:  116
c ---[ 558]---> BDD-cost:  114
c ---[ 556]---> BDD-cost:   79
c ---[ 554]---> BDD-cost:   79
c ---[ 551]---> BDD-cost:  116
c ---[ 549]---> BDD-cost:  116
c ---[ 547]---> BDD-cost:   79
c ---[ 545]---> BDD-cost:   79
c ---[ 543]---> BDD-cost:  112
c ---[ 540]---> BDD-cost:   79
c ---[ 538]---> BDD-cost:  114
c ---[ 536]---> BDD-cost:   79
c ---[ 534]---> BDD-cost:   79
c ---[ 532]---> BDD-cost:  116
c ---[ 529]---> BDD-cost:  116
c ---[ 527]---> BDD-cost:  116
c ---[ 525]---> BDD-cost:  116
c ---[ 524]---> BDD-cost:  137
c ---[ 523]---> BDD-cost:  137
c ---[ 522]---> BDD-cost:  128
c ---[ 521]---> BDD-cost:  128
c ---[ 519]---> BDD-cost:  137
c ---[ 518]---> BDD-cost:  137
c ---[ 517]---> BDD-cost:  128
c ---[ 516]---> BDD-cost:  128
c ---[ 515]---> BDD-cost:  107
c ---[ 514]---> BDD-cost:  107
c ---[ 513]---> BDD-cost:  128
c ---[ 512]---> BDD-cost:  128
c ---[ 511]---> BDD-cost:  137
c ---[ 510]---> BDD-cost:  137
c ---[ 507]---> BDD-cost:  128
c ---[ 506]---> BDD-cost:  128
c ---[ 505]---> BDD-cost:  137
c ---[ 504]---> BDD-cost:  137
c ---[ 503]---> BDD-cost:  128
c ---[ 502]---> BDD-cost:  128
c ---[ 501]---> BDD-cost:  134
c ---[ 500]---> BDD-cost:  134
c ---[ 499]---> BDD-cost:  128
c ---[ 498]---> BDD-cost:  128
c ---[ 496]---> BDD-cost:  132
c ---[ 495]---> BDD-cost:  132
c ---[ 494]---> BDD-cost:  128
c ---[ 493]---> BDD-cost:  128
c ---[ 492]---> BDD-cost:  135
c ---[ 491]---> BDD-cost:  135
c ---[ 490]---> BDD-cost:  128
c ---[ 489]---> BDD-cost:  128
c ---[ 488]---> BDD-cost:  134
c ---[ 487]---> BDD-cost:  134
c ---[ 485]---> BDD-cost:  128
c ---[ 484]---> BDD-cost:  128
c ---[ 483]---> BDD-cost:  134
c ---[ 482]---> BDD-cost:  134
c ---[ 481]---> BDD-cost:  128
c ---[ 480]---> BDD-cost:  128
c ---[ 479]---> BDD-cost:  132
c ---[ 478]---> BDD-cost:  132
c ---[ 477]---> BDD-cost:  128
c ---[ 476]---> BDD-cost:  128
c ---[ 474]---> BDD-cost:  137
c ---[ 473]---> BDD-cost:  137
c ---[ 472]---> BDD-cost:  128
c ---[ 471]---> BDD-cost:  128
c ---[ 470]---> BDD-cost:  134
c ---[ 469]---> BDD-cost:  134
c ---[ 468]---> BDD-cost:  128
c ---[ 467]---> BDD-cost:  128
c ---[ 466]---> BDD-cost:  134
c ---[ 465]---> BDD-cost:  134
c ---[ 463]---> BDD-cost:  128
c ---[ 462]---> BDD-cost:  128
c ---[ 461]---> BDD-cost:  112
c ---[ 460]---> BDD-cost:  112
c ---[ 459]---> BDD-cost:  128
c ---[ 458]---> BDD-cost:  128
c ---[ 457]---> BDD-cost:  127
c ---[ 456]---> BDD-cost:  127
c ---[ 455]---> BDD-cost:  128
c ---[ 454]---> BDD-cost:  128
c ---[ 452]---> BDD-cost:  137
c ---[ 451]---> BDD-cost:  137
c ---[ 450]---> BDD-cost:  128
c ---[ 449]---> BDD-cost:  128
c ---[ 448]---> BDD-cost:  127
c ---[ 447]---> BDD-cost:  127
c ---[ 446]---> BDD-cost:  128
c ---[ 445]---> BDD-cost:  128
c ---[ 444]---> BDD-cost:  132
c ---[ 443]---> BDD-cost:  132
c ---[ 441]---> BDD-cost:  128
c ---[ 440]---> BDD-cost:  128
c ---[ 439]---> BDD-cost:  137
c ---[ 438]---> BDD-cost:  137
c ---[ 437]---> BDD-cost:  128
c ---[ 436]---> BDD-cost:  128
c ---[ 435]---> BDD-cost:  124
c ---[ 434]---> BDD-cost:  124
c ---[ 433]---> BDD-cost:  128
c ---[ 432]---> BDD-cost:  128
c ---[ 430]---> BDD-cost:  137
c ---[ 429]---> BDD-cost:  137
c ---[ 428]---> BDD-cost:  128
c ---[ 427]---> BDD-cost:  128
c ---[ 426]---> BDD-cost:  129
c ---[ 425]---> BDD-cost:  129
c ---[ 424]---> BDD-cost:  128
c ---[ 423]---> BDD-cost:  128
c ---[ 422]---> BDD-cost:  122
c ---[ 421]---> BDD-cost:  122
c ---[ 419]---> BDD-cost:  128
c ---[ 418]---> BDD-cost:  128
c ---[ 417]---> BDD-cost:  137
c ---[ 416]---> BDD-cost:  137
c ---[ 415]---> BDD-cost:  128
c ---[ 414]---> BDD-cost:  128
c ---[ 413]---> BDD-cost:  127
c ---[ 412]---> BDD-cost:  127
c ---[ 411]---> BDD-cost:  128
c ---[ 410]---> BDD-cost:  128
c ---[ 408]---> BDD-cost:  112
c ---[ 407]---> BDD-cost:  112
c ---[ 406]---> BDD-cost:  128
c ---[ 405]---> BDD-cost:  128
c ---[ 404]---> BDD-cost:  132
c ---[ 403]---> BDD-cost:  132
c ---[ 402]---> BDD-cost:  128
c ---[ 401]---> BDD-cost:  128
c ---[ 400]---> BDD-cost:  122
c ---[ 399]---> BDD-cost:  122
c ---[ 396]---> BDD-cost:  128
c ---[ 395]---> BDD-cost:  128
c ---[ 394]---> BDD-cost:  127
c ---[ 393]---> BDD-cost:  127
c ---[ 392]---> BDD-cost:  128
c ---[ 391]---> BDD-cost:  128
c ---[ 390]---> BDD-cost:  107
c ---[ 389]---> BDD-cost:  107
c ---[ 388]---> BDD-cost:  128
c ---[ 387]---> BDD-cost:  128
c ---[ 385]---> BDD-cost:  137
c ---[ 384]---> BDD-cost:  137
c ---[ 383]---> BDD-cost:  128
c ---[ 382]---> BDD-cost:  128
c ---[ 381]---> BDD-cost:  127
c ---[ 380]---> BDD-cost:  127
c ---[ 379]---> BDD-cost:  128
c ---[ 378]---> BDD-cost:  128
c ---[ 377]---> BDD-cost:  107
c ---[ 376]---> BDD-cost:  107
c ---[ 374]---> BDD-cost:  128
c ---[ 373]---> BDD-cost:  128
c ---[ 372]---> BDD-cost:  137
c ---[ 371]---> BDD-cost:  137
c ---[ 370]---> BDD-cost:  128
c ---[ 369]---> BDD-cost:  128
c ---[ 368]---> BDD-cost:  129
c ---[ 367]---> BDD-cost:  129
c ---[ 366]---> BDD-cost:  128
c ---[ 365]---> BDD-cost:  128
c ---[ 363]---> BDD-cost:  132
c ---[ 362]---> BDD-cost:  132
c ---[ 361]---> BDD-cost:  128
c ---[ 360]---> BDD-cost:  128
c ---[ 359]---> BDD-cost:  134
c ---[ 358]---> BDD-cost:  134
c ---[ 357]---> BDD-cost:  128
c ---[ 356]---> BDD-cost:  128
c ---[ 355]---> BDD-cost:  132
c ---[ 354]---> BDD-cost:  132
c ---[ 352]---> BDD-cost:  128
c ---[ 351]---> BDD-cost:  128
c ---[ 350]---> BDD-cost:  122
c ---[ 349]---> BDD-cost:  122
c ---[ 348]---> BDD-cost:  128
c ---[ 347]---> BDD-cost:  128
c ---[ 346]---> BDD-cost:  127
c ---[ 345]---> BDD-cost:  127
c ---[ 344]---> BDD-cost:  128
c ---[ 343]---> BDD-cost:  128
c ---[ 341]---> BDD-cost:  119
c ---[ 340]---> BDD-cost:  119
c ---[ 339]---> BDD-cost:  128
c ---[ 338]---> BDD-cost:  128
c ---[ 337]---> BDD-cost:  137
c ---[ 336]---> BDD-cost:  137
c ---[ 335]---> BDD-cost:  128
c ---[ 334]---> BDD-cost:  128
c ---[ 333]---> BDD-cost:  127
c ---[ 332]---> BDD-cost:  127
c ---[ 330]---> BDD-cost:  128
c ---[ 329]---> BDD-cost:  128
c ---[ 328]---> BDD-cost:  137
c ---[ 327]---> BDD-cost:  137
c ---[ 326]---> BDD-cost:  128
c ---[ 325]---> BDD-cost:  128
c ---[ 324]---> BDD-cost:  132
c ---[ 323]---> BDD-cost:  132
c ---[ 322]---> BDD-cost:  128
c ---[ 321]---> BDD-cost:  128
c ---[ 319]---> BDD-cost:  134
c ---[ 318]---> BDD-cost:  134
c ---[ 317]---> BDD-cost:  128
c ---[ 316]---> BDD-cost:  128
c ---[ 315]---> BDD-cost:  117
c ---[ 314]---> BDD-cost:  117
c ---[ 313]---> BDD-cost:  128
c ---[ 312]---> BDD-cost:  128
c ---[ 311]---> BDD-cost:  113
c ---[ 310]---> BDD-cost:  140
c ---[ 308]---> BDD-cost:  111
c ---[ 307]---> BDD-cost:  132
c ---[ 306]---> BDD-cost:  123
c ---[ 305]---> BDD-cost:  140
c ---[ 304]---> BDD-cost:  115
c ---[ 303]---> BDD-cost:  134
c ---[ 302]---> BDD-cost:  115
c ---[ 301]---> BDD-cost:  130
c ---[ 300]---> BDD-cost:  118
c ---[ 299]---> BDD-cost:  140
c ---[ 297]---> BDD-cost:  115
c ---[ 296]---> BDD-cost:  140
c ---[ 295]---> BDD-cost:  123
c ---[ 294]---> BDD-cost:  130
c ---[ 293]---> BDD-cost:  117
c ---[ 292]---> BDD-cost:  130
c ---[ 291]---> BDD-cost:  123
c ---[ 290]---> BDD-cost:  131
c ---[ 289]---> BDD-cost:  113
c ---[ 288]---> BDD-cost:  135
c ---[ 287]---> BDD-cost:   23
c ---[ 286]---> BDD-cost:   23
c ---[ 285]---> BDD-cost:   23
c ---[ 284]---> BDD-cost:   23
c ---[ 283]---> BDD-cost:   23
c ---[ 282]---> BDD-cost:   23
c ---[ 281]---> BDD-cost:   23
c ---[ 280]---> BDD-cost:   23
c ---[ 279]---> BDD-cost:   23
c ---[ 278]---> BDD-cost:   23
c ---[ 277]---> BDD-cost:   23
c ---[ 276]---> BDD-cost:   23
c ---[ 275]---> BDD-cost:   23
c ---[ 274]---> BDD-cost:   23
c ---[ 273]---> BDD-cost:   23
c ---[ 272]---> BDD-cost:   23
c ---[ 271]---> BDD-cost:   23
c ---[ 270]---> BDD-cost:   23
c ---[ 269]---> BDD-cost:   23
c ---[ 268]---> BDD-cost:   23
c ---[ 267]---> BDD-cost:   23
c ---[ 266]---> BDD-cost:   23
c ---[ 265]---> BDD-cost:   23
c ---[ 264]---> BDD-cost:   23
c ---[ 263]---> BDD-cost:   23
c ---[ 262]---> BDD-cost:   23
c ---[ 261]---> BDD-cost:   23
c ---[ 260]---> BDD-cost:   23
c ---[ 259]---> BDD-cost:   23
c ---[ 258]---> BDD-cost:   23
c ---[ 257]---> BDD-cost:   23
c ---[ 256]---> BDD-cost:   23
c ---[ 255]---> BDD-cost:   23
c ---[ 254]---> BDD-cost:   23
c ---[ 253]---> BDD-cost:   23
c ---[ 252]---> BDD-cost:   23
c ---[ 251]---> BDD-cost:   23
c ---[ 250]---> BDD-cost:   23
c ---[ 249]---> BDD-cost:   23
c ---[ 248]---> BDD-cost:   23
c ---[ 247]---> BDD-cost:   23
c ---[ 246]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:   23
c ---[ 244]---> BDD-cost:   23
c ---[ 243]---> BDD-cost:   23
c ---[ 242]---> BDD-cost:   23
c ---[ 241]---> BDD-cost:   23
c ---[ 240]---> BDD-cost:   23
c ---[ 239]---> BDD-cost:   23
c ---[ 238]---> BDD-cost:   23
c ---[ 237]---> BDD-cost:   23
c ---[ 236]---> BDD-cost:   23
c ---[ 235]---> BDD-cost:   23
c ---[ 234]---> BDD-cost:   23
c ---[ 233]---> BDD-cost:   23
c ---[ 232]---> BDD-cost:   23
c ---[ 231]---> BDD-cost:   23
c ---[ 230]---> BDD-cost:   23
c ---[ 229]---> BDD-cost:   23
c ---[ 228]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   23
c ---[ 226]---> BDD-cost:   23
c ---[ 225]---> BDD-cost:   23
c ---[ 224]---> BDD-cost:   23
c ---[ 223]---> BDD-cost:   23
c ---[ 222]---> BDD-cost:   23
c ---[ 221]---> BDD-cost:   23
c ---[ 220]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   23
c ---[ 218]---> BDD-cost:   23
c ---[ 217]---> BDD-cost:   23
c ---[ 216]---> BDD-cost:   23
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:   23
c ---[ 212]---> BDD-cost:   23
c ---[ 211]---> BDD-cost:   23
c ---[ 210]---> BDD-cost:   23
c ---[ 209]---> BDD-cost:   23
c ---[ 208]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   23
c ---[ 206]---> BDD-cost:   23
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   23
c ---[ 203]---> BDD-cost:   23
c ---[ 202]---> BDD-cost:   23
c ---[ 201]---> BDD-cost:   23
c ---[ 200]---> BDD-cost:   23
c ---[ 199]---> BDD-cost:   23
c ---[ 198]---> BDD-cost:   23
c ---[ 197]---> BDD-cost:   23
c ---[ 196]---> BDD-cost:   23
c ---[ 195]---> BDD-cost:   23
c ---[ 194]---> BDD-cost:   23
c ---[ 193]---> BDD-cost:   23
c ---[ 192]---> BDD-cost:   23
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   23
c ---[ 189]---> BDD-cost:   23
c ---[ 188]---> BDD-cost:   23
c ---[ 187]---> BDD-cost:   23
c ---[ 186]---> BDD-cost:   23
c ---[ 185]---> BDD-cost:   23
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   23
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   23
c ---[ 178]---> BDD-cost:   23
c ---[ 177]---> BDD-cost:   23
c ---[ 176]---> BDD-cost:   23
c ---[ 175]---> BDD-cost:   23
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   23
c ---[ 172]---> BDD-cost:   23
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   23
c ---[ 169]---> BDD-cost:   23
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   23
c ---[ 165]---> BDD-cost:   23
c ---[ 164]---> BDD-cost:   23
c ---[ 163]---> BDD-cost:   23
c ---[ 162]---> BDD-cost:   23
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   23
c ---[ 159]---> BDD-cost:   23
c ---[ 158]---> BDD-cost:   23
c ---[ 157]---> BDD-cost:   23
c ---[ 156]---> BDD-cost:   23
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   23
c ---[ 153]---> BDD-cost:   23
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   23
c ---[ 149]---> BDD-cost:   23
c ---[ 148]---> BDD-cost:   23
c ---[ 147]---> BDD-cost:   23
c ---[ 146]---> BDD-cost:   23
c ---[ 145]---> BDD-cost:   23
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:   23
c ---[ 140]---> BDD-cost:   23
c ---[ 139]---> BDD-cost:   23
c ---[ 138]---> BDD-cost:   23
c ---[ 137]---> BDD-cost:   23
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   23
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:   23
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   23
c ---[ 123]---> BDD-cost:   23
c ---[ 122]---> BDD-cost:   23
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   23
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:   23
c ---[ 117]---> BDD-cost:   23
c ---[ 116]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   23
c ---[ 114]---> BDD-cost:   23
c ---[ 113]---> BDD-cost:   23
c ---[ 112]---> BDD-cost:   23
c ---[ 111]---> BDD-cost:   23
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   23
c ---[ 107]---> BDD-cost:   23
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   23
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   23
c ---[ 102]---> BDD-cost:   23
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   23
c ---[  99]---> BDD-cost:   23
c ---[  98]---> BDD-cost:   23
c ---[  97]---> BDD-cost:   23
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   23
c ---[  94]---> BDD-cost:   23
c ---[  93]---> BDD-cost:   23
c ---[  92]---> BDD-cost:   23
c ---[  91]---> BDD-cost:   23
c ---[  90]---> BDD-cost:   23
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   23
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   23
c ---[  85]---> BDD-cost:   23
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   23
c ---[  82]---> BDD-cost:   23
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   23
c ---[  78]---> BDD-cost:   23
c ---[  77]---> BDD-cost:   23
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   23
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   23
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:   23
c ---[  68]---> BDD-cost:   23
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   23
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   23
c ---[  62]---> BDD-cost:   23
c ---[  61]---> BDD-cost:   23
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   23
c ---[  58]---> BDD-cost:   23
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   23
c ---[  55]---> BDD-cost:   23
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   23
c ---[  52]---> BDD-cost:   23
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   23
c ---[  49]---> BDD-cost:   23
c ---[  48]---> BDD-cost:   23
c ---[  47]---> BDD-cost:   23
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:   23
c ---[  42]---> BDD-cost:   23
c ---[  41]---> BDD-cost:   23
c ---[  40]---> BDD-cost:   23
c ---[  39]---> BDD-cost:   23
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   23
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   23
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   23
c ---[  28]---> BDD-cost:   23
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   23
c ---[  25]---> BDD-cost:   23
c ---[  24]---> BDD-cost:   23
c ---[  23]---> BDD-cost:   23
c ---[  22]---> BDD-cost:   23
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   23
c ---[  19]---> BDD-cost:   23
c ---[  18]---> BDD-cost:   23
c ---[  17]---> BDD-cost:   23
c ---[  16]---> BDD-cost:   23
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   23
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   23
c ---[  11]---> BDD-cost:   23
c ---[  10]---> BDD-cost:   23
c ---[   9]---> BDD-cost:   23
c ---[   8]---> BDD-cost:   23
c ---[   7]---> BDD-cost:   23
c ---[   6]---> BDD-cost:   23
c ---[   5]---> BDD-cost:   23
c ---[   4]---> BDD-cost:   23
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   23
c ---[   1]---> BDD-cost:   23
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  269814   723653 |   89938       0        0     nan |  0.000 % |
c |       100 |  269814   723653 |   98931     100      807     8.1 |  1.135 % |
c |       250 |  269774   723573 |  108824     230     1712     7.4 |  1.151 % |
c |       475 |  269682   723389 |  119707     409     3023     7.4 |  1.188 % |
c |       812 |  269682   723389 |  131678     746     7016     9.4 |  1.188 % |
c |      1318 |  269680   723385 |  144846    1251    14324    11.5 |  1.188 % |
c ==============================================================================
c [1mFound solution: 12544[0m
c ---[   0]---> BDD-cost:  137
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1401 |  269995   724330 |   89998    1332    14893    11.2 |  1.188 % |
c |      1501 |  269945   724230 |   98997    1407    15879    11.3 |  1.209 % |
c |      1651 |  269943   724226 |  108897    1556    16744    10.8 |  1.210 % |
c ==============================================================================
c [1mFound solution: 12032[0m
c ---[   0]---> BDD-cost:  168
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1856 |  270425   725682 |   90141    1752    18725    10.7 |  1.210 % |
c |      1957 |  270421   725674 |   99155    1851    19401    10.5 |  1.218 % |
c |      2107 |  270405   725642 |  109070    1992    20816    10.4 |  1.224 % |
c |      2332 |  270285   725402 |  119977    2157    22063    10.2 |  1.271 % |
c ==============================================================================
c [1mFound solution: 10240[0m
c ---[   0]---> Sorter-cost:  766     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2507 |  271094   727308 |   90364    2332    24681    10.6 |  1.271 % |
c |      2607 |  271062   727244 |   99400    2416    25195    10.4 |  1.283 % |
c |      2758 |  271026   727172 |  109340    2549    26539    10.4 |  1.297 % |
c |      2984 |  271012   727144 |  120274    2768    29734    10.7 |  1.303 % |
c ==============================================================================
c [1mFound solution: 9728[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3152 |  271031   727205 |   90343    2929    31312    10.7 |  1.303 % |
c |      3253 |  271031   727205 |   99377    3030    31978    10.6 |  1.314 % |
c |      3403 |  271017   727177 |  109315    3173    33099    10.4 |  1.319 % |
c |      3629 |  270919   726981 |  120246    3349    34482    10.3 |  1.358 % |
c |      3966 |  270869   726881 |  132271    3661    36488    10.0 |  1.377 % |
c |      4473 |  270827   726797 |  145498    4147    42020    10.1 |  1.394 % |
c |      5233 |  270639   726421 |  160048    4813    47823     9.9 |  1.468 % |
c |      6373 |  270585   726313 |  176052    5926    70851    12.0 |  1.489 % |
c ==============================================================================
c [1mFound solution: 9472[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6857 |  270548   726239 |   90182    6383    74634    11.7 |  1.489 % |
c |      6957 |  270548   726239 |   99200    6483    75274    11.6 |  1.513 % |
c |      7107 |  270546   726235 |  109120    6632    76554    11.5 |  1.514 % |
c |      7335 |  270508   726159 |  120032    6841    80150    11.7 |  1.529 % |
c ==============================================================================
c [1mFound solution: 9344[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7509 |  270527   726214 |   90175    7014    82212    11.7 |  1.529 % |
c |      7609 |  270527   726214 |   99192    7114    83021    11.7 |  1.530 % |
c |      7759 |  270513   726186 |  109111    7255    83949    11.6 |  1.536 % |
c ==============================================================================
c [1mFound solution: 9216[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7903 |  270505   726162 |   90168    7399    85692    11.6 |  1.536 % |
c |      8004 |  270503   726158 |   99184    7499    86620    11.6 |  1.543 % |
c |      8154 |  270503   726158 |  109103    7649    87526    11.4 |  1.543 % |
c |      8380 |  270485   726122 |  120013    7866    89920    11.4 |  1.551 % |
c ==============================================================================
c [1mFound solution: 8832[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8651 |  270514   726198 |   90171    8137    93675    11.5 |  1.551 % |
c |      8752 |  270510   726190 |   99188    8236    94931    11.5 |  1.553 % |
c |      8903 |  270510   726190 |  109106    8387    96278    11.5 |  1.553 % |
c |      9128 |  270510   726190 |  120017    8612   100395    11.7 |  1.553 % |
c |      9465 |  270510   726190 |  132019    8949   103347    11.5 |  1.553 % |
c |      9971 |  270510   726190 |  145221    9455   111202    11.8 |  1.553 % |
c |     10730 |  270510   726190 |  159743   10214   126020    12.3 |  1.553 % |
c |     11870 |  270508   726186 |  175717   11353   145407    12.8 |  1.553 % |
c ==============================================================================
c [1mFound solution: 8704[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12657 |  270468   726088 |   90156   12132   159717    13.2 |  1.553 % |
c |     12757 |  270466   726084 |   99171   12231   160888    13.2 |  1.575 % |
c |     12907 |  270464   726080 |  109088   12380   164760    13.3 |  1.576 % |
c |     13132 |  270464   726080 |  119997   12605   169071    13.4 |  1.576 % |
c |     13469 |  270464   726080 |  131997   12942   173106    13.4 |  1.576 % |
c |     13975 |  270464   726080 |  145197   13448   182789    13.6 |  1.576 % |
c |     14735 |  270454   726060 |  159716   14203   191478    13.5 |  1.580 % |
c |     15875 |  270454   726060 |  175688   15343   227684    14.8 |  1.580 % |
c |     17583 |  270452   726056 |  193257   17050   254617    14.9 |  1.581 % |
c |     20145 |  270376   725904 |  212583   19571   307342    15.7 |  1.611 % |
c |     23990 |  270180   725512 |  233841   23315   365062    15.7 |  1.688 % |
c |     29756 |  270162   725476 |  257225   29072   615918    21.2 |  1.695 % |
c |     38406 |  270118   725388 |  282948   37700   809203    21.5 |  1.712 % |
c |     51380 |  269976   725104 |  311242   50603  1112740    22.0 |  1.768 % |
c ==============================================================================
c [1mFound solution: 8576[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64893 |  269956   725073 |   89985   64100  1390090    21.7 |  1.768 % |
c |     64994 |  269954   725069 |   98983   64200  1390939    21.7 |  1.782 % |
c |     65144 |  269910   724981 |  108881   64328  1393826    21.7 |  1.799 % |
c |     65369 |  269910   724981 |  119770   64553  1398029    21.7 |  1.799 % |
c |     65706 |  269906   724973 |  131747   64888  1403813    21.6 |  1.801 % |
c |     66212 |  269906   724973 |  144921   65394  1410520    21.6 |  1.801 % |
c |     66971 |  269904   724969 |  159413   66152  1432391    21.7 |  1.801 % |
c ==============================================================================
c [1mFound solution: 8448[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67547 |  269890   724928 |   89963   66712  1454069    21.8 |  1.801 % |
c |     67648 |  269890   724928 |   98959   66813  1455502    21.8 |  1.812 % |
c |     67799 |  269890   724928 |  108855   66964  1456679    21.8 |  1.812 % |
c |     68024 |  269890   724928 |  119740   67189  1478662    22.0 |  1.812 % |
c |     68361 |  269890   724928 |  131714   67526  1485354    22.0 |  1.812 % |
c |     68867 |  269882   724912 |  144886   68028  1494406    22.0 |  1.815 % |
c |     69626 |  269880   724908 |  159374   68786  1508964    21.9 |  1.816 % |
c |     70766 |  269878   724904 |  175312   69925  1538691    22.0 |  1.816 % |
c ==============================================================================
c [1mFound solution: 8320[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70863 |  269891   724939 |   89963   70022  1540321    22.0 |  1.816 % |
c |     70963 |  269891   724939 |   98959   70122  1541348    22.0 |  1.817 % |
c |     71114 |  269887   724931 |  108855   70271  1542942    22.0 |  1.818 % |
c |     71339 |  269885   724927 |  119740   70495  1549185    22.0 |  1.819 % |
c |     71676 |  269885   724927 |  131714   70832  1555221    22.0 |  1.819 % |
c |     72183 |  269885   724927 |  144886   71339  1577780    22.1 |  1.819 % |
c |     72944 |  269877   724911 |  159374   72094  1595857    22.1 |  1.822 % |
c |     74083 |  269877   724911 |  175312   73233  1644113    22.5 |  1.822 % |
c |     75793 |  269873   724903 |  192843   74941  1716056    22.9 |  1.824 % |
c ==============================================================================
c [1mFound solution: 8192[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76191 |  269840   724821 |   89946   75322  1722648    22.9 |  1.824 % |
c |     76292 |  269840   724821 |   98940   75423  1723500    22.9 |  1.844 % |
c |     76444 |  269840   724821 |  108834   75575  1735953    23.0 |  1.844 % |
c |     76669 |  269840   724821 |  119718   75800  1740543    23.0 |  1.844 % |
c |     77007 |  269840   724821 |  131689   76138  1747050    22.9 |  1.844 % |
c |     77513 |  269840   724821 |  144858   76644  1756948    22.9 |  1.844 % |
c |     78272 |  269840   724821 |  159344   77403  1769077    22.9 |  1.844 % |
c |     79412 |  269840   724821 |  175279   78543  1823965    23.2 |  1.844 % |
c |     81120 |  269840   724821 |  192807   80251  2039997    25.4 |  1.844 % |
c |     83682 |  269838   724817 |  212087   82812  2326326    28.1 |  1.844 % |
c |     87526 |  269838   724817 |  233296   86656  2852355    32.9 |  1.844 % |
c |     93292 |  269832   724805 |  256626   92419  3421598    37.0 |  1.847 % |
c |    101942 |  269818   724777 |  282289  101061  4162704    41.2 |  1.852 % |
c |    114917 |  269810   724761 |  310517  114032  5661008    49.6 |  1.855 % |
c |    134378 |  269786   724713 |  341569  133481  6993950    52.4 |  1.865 % |
c |    163570 |  269770   724681 |  375726  162665  9345925    57.5 |  1.871 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 12267 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.93 0.98 0.91 2/54 12263
Raw data (stat): 12263 (runsolver) R 12262 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784857237 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.001 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0032 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.018 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.018 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.018 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.019 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.019 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.022 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 12267
Raw data (stat): 12263 (minisat+_script) S 12262 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784857237 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.87
CPU user time (s): 1229.01
CPU system time (s): 0.867868
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####