PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-berlin_5_8_0.opb
MD5SUM	9a578fa18e88cebdbf227cdbb9fbab5f
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	84992
Optimality of the best value was proved	NO
Number of terms in the objective function	78
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	1073790975
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1024000000
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	2147979262
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1200.77
Number of variables	9464
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	61
Trace number 30934

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-05-25 20:57:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22332 boxname=wulflinc17 idbench=1148 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  9a578fa18e88cebdbf227cdbb9fbab5f  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-berlin_5_8_0.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-berlin_5_8_0.opb
IDLAUNCH: 22332
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        887992 kB
Buffers:         21484 kB
Cached:         102404 kB
SwapCached:        484 kB
Active:          19812 kB
Inactive:       106204 kB
HighTotal:      131008 kB
HighFree:        27804 kB
LowTotal:       903652 kB
LowFree:        860188 kB
SwapTotal:     2097892 kB
SwapFree:      2096560 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            14848 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:18:06 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22332 7 1229.88 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:  122
c ---[1814]---> BDD-cost:  149
c ---[1813]---> BDD-cost:  127
c ---[1812]---> BDD-cost:  139
c ---[1811]---> BDD-cost:  131
c ---[1810]---> BDD-cost:  146
c ---[1809]---> BDD-cost:  134
c ---[1808]---> BDD-cost:  133
c ---[1807]---> BDD-cost:  137
c ---[1806]---> BDD-cost:  149
c ---[1804]---> BDD-cost:  137
c ---[1803]---> BDD-cost:  143
c ---[1802]---> BDD-cost:  137
c ---[1801]---> BDD-cost:  136
c ---[1800]---> BDD-cost:  137
c ---[1799]---> BDD-cost:  149
c ---[1798]---> BDD-cost:  137
c ---[1797]---> BDD-cost:  149
c ---[1796]---> BDD-cost:  129
c ---[1795]---> BDD-cost:  149
c ---[1793]---> BDD-cost:  137
c ---[1792]---> BDD-cost:  144
c ---[1791]---> BDD-cost:  122
c ---[1790]---> BDD-cost:  132
c ---[1789]---> BDD-cost:  129
c ---[1788]---> BDD-cost:  149
c ---[1787]---> BDD-cost:  137
c ---[1786]---> BDD-cost:  144
c ---[1785]---> BDD-cost:  137
c ---[1784]---> BDD-cost:  140
c ---[1782]---> BDD-cost:  140
c ---[1781]---> BDD-cost:  140
c ---[1780]---> BDD-cost:  114
c ---[1779]---> BDD-cost:  114
c ---[1778]---> BDD-cost:  140
c ---[1777]---> BDD-cost:  140
c ---[1776]---> BDD-cost:  149
c ---[1775]---> BDD-cost:  149
c ---[1774]---> BDD-cost:  137
c ---[1773]---> BDD-cost:  114
c ---[1771]---> BDD-cost:  137
c ---[1770]---> BDD-cost:  141
c ---[1769]---> BDD-cost:  122
c ---[1768]---> BDD-cost:  141
c ---[1767]---> BDD-cost:  137
c ---[1766]---> BDD-cost:  146
c ---[1765]---> BDD-cost:  122
c ---[1764]---> BDD-cost:  149
c ---[1763]---> BDD-cost:  124
c ---[1762]---> BDD-cost:  146
c ---[1760]---> BDD-cost:  137
c ---[1759]---> BDD-cost:  144
c ---[1758]---> BDD-cost:  131
c ---[1757]---> BDD-cost:  143
c ---[1756]---> BDD-cost:  137
c ---[1755]---> BDD-cost:  144
c ---[1754]---> BDD-cost:  132
c ---[1753]---> BDD-cost:  149
c ---[1752]---> BDD-cost:  127
c ---[1751]---> BDD-cost:  141
c ---[1749]---> BDD-cost:  122
c ---[1748]---> BDD-cost:  146
c ---[1747]---> BDD-cost:  137
c ---[1746]---> BDD-cost:  143
c ---[1745]---> BDD-cost:  122
c ---[1744]---> BDD-cost:  128
c ---[1743]---> BDD-cost:  131
c ---[1742]---> BDD-cost:  136
c ---[1741]---> BDD-cost:  132
c ---[1740]---> BDD-cost:  146
c ---[1738]---> BDD-cost:  137
c ---[1737]---> BDD-cost:  131
c ---[1736]---> BDD-cost:  131
c ---[1735]---> BDD-cost:  143
c ---[1734]---> BDD-cost:  126
c ---[1733]---> BDD-cost:  144
c ---[1732]---> BDD-cost:  140
c ---[1731]---> BDD-cost:  140
c ---[1730]---> BDD-cost:  149
c ---[1729]---> BDD-cost:  140
c ---[1727]---> BDD-cost:  140
c ---[1726]---> BDD-cost:  149
c ---[1725]---> BDD-cost:  122
c ---[1724]---> BDD-cost:  136
c ---[1723]---> BDD-cost:  129
c ---[1722]---> BDD-cost:  146
c ---[1721]---> BDD-cost:  132
c ---[1720]---> BDD-cost:  141
c ---[1719]---> BDD-cost:  137
c ---[1718]---> BDD-cost:  141
c ---[1716]---> BDD-cost:  134
c ---[1715]---> BDD-cost:  120
c ---[1714]---> BDD-cost:  132
c ---[1713]---> BDD-cost:  143
c ---[1712]---> BDD-cost:  131
c ---[1711]---> BDD-cost:  146
c ---[1710]---> BDD-cost:  129
c ---[1709]---> BDD-cost:  123
c ---[1708]---> BDD-cost:  129
c ---[1707]---> BDD-cost:  143
c ---[1704]---> BDD-cost:  132
c ---[1703]---> BDD-cost:  149
c ---[1702]---> BDD-cost:  132
c ---[1701]---> BDD-cost:  149
c ---[1700]---> BDD-cost:  134
c ---[1699]---> BDD-cost:  136
c ---[1698]---> BDD-cost:  131
c ---[1697]---> BDD-cost:  149
c ---[1696]---> BDD-cost:  140
c ---[1695]---> BDD-cost:  140
c ---[1693]---> BDD-cost:  144
c ---[1692]---> BDD-cost:  144
c ---[1691]---> BDD-cost:  124
c ---[1690]---> BDD-cost:  146
c ---[1689]---> BDD-cost:  127
c ---[1688]---> BDD-cost:  144
c ---[1687]---> BDD-cost:  124
c ---[1686]---> BDD-cost:  131
c ---[1685]---> BDD-cost:  140
c ---[1684]---> BDD-cost:  140
c ---[1682]---> BDD-cost:  146
c ---[1681]---> BDD-cost:  129
c ---[1680]---> BDD-cost:  149
c ---[1679]---> BDD-cost:  124
c ---[1678]---> BDD-cost:  131
c ---[1677]---> BDD-cost:  124
c ---[1676]---> BDD-cost:  149
c ---[1675]---> BDD-cost:  132
c ---[1674]---> BDD-cost:  149
c ---[1673]---> BDD-cost:  129
c ---[1671]---> BDD-cost:  146
c ---[1670]---> BDD-cost:  137
c ---[1669]---> BDD-cost:  136
c ---[1668]---> BDD-cost:  134
c ---[1667]---> BDD-cost:  134
c ---[1666]---> BDD-cost:  137
c ---[1665]---> BDD-cost:  139
c ---[1664]---> BDD-cost:  120
c ---[1663]---> BDD-cost:  146
c ---[1662]---> BDD-cost:  132
c ---[1660]---> BDD-cost:  133
c ---[1659]---> BDD-cost:  129
c ---[1658]---> BDD-cost:  143
c ---[1657]---> BDD-cost:  137
c ---[1656]---> BDD-cost:  140
c ---[1655]---> BDD-cost:  134
c ---[1654]---> BDD-cost:  131
c ---[1653]---> BDD-cost:  131
c ---[1652]---> BDD-cost:  146
c ---[1651]---> BDD-cost:  131
c ---[1649]---> BDD-cost:  149
c ---[1648]---> BDD-cost:  129
c ---[1647]---> BDD-cost:  133
c ---[1646]---> BDD-cost:  137
c ---[1645]---> BDD-cost:  149
c ---[1644]---> BDD-cost:  126
c ---[1643]---> BDD-cost:  134
c ---[1642]---> BDD-cost:  140
c ---[1641]---> BDD-cost:  140
c ---[1640]---> BDD-cost:  137
c ---[1638]---> BDD-cost:  137
c ---[1637]---> BDD-cost:  140
c ---[1636]---> BDD-cost:  137
c ---[1635]---> BDD-cost:  143
c ---[1634]---> BDD-cost:  137
c ---[1633]---> BDD-cost:  131
c ---[1632]---> BDD-cost:  131
c ---[1631]---> BDD-cost:  138
c ---[1630]---> BDD-cost:  131
c ---[1629]---> BDD-cost:  140
c ---[1627]---> BDD-cost:  137
c ---[1626]---> BDD-cost:  136
c ---[1625]---> BDD-cost:  131
c ---[1624]---> BDD-cost:  133
c ---[1623]---> BDD-cost:  137
c ---[1622]---> BDD-cost:  146
c ---[1621]---> BDD-cost:  137
c ---[1620]---> BDD-cost:  130
c ---[1619]---> BDD-cost:  134
c ---[1618]---> BDD-cost:  143
c ---[1616]---> BDD-cost:  134
c ---[1615]---> BDD-cost:  128
c ---[1614]---> BDD-cost:  137
c ---[1613]---> BDD-cost:  143
c ---[1612]---> BDD-cost:  124
c ---[1611]---> BDD-cost:  141
c ---[1610]---> BDD-cost:  137
c ---[1609]---> BDD-cost:  146
c ---[1608]---> BDD-cost:  126
c ---[1607]---> BDD-cost:  146
c ---[1605]---> BDD-cost:  126
c ---[1604]---> BDD-cost:  140
c ---[1603]---> BDD-cost:  137
c ---[1602]---> BDD-cost:  149
c ---[1601]---> BDD-cost:  126
c ---[1600]---> BDD-cost:  144
c ---[1599]---> BDD-cost:  134
c ---[1598]---> BDD-cost:  139
c ---[1597]---> BDD-cost:  127
c ---[1596]---> BDD-cost:  146
c ---[1593]---> BDD-cost:  126
c ---[1592]---> BDD-cost:  144
c ---[1591]---> BDD-cost:  137
c ---[1590]---> BDD-cost:  149
c ---[1589]---> BDD-cost:  137
c ---[1588]---> BDD-cost:  144
c ---[1587]---> BDD-cost:  124
c ---[1586]---> BDD-cost:  146
c ---[1585]---> BDD-cost:  127
c ---[1584]---> BDD-cost:  143
c ---[1582]---> BDD-cost:  127
c ---[1581]---> BDD-cost:  139
c ---[1580]---> BDD-cost:  134
c ---[1579]---> BDD-cost:  146
c ---[1578]---> BDD-cost:  134
c ---[1577]---> BDD-cost:  139
c ---[1576]---> BDD-cost:  137
c ---[1575]---> BDD-cost:  149
c ---[1574]---> BDD-cost:  134
c ---[1573]---> BDD-cost:  149
c ---[1571]---> BDD-cost:  140
c ---[1570]---> BDD-cost:  140
c ---[1569]---> BDD-cost:  144
c ---[1568]---> BDD-cost:  144
c ---[1567]---> BDD-cost:  126
c ---[1566]---> BDD-cost:  138
c ---[1565]---> BDD-cost:  134
c ---[1564]---> BDD-cost:  144
c ---[1563]---> BDD-cost:  140
c ---[1562]---> BDD-cost:  140
c ---[1560]---> BDD-cost:  143
c ---[1559]---> BDD-cost:  137
c ---[1558]---> BDD-cost:  134
c ---[1557]---> BDD-cost:  137
c ---[1556]---> BDD-cost:  149
c ---[1555]---> BDD-cost:  137
c ---[1554]---> BDD-cost:  134
c ---[1553]---> BDD-cost:  140
c ---[1552]---> BDD-cost:  140
c ---[1551]---> BDD-cost:  130
c ---[1549]---> BDD-cost:  137
c ---[1548]---> BDD-cost:  146
c ---[1547]---> BDD-cost:  140
c ---[1546]---> BDD-cost:  140
c ---[1545]---> BDD-cost:  143
c ---[1544]---> BDD-cost:  132
c ---[1543]---> BDD-cost:  146
c ---[1542]---> BDD-cost:  134
c ---[1541]---> BDD-cost:  141
c ---[1540]---> BDD-cost:  127
c ---[1538]---> BDD-cost:  138
c ---[1537]---> BDD-cost:  132
c ---[1536]---> BDD-cost:  146
c ---[1535]---> BDD-cost:  137
c ---[1534]---> BDD-cost:  138
c ---[1533]---> BDD-cost:  134
c ---[1532]---> BDD-cost:  143
c ---[1531]---> BDD-cost:  137
c ---[1530]---> BDD-cost:  128
c ---[1529]---> BDD-cost:  137
c ---[1527]---> BDD-cost:  143
c ---[1526]---> BDD-cost:  137
c ---[1525]---> BDD-cost:  128
c ---[1524]---> BDD-cost:  137
c ---[1523]---> BDD-cost:  144
c ---[1522]---> BDD-cost:  140
c ---[1521]---> BDD-cost:  140
c ---[1520]---> BDD-cost:  141
c ---[1519]---> BDD-cost:  141
c ---[1518]---> BDD-cost:  132
c ---[1516]---> BDD-cost:  144
c ---[1515]---> BDD-cost:  134
c ---[1514]---> BDD-cost:  149
c ---[1513]---> BDD-cost:  132
c ---[1512]---> BDD-cost:  144
c ---[1511]---> BDD-cost:  137
c ---[1510]---> BDD-cost:  146
c ---[1509]---> BDD-cost:  137
c ---[1508]---> BDD-cost:  146
c ---[1507]---> BDD-cost:  137
c ---[1505]---> BDD-cost:  126
c ---[1504]---> BDD-cost:  137
c ---[1503]---> BDD-cost:  146
c ---[1502]---> BDD-cost:  127
c ---[1501]---> BDD-cost:  146
c ---[1500]---> BDD-cost:  127
c ---[1499]---> BDD-cost:  141
c ---[1498]---> BDD-cost:  137
c ---[1497]---> BDD-cost:  131
c ---[1496]---> BDD-cost:  120
c ---[1494]---> BDD-cost:  140
c ---[1493]---> BDD-cost:  134
c ---[1492]---> BDD-cost:  146
c ---[1491]---> BDD-cost:  137
c ---[1490]---> BDD-cost:  133
c ---[1489]---> BDD-cost:  120
c ---[1488]---> BDD-cost:  141
c ---[1487]---> BDD-cost:  140
c ---[1486]---> BDD-cost:  140
c ---[1485]---> BDD-cost:  149
c ---[1482]---> BDD-cost:  122
c ---[1481]---> BDD-cost:  124
c ---[1480]---> BDD-cost:  129
c ---[1479]---> BDD-cost:  149
c ---[1478]---> BDD-cost:  132
c ---[1477]---> BDD-cost:  144
c ---[1476]---> BDD-cost:  137
c ---[1475]---> BDD-cost:  141
c ---[1474]---> BDD-cost:  134
c ---[1473]---> BDD-cost:  133
c ---[1471]---> BDD-cost:  132
c ---[1470]---> BDD-cost:  146
c ---[1469]---> BDD-cost:  131
c ---[1468]---> BDD-cost:  146
c ---[1467]---> BDD-cost:  137
c ---[1466]---> BDD-cost:  149
c ---[1465]---> BDD-cost:  126
c ---[1464]---> BDD-cost:  149
c ---[1463]---> BDD-cost:  149
c ---[1462]---> BDD-cost:  137
c ---[1460]---> BDD-cost:  144
c ---[1459]---> BDD-cost:  124
c ---[1458]---> BDD-cost:  138
c ---[1457]---> BDD-cost:  126
c ---[1456]---> BDD-cost:  149
c ---[1455]---> BDD-cost:  149
c ---[1454]---> BDD-cost:  134
c ---[1453]---> BDD-cost:  134
c ---[1452]---> BDD-cost:  137
c ---[1451]---> BDD-cost:  146
c ---[1449]---> BDD-cost:  137
c ---[1448]---> BDD-cost:  129
c ---[1447]---> BDD-cost:  137
c ---[1446]---> BDD-cost:  149
c ---[1445]---> BDD-cost:  140
c ---[1444]---> BDD-cost:  140
c ---[1443]---> BDD-cost:  144
c ---[1442]---> BDD-cost:  144
c ---[1441]---> BDD-cost:  132
c ---[1440]---> BDD-cost:  149
c ---[1438]---> BDD-cost:  134
c ---[1437]---> BDD-cost:  144
c ---[1436]---> BDD-cost:  127
c ---[1435]---> BDD-cost:  129
c ---[1434]---> BDD-cost:  132
c ---[1433]---> BDD-cost:  149
c ---[1432]---> BDD-cost:  137
c ---[1431]---> BDD-cost:  139
c ---[1430]---> BDD-cost:  134
c ---[1429]---> BDD-cost:  137
c ---[1427]---> BDD-cost:  137
c ---[1426]---> BDD-cost:  131
c ---[1425]---> BDD-cost:  137
c ---[1424]---> BDD-cost:  149
c ---[1423]---> BDD-cost:  137
c ---[1422]---> BDD-cost:  141
c ---[1421]---> BDD-cost:  134
c ---[1420]---> BDD-cost:  141
c ---[1419]---> BDD-cost:  132
c ---[1418]---> BDD-cost:  138
c ---[1416]---> BDD-cost:  132
c ---[1415]---> BDD-cost:  146
c ---[1414]---> BDD-cost:  131
c ---[1413]---> BDD-cost:  141
c ---[1412]---> BDD-cost:  132
c ---[1411]---> BDD-cost:  149
c ---[1410]---> BDD-cost:  132
c ---[1409]---> BDD-cost:  143
c ---[1408]---> BDD-cost:  129
c ---[1407]---> BDD-cost:  143
c ---[1405]---> BDD-cost:  122
c ---[1404]---> BDD-cost:  144
c ---[1403]---> BDD-cost:  134
c ---[1402]---> BDD-cost:  146
c ---[1401]---> BDD-cost:  129
c ---[1400]---> BDD-cost:  140
c ---[1399]---> BDD-cost:  122
c ---[1398]---> BDD-cost:  134
c ---[1397]---> BDD-cost:  129
c ---[1396]---> BDD-cost:  149
c ---[1394]---> BDD-cost:  132
c ---[1393]---> BDD-cost:  129
c ---[1392]---> BDD-cost:  137
c ---[1391]---> BDD-cost:  131
c ---[1390]---> BDD-cost:  134
c ---[1389]---> BDD-cost:  138
c ---[1388]---> BDD-cost:  132
c ---[1387]---> BDD-cost:  146
c ---[1386]---> BDD-cost:  131
c ---[1385]---> BDD-cost:  146
c ---[1383]---> BDD-cost:  137
c ---[1382]---> BDD-cost:  131
c ---[1381]---> BDD-cost:  134
c ---[1380]---> BDD-cost:  146
c ---[1379]---> BDD-cost:  132
c ---[1378]---> BDD-cost:  146
c ---[1377]---> BDD-cost:  120
c ---[1376]---> BDD-cost:  131
c ---[1375]---> BDD-cost:  134
c ---[1374]---> BDD-cost:  138
c ---[1371]---> BDD-cost:  129
c ---[1370]---> BDD-cost:  136
c ---[1369]---> BDD-cost:  137
c ---[1368]---> BDD-cost:  135
c ---[1367]---> BDD-cost:  140
c ---[1366]---> BDD-cost:  140
c ---[1365]---> BDD-cost:  149
c ---[1364]---> BDD-cost:  149
c ---[1363]---> BDD-cost:  127
c ---[1362]---> BDD-cost:  129
c ---[1360]---> BDD-cost:  129
c ---[1359]---> BDD-cost:  134
c ---[1358]---> BDD-cost:  129
c ---[1357]---> BDD-cost:  149
c ---[1356]---> BDD-cost:  129
c ---[1355]---> BDD-cost:  139
c ---[1354]---> BDD-cost:  129
c ---[1353]---> BDD-cost:  141
c ---[1352]---> BDD-cost:  126
c ---[1351]---> BDD-cost:  144
c ---[1349]---> BDD-cost:  144
c ---[1348]---> BDD-cost:  131
c ---[1347]---> BDD-cost:  144
c ---[1346]---> BDD-cost:  122
c ---[1345]---> BDD-cost:  144
c ---[1344]---> BDD-cost:  120
c ---[1343]---> BDD-cost:  141
c ---[1342]---> BDD-cost:  131
c ---[1341]---> BDD-cost:  149
c ---[1340]---> BDD-cost:  122
c ---[1338]---> BDD-cost:  140
c ---[1337]---> BDD-cost:  124
c ---[1336]---> BDD-cost:  141
c ---[1335]---> BDD-cost:  127
c ---[1334]---> BDD-cost:  149
c ---[1333]---> BDD-cost:  124
c ---[1332]---> BDD-cost:  146
c ---[1331]---> BDD-cost:  140
c ---[1330]---> BDD-cost:  140
c ---[1329]---> BDD-cost:  136
c ---[1327]---> BDD-cost:  129
c ---[1326]---> BDD-cost:  144
c ---[1325]---> BDD-cost:  124
c ---[1324]---> BDD-cost:  139
c ---[1323]---> BDD-cost:  126
c ---[1322]---> BDD-cost:  140
c ---[1321]---> BDD-cost:  134
c ---[1320]---> BDD-cost:  149
c ---[1319]---> BDD-cost:  140
c ---[1318]---> BDD-cost:  140
c ---[1316]---> BDD-cost:  128
c ---[1315]---> BDD-cost:  137
c ---[1314]---> BDD-cost:  149
c ---[1313]---> BDD-cost:  137
c ---[1312]---> BDD-cost:  144
c ---[1311]---> BDD-cost:  137
c ---[1310]---> BDD-cost:  149
c ---[1309]---> BDD-cost:  124
c ---[1308]---> BDD-cost:  146
c ---[1307]---> BDD-cost:  124
c ---[1305]---> BDD-cost:  143
c ---[1304]---> BDD-cost:  137
c ---[1303]---> BDD-cost:  146
c ---[1302]---> BDD-cost:  140
c ---[1301]---> BDD-cost:  140
c ---[1300]---> BDD-cost:  146
c ---[1299]---> BDD-cost:  137
c ---[1298]---> BDD-cost:  146
c ---[1297]---> BDD-cost:  127
c ---[1296]---> BDD-cost:  131
c ---[1294]---> BDD-cost:  137
c ---[1293]---> BDD-cost:  135
c ---[1292]---> BDD-cost:  126
c ---[1291]---> BDD-cost:  131
c ---[1290]---> BDD-cost:  126
c ---[1289]---> BDD-cost:  146
c ---[1288]---> BDD-cost:  122
c ---[1287]---> BDD-cost:  132
c ---[1286]---> BDD-cost:  124
c ---[1285]---> BDD-cost:  140
c ---[1283]---> BDD-cost:  124
c ---[1282]---> BDD-cost:  149
c ---[1281]---> BDD-cost:  127
c ---[1280]---> BDD-cost:  129
c ---[1279]---> BDD-cost:  129
c ---[1278]---> BDD-cost:  134
c ---[1277]---> BDD-cost:  129
c ---[1276]---> BDD-cost:  149
c ---[1275]---> BDD-cost:  129
c ---[1274]---> BDD-cost:  139
c ---[1272]---> BDD-cost:  129
c ---[1271]---> BDD-cost:  141
c ---[1270]---> BDD-cost:  126
c ---[1269]---> BDD-cost:  144
c ---[1268]---> BDD-cost:  144
c ---[1267]---> BDD-cost:  134
c ---[1266]---> BDD-cost:  122
c ---[1265]---> BDD-cost:  137
c ---[1264]---> BDD-cost:  146
c ---[1263]---> BDD-cost:  137
c ---[1260]---> BDD-cost:  141
c ---[1259]---> BDD-cost:  134
c ---[1258]---> BDD-cost:  146
c ---[1257]---> BDD-cost:  126
c ---[1256]---> BDD-cost:  149
c ---[1255]---> BDD-cost:  124
c ---[1254]---> BDD-cost:  136
c ---[1253]---> BDD-cost:  129
c ---[1252]---> BDD-cost:  146
c ---[1251]---> BDD-cost:  124
c ---[1249]---> BDD-cost:  140
c ---[1248]---> BDD-cost:  124
c ---[1247]---> BDD-cost:  149
c ---[1246]---> BDD-cost:  137
c ---[1245]---> BDD-cost:  129
c ---[1244]---> BDD-cost:  137
c ---[1243]---> BDD-cost:  140
c ---[1242]---> BDD-cost:  137
c ---[1241]---> BDD-cost:  129
c ---[1240]---> BDD-cost:  137
c ---[1238]---> BDD-cost:  149
c ---[1237]---> BDD-cost:  140
c ---[1236]---> BDD-cost:  140
c ---[1235]---> BDD-cost:  136
c ---[1234]---> BDD-cost:  136
c ---[1233]---> BDD-cost:  137
c ---[1232]---> BDD-cost:  146
c ---[1231]---> BDD-cost:  137
c ---[1230]---> BDD-cost:  136
c ---[1229]---> BDD-cost:  140
c ---[1227]---> BDD-cost:  140
c ---[1226]---> BDD-cost:  146
c ---[1051]---> BDD-cost:  119
c ---[1050]---> BDD-cost:  119
c ---[1049]---> BDD-cost:   88
c ---[1048]---> BDD-cost:   88
c ---[1047]---> BDD-cost:   88
c ---[1046]---> BDD-cost:   88
c ---[1045]---> BDD-cost:  119
c ---[1044]---> BDD-cost:  119
c ---[1043]---> BDD-cost:   88
c ---[1042]---> BDD-cost:   88
c ---[1040]---> BDD-cost:   88
c ---[1039]---> BDD-cost:   88
c ---[1038]---> BDD-cost:  125
c ---[1037]---> BDD-cost:  119
c ---[1036]---> BDD-cost:   88
c ---[1035]---> BDD-cost:   88
c ---[1034]---> BDD-cost:   88
c ---[1033]---> BDD-cost:   88
c ---[1032]---> BDD-cost:  113
c ---[1031]---> BDD-cost:  119
c ---[1029]---> BDD-cost:   88
c ---[1028]---> BDD-cost:   88
c ---[1027]---> BDD-cost:   88
c ---[1026]---> BDD-cost:   88
c ---[1025]---> BDD-cost:  119
c ---[1024]---> BDD-cost:  119
c ---[1023]---> BDD-cost:   88
c ---[1022]---> BDD-cost:   88
c ---[1021]---> BDD-cost:   88
c ---[1020]---> BDD-cost:   88
c ---[1018]---> BDD-cost:  121
c ---[1017]---> BDD-cost:  119
c ---[1016]---> BDD-cost:   88
c ---[1015]---> BDD-cost:   88
c ---[1014]---> BDD-cost:   88
c ---[1013]---> BDD-cost:   88
c ---[1012]---> BDD-cost:  125
c ---[1011]---> BDD-cost:  119
c ---[1010]---> BDD-cost:   88
c ---[1009]---> BDD-cost:   88
c ---[1007]---> BDD-cost:   88
c ---[1006]---> BDD-cost:   88
c ---[1005]---> BDD-cost:  125
c ---[1004]---> BDD-cost:  119
c ---[1003]---> BDD-cost:   88
c ---[1002]---> BDD-cost:   88
c ---[1001]---> BDD-cost:   88
c ---[1000]---> BDD-cost:   88
c ---[ 999]---> BDD-cost:  115
c ---[ 998]---> BDD-cost:  119
c ---[ 996]---> BDD-cost:   88
c ---[ 995]---> BDD-cost:   88
c ---[ 994]---> BDD-cost:   88
c ---[ 993]---> BDD-cost:   88
c ---[ 992]---> BDD-cost:  123
c ---[ 991]---> BDD-cost:  119
c ---[ 990]---> BDD-cost:   88
c ---[ 989]---> BDD-cost:   88
c ---[ 988]---> BDD-cost:   88
c ---[ 987]---> BDD-cost:   88
c ---[ 985]---> BDD-cost:  125
c ---[ 984]---> BDD-cost:  119
c ---[ 983]---> BDD-cost:   88
c ---[ 982]---> BDD-cost:   88
c ---[ 981]---> BDD-cost:   88
c ---[ 980]---> BDD-cost:   88
c ---[ 979]---> BDD-cost:  123
c ---[ 978]---> BDD-cost:  119
c ---[ 977]---> BDD-cost:   88
c ---[ 976]---> BDD-cost:   88
c ---[ 974]---> BDD-cost:   88
c ---[ 973]---> BDD-cost:   88
c ---[ 972]---> BDD-cost:  123
c ---[ 971]---> BDD-cost:  119
c ---[ 970]---> BDD-cost:   88
c ---[ 969]---> BDD-cost:   88
c ---[ 968]---> BDD-cost:   88
c ---[ 967]---> BDD-cost:   88
c ---[ 966]---> BDD-cost:  117
c ---[ 965]---> BDD-cost:  119
c ---[ 963]---> BDD-cost:   88
c ---[ 962]---> BDD-cost:   88
c ---[ 961]---> BDD-cost:   88
c ---[ 960]---> BDD-cost:   88
c ---[ 959]---> BDD-cost:  125
c ---[ 958]---> BDD-cost:  119
c ---[ 957]---> BDD-cost:   88
c ---[ 956]---> BDD-cost:   88
c ---[ 955]---> BDD-cost:   88
c ---[ 954]---> BDD-cost:   88
c ---[ 951]---> BDD-cost:  125
c ---[ 950]---> BDD-cost:  119
c ---[ 949]---> BDD-cost:   88
c ---[ 948]---> BDD-cost:   88
c ---[ 947]---> BDD-cost:   88
c ---[ 946]---> BDD-cost:   88
c ---[ 945]---> BDD-cost:  119
c ---[ 944]---> BDD-cost:  119
c ---[ 943]---> BDD-cost:   88
c ---[ 942]---> BDD-cost:   88
c ---[ 940]---> BDD-cost:   88
c ---[ 939]---> BDD-cost:   88
c ---[ 938]---> BDD-cost:  125
c ---[ 937]---> BDD-cost:  119
c ---[ 936]---> BDD-cost:   88
c ---[ 935]---> BDD-cost:   88
c ---[ 934]---> BDD-cost:   88
c ---[ 933]---> BDD-cost:   88
c ---[ 932]---> BDD-cost:  125
c ---[ 931]---> BDD-cost:  119
c ---[ 929]---> BDD-cost:   88
c ---[ 928]---> BDD-cost:   88
c ---[ 927]---> BDD-cost:   88
c ---[ 926]---> BDD-cost:   88
c ---[ 925]---> BDD-cost:  123
c ---[ 924]---> BDD-cost:  119
c ---[ 923]---> BDD-cost:   88
c ---[ 922]---> BDD-cost:   88
c ---[ 921]---> BDD-cost:   88
c ---[ 920]---> BDD-cost:   88
c ---[ 918]---> BDD-cost:  125
c ---[ 917]---> BDD-cost:  119
c ---[ 916]---> BDD-cost:   88
c ---[ 915]---> BDD-cost:   88
c ---[ 914]---> BDD-cost:   88
c ---[ 913]---> BDD-cost:   88
c ---[ 912]---> BDD-cost:  119
c ---[ 911]---> BDD-cost:  119
c ---[ 910]---> BDD-cost:   88
c ---[ 909]---> BDD-cost:   88
c ---[ 907]---> BDD-cost:   88
c ---[ 906]---> BDD-cost:   88
c ---[ 905]---> BDD-cost:  125
c ---[ 904]---> BDD-cost:  119
c ---[ 903]---> BDD-cost:   88
c ---[ 902]---> BDD-cost:   88
c ---[ 901]---> BDD-cost:   88
c ---[ 900]---> BDD-cost:   88
c ---[ 899]---> BDD-cost:  125
c ---[ 898]---> BDD-cost:  119
c ---[ 896]---> BDD-cost:   88
c ---[ 895]---> BDD-cost:   88
c ---[ 894]---> BDD-cost:   88
c ---[ 893]---> BDD-cost:   88
c ---[ 892]---> BDD-cost:  121
c ---[ 891]---> BDD-cost:  119
c ---[ 890]---> BDD-cost:   88
c ---[ 889]---> BDD-cost:   88
c ---[ 888]---> BDD-cost:   88
c ---[ 887]---> BDD-cost:   88
c ---[ 885]---> BDD-cost:  125
c ---[ 884]---> BDD-cost:  119
c ---[ 883]---> BDD-cost:   88
c ---[ 882]---> BDD-cost:   88
c ---[ 881]---> BDD-cost:   88
c ---[ 880]---> BDD-cost:   88
c ---[ 879]---> BDD-cost:  125
c ---[ 878]---> BDD-cost:  119
c ---[ 877]---> BDD-cost:   88
c ---[ 876]---> BDD-cost:   88
c ---[ 874]---> BDD-cost:   88
c ---[ 873]---> BDD-cost:   88
c ---[ 872]---> BDD-cost:  125
c ---[ 871]---> BDD-cost:  119
c ---[ 870]---> BDD-cost:   88
c ---[ 869]---> BDD-cost:   88
c ---[ 868]---> BDD-cost:   88
c ---[ 867]---> BDD-cost:   88
c ---[ 866]---> BDD-cost:  125
c ---[ 865]---> BDD-cost:  119
c ---[ 863]---> BDD-cost:   88
c ---[ 862]---> BDD-cost:   88
c ---[ 861]---> BDD-cost:   88
c ---[ 860]---> BDD-cost:   88
c ---[ 859]---> BDD-cost:  125
c ---[ 858]---> BDD-cost:  119
c ---[ 857]---> BDD-cost:   88
c ---[ 856]---> BDD-cost:   88
c ---[ 855]---> BDD-cost:   88
c ---[ 854]---> BDD-cost:   88
c ---[ 852]---> BDD-cost:  125
c ---[ 851]---> BDD-cost:  119
c ---[ 850]---> BDD-cost:   88
c ---[ 849]---> BDD-cost:   88
c ---[ 848]---> BDD-cost:   88
c ---[ 847]---> BDD-cost:   88
c ---[ 846]---> BDD-cost:  117
c ---[ 845]---> BDD-cost:  119
c ---[ 844]---> BDD-cost:   88
c ---[ 843]---> BDD-cost:   88
c ---[ 840]---> BDD-cost:   88
c ---[ 839]---> BDD-cost:   88
c ---[ 838]---> BDD-cost:  125
c ---[ 837]---> BDD-cost:  119
c ---[ 836]---> BDD-cost:   88
c ---[ 835]---> BDD-cost:   88
c ---[ 834]---> BDD-cost:   88
c ---[ 833]---> BDD-cost:   88
c ---[ 832]---> BDD-cost:  125
c ---[ 831]---> BDD-cost:  119
c ---[ 829]---> BDD-cost:   88
c ---[ 828]---> BDD-cost:   88
c ---[ 827]---> BDD-cost:   88
c ---[ 826]---> BDD-cost:   88
c ---[ 825]---> BDD-cost:  123
c ---[ 824]---> BDD-cost:  119
c ---[ 823]---> BDD-cost:   88
c ---[ 822]---> BDD-cost:   88
c ---[ 821]---> BDD-cost:   88
c ---[ 820]---> BDD-cost:   88
c ---[ 818]---> BDD-cost:  125
c ---[ 817]---> BDD-cost:  119
c ---[ 816]---> BDD-cost:   88
c ---[ 815]---> BDD-cost:   88
c ---[ 814]---> BDD-cost:   88
c ---[ 813]---> BDD-cost:   88
c ---[ 812]---> BDD-cost:  125
c ---[ 811]---> BDD-cost:  119
c ---[ 810]---> BDD-cost:   88
c ---[ 809]---> BDD-cost:   88
c ---[ 807]---> BDD-cost:   88
c ---[ 806]---> BDD-cost:   88
c ---[ 805]---> BDD-cost:  119
c ---[ 804]---> BDD-cost:  119
c ---[ 803]---> BDD-cost:   88
c ---[ 802]---> BDD-cost:   88
c ---[ 801]---> BDD-cost:   88
c ---[ 800]---> BDD-cost:   88
c ---[ 799]---> BDD-cost:  125
c ---[ 798]---> BDD-cost:  119
c ---[ 796]---> BDD-cost:   88
c ---[ 795]---> BDD-cost:   88
c ---[ 794]---> BDD-cost:   88
c ---[ 793]---> BDD-cost:   88
c ---[ 792]---> BDD-cost:  125
c ---[ 791]---> BDD-cost:  119
c ---[ 790]---> BDD-cost:   88
c ---[ 789]---> BDD-cost:   88
c ---[ 788]---> BDD-cost:   88
c ---[ 787]---> BDD-cost:   88
c ---[ 785]---> BDD-cost:  125
c ---[ 784]---> BDD-cost:  119
c ---[ 783]---> BDD-cost:   88
c ---[ 782]---> BDD-cost:   88
c ---[ 781]---> BDD-cost:   88
c ---[ 780]---> BDD-cost:   88
c ---[ 779]---> BDD-cost:  125
c ---[ 778]---> BDD-cost:  119
c ---[ 777]---> BDD-cost:   88
c ---[ 776]---> BDD-cost:   88
c ---[ 774]---> BDD-cost:   88
c ---[ 773]---> BDD-cost:   88
c ---[ 772]---> BDD-cost:  121
c ---[ 771]---> BDD-cost:  119
c ---[ 770]---> BDD-cost:   88
c ---[ 769]---> BDD-cost:   88
c ---[ 768]---> BDD-cost:   88
c ---[ 767]---> BDD-cost:   88
c ---[ 766]---> BDD-cost:  125
c ---[ 765]---> BDD-cost:  119
c ---[ 763]---> BDD-cost:   88
c ---[ 762]---> BDD-cost:   88
c ---[ 761]---> BDD-cost:   88
c ---[ 760]---> BDD-cost:   88
c ---[ 759]---> BDD-cost:  117
c ---[ 758]---> BDD-cost:  119
c ---[ 757]---> BDD-cost:   88
c ---[ 756]---> BDD-cost:   88
c ---[ 755]---> BDD-cost:   88
c ---[ 754]---> BDD-cost:   88
c ---[ 752]---> BDD-cost:  125
c ---[ 751]---> BDD-cost:  119
c ---[ 750]---> BDD-cost:   88
c ---[ 749]---> BDD-cost:   88
c ---[ 748]---> BDD-cost:   88
c ---[ 747]---> BDD-cost:   88
c ---[ 746]---> BDD-cost:  123
c ---[ 745]---> BDD-cost:  119
c ---[ 744]---> BDD-cost:   88
c ---[ 743]---> BDD-cost:   88
c ---[ 741]---> BDD-cost:   88
c ---[ 740]---> BDD-cost:   88
c ---[ 739]---> BDD-cost:  125
c ---[ 738]---> BDD-cost:  119
c ---[ 737]---> BDD-cost:   88
c ---[ 736]---> BDD-cost:   88
c ---[ 735]---> BDD-cost:   88
c ---[ 734]---> BDD-cost:   88
c ---[ 732]---> BDD-cost:  123
c ---[ 728]---> BDD-cost:  125
c ---[ 726]---> BDD-cost:  121
c ---[ 724]---> BDD-cost:   88
c ---[ 722]---> BDD-cost:  125
c ---[ 720]---> BDD-cost:   88
c ---[ 717]---> BDD-cost:  123
c ---[ 715]---> BDD-cost:   88
c ---[ 713]---> BDD-cost:   88
c ---[ 711]---> BDD-cost:   88
c ---[ 709]---> BDD-cost:  125
c ---[ 706]---> BDD-cost:   88
c ---[ 704]---> BDD-cost:   88
c ---[ 702]---> BDD-cost:  123
c ---[ 700]---> BDD-cost:   88
c ---[ 698]---> BDD-cost:  121
c ---[ 695]---> BDD-cost:  123
c ---[ 693]---> BDD-cost:  125
c ---[ 691]---> BDD-cost:  125
c ---[ 689]---> BDD-cost:  125
c ---[ 687]---> BDD-cost:  125
c ---[ 684]---> BDD-cost:  125
c ---[ 682]---> BDD-cost:  125
c ---[ 680]---> BDD-cost:  121
c ---[ 678]---> BDD-cost:  125
c ---[ 676]---> BDD-cost:  123
c ---[ 673]---> BDD-cost:  125
c ---[ 671]---> BDD-cost:  123
c ---[ 669]---> BDD-cost:  125
c ---[ 667]---> BDD-cost:  123
c ---[ 665]---> BDD-cost:   88
c ---[ 662]---> BDD-cost:  117
c ---[ 660]---> BDD-cost:  121
c ---[ 658]---> BDD-cost:  125
c ---[ 656]---> BDD-cost:  125
c ---[ 654]---> BDD-cost:  123
c ---[ 651]---> BDD-cost:  125
c ---[ 649]---> BDD-cost:  121
c ---[ 647]---> BDD-cost:  117
c ---[ 645]---> BDD-cost:  125
c ---[ 643]---> BDD-cost:  125
c ---[ 640]---> BDD-cost:  123
c ---[ 638]---> BDD-cost:  121
c ---[ 636]---> BDD-cost:  125
c ---[ 634]---> BDD-cost:  125
c ---[ 632]---> BDD-cost:  123
c ---[ 629]---> BDD-cost:  125
c ---[ 627]---> BDD-cost:  125
c ---[ 625]---> BDD-cost:  125
c ---[ 623]---> BDD-cost:  123
c ---[ 621]---> BDD-cost:  121
c ---[ 617]---> BDD-cost:  125
c ---[ 615]---> BDD-cost:   88
c ---[ 613]---> BDD-cost:  125
c ---[ 611]---> BDD-cost:  121
c ---[ 609]---> BDD-cost:  121
c ---[ 606]---> BDD-cost:  125
c ---[ 604]---> BDD-cost:  125
c ---[ 602]---> BDD-cost:  125
c ---[ 600]---> BDD-cost:  123
c ---[ 598]---> BDD-cost:  121
c ---[ 595]---> BDD-cost:  123
c ---[ 593]---> BDD-cost:   88
c ---[ 591]---> BDD-cost:   88
c ---[ 589]---> BDD-cost:  125
c ---[ 587]---> BDD-cost:  123
c ---[ 584]---> BDD-cost:   88
c ---[ 582]---> BDD-cost:   88
c ---[ 580]---> BDD-cost:  123
c ---[ 578]---> BDD-cost:  125
c ---[ 576]---> BDD-cost:   88
c ---[ 573]---> BDD-cost:  123
c ---[ 571]---> BDD-cost:   88
c ---[ 569]---> BDD-cost:   88
c ---[ 567]---> BDD-cost:  125
c ---[ 565]---> BDD-cost:   88
c ---[ 562]---> BDD-cost:  123
c ---[ 560]---> BDD-cost:  125
c ---[ 558]---> BDD-cost:  123
c ---[ 556]---> BDD-cost:   88
c ---[ 554]---> BDD-cost:   88
c ---[ 551]---> BDD-cost:  125
c ---[ 549]---> BDD-cost:  125
c ---[ 547]---> BDD-cost:   88
c ---[ 545]---> BDD-cost:   88
c ---[ 543]---> BDD-cost:  121
c ---[ 540]---> BDD-cost:   88
c ---[ 538]---> BDD-cost:  123
c ---[ 536]---> BDD-cost:   88
c ---[ 534]---> BDD-cost:   88
c ---[ 532]---> BDD-cost:  125
c ---[ 529]---> BDD-cost:  125
c ---[ 527]---> BDD-cost:  125
c ---[ 525]---> BDD-cost:  125
c ---[ 524]---> BDD-cost:  146
c ---[ 523]---> BDD-cost:  146
c ---[ 522]---> BDD-cost:  137
c ---[ 521]---> BDD-cost:  137
c ---[ 519]---> BDD-cost:  146
c ---[ 518]---> BDD-cost:  146
c ---[ 517]---> BDD-cost:  137
c ---[ 516]---> BDD-cost:  137
c ---[ 515]---> BDD-cost:  116
c ---[ 514]---> BDD-cost:  116
c ---[ 513]---> BDD-cost:  137
c ---[ 512]---> BDD-cost:  137
c ---[ 511]---> BDD-cost:  146
c ---[ 510]---> BDD-cost:  146
c ---[ 507]---> BDD-cost:  137
c ---[ 506]---> BDD-cost:  137
c ---[ 505]---> BDD-cost:  146
c ---[ 504]---> BDD-cost:  146
c ---[ 503]---> BDD-cost:  137
c ---[ 502]---> BDD-cost:  137
c ---[ 501]---> BDD-cost:  143
c ---[ 500]---> BDD-cost:  143
c ---[ 499]---> BDD-cost:  137
c ---[ 498]---> BDD-cost:  137
c ---[ 496]---> BDD-cost:  141
c ---[ 495]---> BDD-cost:  141
c ---[ 494]---> BDD-cost:  137
c ---[ 493]---> BDD-cost:  137
c ---[ 492]---> BDD-cost:  144
c ---[ 491]---> BDD-cost:  144
c ---[ 490]---> BDD-cost:  137
c ---[ 489]---> BDD-cost:  137
c ---[ 488]---> BDD-cost:  143
c ---[ 487]---> BDD-cost:  143
c ---[ 485]---> BDD-cost:  137
c ---[ 484]---> BDD-cost:  137
c ---[ 483]---> BDD-cost:  143
c ---[ 482]---> BDD-cost:  143
c ---[ 481]---> BDD-cost:  137
c ---[ 480]---> BDD-cost:  137
c ---[ 479]---> BDD-cost:  141
c ---[ 478]---> BDD-cost:  141
c ---[ 477]---> BDD-cost:  137
c ---[ 476]---> BDD-cost:  137
c ---[ 474]---> BDD-cost:  146
c ---[ 473]---> BDD-cost:  146
c ---[ 472]---> BDD-cost:  137
c ---[ 471]---> BDD-cost:  137
c ---[ 470]---> BDD-cost:  143
c ---[ 469]---> BDD-cost:  143
c ---[ 468]---> BDD-cost:  137
c ---[ 467]---> BDD-cost:  137
c ---[ 466]---> BDD-cost:  143
c ---[ 465]---> BDD-cost:  143
c ---[ 463]---> BDD-cost:  137
c ---[ 462]---> BDD-cost:  137
c ---[ 461]---> BDD-cost:  121
c ---[ 460]---> BDD-cost:  121
c ---[ 459]---> BDD-cost:  137
c ---[ 458]---> BDD-cost:  137
c ---[ 457]---> BDD-cost:  136
c ---[ 456]---> BDD-cost:  136
c ---[ 455]---> BDD-cost:  137
c ---[ 454]---> BDD-cost:  137
c ---[ 452]---> BDD-cost:  146
c ---[ 451]---> BDD-cost:  146
c ---[ 450]---> BDD-cost:  137
c ---[ 449]---> BDD-cost:  137
c ---[ 448]---> BDD-cost:  136
c ---[ 447]---> BDD-cost:  136
c ---[ 446]---> BDD-cost:  137
c ---[ 445]---> BDD-cost:  137
c ---[ 444]---> BDD-cost:  141
c ---[ 443]---> BDD-cost:  141
c ---[ 441]---> BDD-cost:  137
c ---[ 440]---> BDD-cost:  137
c ---[ 439]---> BDD-cost:  146
c ---[ 438]---> BDD-cost:  146
c ---[ 437]---> BDD-cost:  137
c ---[ 436]---> BDD-cost:  137
c ---[ 435]---> BDD-cost:  133
c ---[ 434]---> BDD-cost:  133
c ---[ 433]---> BDD-cost:  137
c ---[ 432]---> BDD-cost:  137
c ---[ 430]---> BDD-cost:  146
c ---[ 429]---> BDD-cost:  146
c ---[ 428]---> BDD-cost:  137
c ---[ 427]---> BDD-cost:  137
c ---[ 426]---> BDD-cost:  138
c ---[ 425]---> BDD-cost:  138
c ---[ 424]---> BDD-cost:  137
c ---[ 423]---> BDD-cost:  137
c ---[ 422]---> BDD-cost:  131
c ---[ 421]---> BDD-cost:  131
c ---[ 419]---> BDD-cost:  137
c ---[ 418]---> BDD-cost:  137
c ---[ 417]---> BDD-cost:  146
c ---[ 416]---> BDD-cost:  146
c ---[ 415]---> BDD-cost:  137
c ---[ 414]---> BDD-cost:  137
c ---[ 413]---> BDD-cost:  136
c ---[ 412]---> BDD-cost:  136
c ---[ 411]---> BDD-cost:  137
c ---[ 410]---> BDD-cost:  137
c ---[ 408]---> BDD-cost:  121
c ---[ 407]---> BDD-cost:  121
c ---[ 406]---> BDD-cost:  137
c ---[ 405]---> BDD-cost:  137
c ---[ 404]---> BDD-cost:  141
c ---[ 403]---> BDD-cost:  141
c ---[ 402]---> BDD-cost:  137
c ---[ 401]---> BDD-cost:  137
c ---[ 400]---> BDD-cost:  131
c ---[ 399]---> BDD-cost:  131
c ---[ 396]---> BDD-cost:  137
c ---[ 395]---> BDD-cost:  137
c ---[ 394]---> BDD-cost:  136
c ---[ 393]---> BDD-cost:  136
c ---[ 392]---> BDD-cost:  137
c ---[ 391]---> BDD-cost:  137
c ---[ 390]---> BDD-cost:  116
c ---[ 389]---> BDD-cost:  116
c ---[ 388]---> BDD-cost:  137
c ---[ 387]---> BDD-cost:  137
c ---[ 385]---> BDD-cost:  146
c ---[ 384]---> BDD-cost:  146
c ---[ 383]---> BDD-cost:  137
c ---[ 382]---> BDD-cost:  137
c ---[ 381]---> BDD-cost:  136
c ---[ 380]---> BDD-cost:  136
c ---[ 379]---> BDD-cost:  137
c ---[ 378]---> BDD-cost:  137
c ---[ 377]---> BDD-cost:  116
c ---[ 376]---> BDD-cost:  116
c ---[ 374]---> BDD-cost:  137
c ---[ 373]---> BDD-cost:  137
c ---[ 372]---> BDD-cost:  146
c ---[ 371]---> BDD-cost:  146
c ---[ 370]---> BDD-cost:  137
c ---[ 369]---> BDD-cost:  137
c ---[ 368]---> BDD-cost:  138
c ---[ 367]---> BDD-cost:  138
c ---[ 366]---> BDD-cost:  137
c ---[ 365]---> BDD-cost:  137
c ---[ 363]---> BDD-cost:  141
c ---[ 362]---> BDD-cost:  141
c ---[ 361]---> BDD-cost:  137
c ---[ 360]---> BDD-cost:  137
c ---[ 359]---> BDD-cost:  143
c ---[ 358]---> BDD-cost:  143
c ---[ 357]---> BDD-cost:  137
c ---[ 356]---> BDD-cost:  137
c ---[ 355]---> BDD-cost:  141
c ---[ 354]---> BDD-cost:  141
c ---[ 352]---> BDD-cost:  137
c ---[ 351]---> BDD-cost:  137
c ---[ 350]---> BDD-cost:  131
c ---[ 349]---> BDD-cost:  131
c ---[ 348]---> BDD-cost:  137
c ---[ 347]---> BDD-cost:  137
c ---[ 346]---> BDD-cost:  136
c ---[ 345]---> BDD-cost:  136
c ---[ 344]---> BDD-cost:  137
c ---[ 343]---> BDD-cost:  137
c ---[ 341]---> BDD-cost:  128
c ---[ 340]---> BDD-cost:  128
c ---[ 339]---> BDD-cost:  137
c ---[ 338]---> BDD-cost:  137
c ---[ 337]---> BDD-cost:  146
c ---[ 336]---> BDD-cost:  146
c ---[ 335]---> BDD-cost:  137
c ---[ 334]---> BDD-cost:  137
c ---[ 333]---> BDD-cost:  136
c ---[ 332]---> BDD-cost:  136
c ---[ 330]---> BDD-cost:  137
c ---[ 329]---> BDD-cost:  137
c ---[ 328]---> BDD-cost:  146
c ---[ 327]---> BDD-cost:  146
c ---[ 326]---> BDD-cost:  137
c ---[ 325]---> BDD-cost:  137
c ---[ 324]---> BDD-cost:  141
c ---[ 323]---> BDD-cost:  141
c ---[ 322]---> BDD-cost:  137
c ---[ 321]---> BDD-cost:  137
c ---[ 319]---> BDD-cost:  143
c ---[ 318]---> BDD-cost:  143
c ---[ 317]---> BDD-cost:  137
c ---[ 316]---> BDD-cost:  137
c ---[ 315]---> BDD-cost:  126
c ---[ 314]---> BDD-cost:  126
c ---[ 313]---> BDD-cost:  137
c ---[ 312]---> BDD-cost:  137
c ---[ 311]---> BDD-cost:  122
c ---[ 310]---> BDD-cost:  149
c ---[ 308]---> BDD-cost:  120
c ---[ 307]---> BDD-cost:  141
c ---[ 306]---> BDD-cost:  132
c ---[ 305]---> BDD-cost:  149
c ---[ 304]---> BDD-cost:  124
c ---[ 303]---> BDD-cost:  143
c ---[ 302]---> BDD-cost:  124
c ---[ 301]---> BDD-cost:  139
c ---[ 300]---> BDD-cost:  127
c ---[ 299]---> BDD-cost:  149
c ---[ 297]---> BDD-cost:  124
c ---[ 296]---> BDD-cost:  149
c ---[ 295]---> BDD-cost:  132
c ---[ 294]---> BDD-cost:  139
c ---[ 293]---> BDD-cost:  126
c ---[ 292]---> BDD-cost:  139
c ---[ 291]---> BDD-cost:  132
c ---[ 290]---> BDD-cost:  140
c ---[ 289]---> BDD-cost:  122
c ---[ 288]---> BDD-cost:  144
c ---[ 287]---> BDD-cost:   26
c ---[ 286]---> BDD-cost:   26
c ---[ 285]---> BDD-cost:   26
c ---[ 284]---> BDD-cost:   26
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   26
c ---[ 281]---> BDD-cost:   26
c ---[ 280]---> BDD-cost:   26
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   26
c ---[ 276]---> BDD-cost:   26
c ---[ 275]---> BDD-cost:   26
c ---[ 274]---> BDD-cost:   26
c ---[ 273]---> BDD-cost:   26
c ---[ 272]---> BDD-cost:   26
c ---[ 271]---> BDD-cost:   26
c ---[ 270]---> BDD-cost:   26
c ---[ 269]---> BDD-cost:   26
c ---[ 268]---> BDD-cost:   26
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:   26
c ---[ 265]---> BDD-cost:   26
c ---[ 264]---> BDD-cost:   26
c ---[ 263]---> BDD-cost:   26
c ---[ 262]---> BDD-cost:   26
c ---[ 261]---> BDD-cost:   26
c ---[ 260]---> BDD-cost:   26
c ---[ 259]---> BDD-cost:   26
c ---[ 258]---> BDD-cost:   26
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   26
c ---[ 254]---> BDD-cost:   26
c ---[ 253]---> BDD-cost:   26
c ---[ 252]---> BDD-cost:   26
c ---[ 251]---> BDD-cost:   26
c ---[ 250]---> BDD-cost:   26
c ---[ 249]---> BDD-cost:   26
c ---[ 248]---> BDD-cost:   26
c ---[ 247]---> BDD-cost:   26
c ---[ 246]---> BDD-cost:   26
c ---[ 245]---> BDD-cost:   26
c ---[ 244]---> BDD-cost:   26
c ---[ 243]---> BDD-cost:   26
c ---[ 242]---> BDD-cost:   26
c ---[ 241]---> BDD-cost:   26
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   26
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   26
c ---[ 236]---> BDD-cost:   26
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   26
c ---[ 233]---> BDD-cost:   26
c ---[ 232]---> BDD-cost:   26
c ---[ 231]---> BDD-cost:   26
c ---[ 230]---> BDD-cost:   26
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   26
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   26
c ---[ 225]---> BDD-cost:   26
c ---[ 224]---> BDD-cost:   26
c ---[ 223]---> BDD-cost:   26
c ---[ 222]---> BDD-cost:   26
c ---[ 221]---> BDD-cost:   26
c ---[ 220]---> BDD-cost:   26
c ---[ 219]---> BDD-cost:   26
c ---[ 218]---> BDD-cost:   26
c ---[ 217]---> BDD-cost:   26
c ---[ 216]---> BDD-cost:   26
c ---[ 215]---> BDD-cost:   26
c ---[ 214]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   26
c ---[ 210]---> BDD-cost:   26
c ---[ 209]---> BDD-cost:   26
c ---[ 208]---> BDD-cost:   26
c ---[ 207]---> BDD-cost:   26
c ---[ 206]---> BDD-cost:   26
c ---[ 205]---> BDD-cost:   26
c ---[ 204]---> BDD-cost:   26
c ---[ 203]---> BDD-cost:   26
c ---[ 202]---> BDD-cost:   26
c ---[ 201]---> BDD-cost:   26
c ---[ 200]---> BDD-cost:   26
c ---[ 199]---> BDD-cost:   26
c ---[ 198]---> BDD-cost:   26
c ---[ 197]---> BDD-cost:   26
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   26
c ---[ 194]---> BDD-cost:   26
c ---[ 193]---> BDD-cost:   26
c ---[ 192]---> BDD-cost:   26
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:   26
c ---[ 189]---> BDD-cost:   26
c ---[ 188]---> BDD-cost:   26
c ---[ 187]---> BDD-cost:   26
c ---[ 186]---> BDD-cost:   26
c ---[ 185]---> BDD-cost:   26
c ---[ 184]---> BDD-cost:   26
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   26
c ---[ 181]---> BDD-cost:   26
c ---[ 180]---> BDD-cost:   26
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   26
c ---[ 177]---> BDD-cost:   26
c ---[ 176]---> BDD-cost:   26
c ---[ 175]---> BDD-cost:   26
c ---[ 174]---> BDD-cost:   26
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   26
c ---[ 171]---> BDD-cost:   26
c ---[ 170]---> BDD-cost:   26
c ---[ 169]---> BDD-cost:   26
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   26
c ---[ 165]---> BDD-cost:   26
c ---[ 164]---> BDD-cost:   26
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   26
c ---[ 160]---> BDD-cost:   26
c ---[ 159]---> BDD-cost:   26
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   26
c ---[ 156]---> BDD-cost:   26
c ---[ 155]---> BDD-cost:   26
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   26
c ---[ 152]---> BDD-cost:   26
c ---[ 151]---> BDD-cost:   26
c ---[ 150]---> BDD-cost:   26
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   26
c ---[ 146]---> BDD-cost:   26
c ---[ 145]---> BDD-cost:   26
c ---[ 144]---> BDD-cost:   26
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   26
c ---[ 140]---> BDD-cost:   26
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:   26
c ---[ 137]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   26
c ---[ 135]---> BDD-cost:   26
c ---[ 134]---> BDD-cost:   26
c ---[ 133]---> BDD-cost:   26
c ---[ 132]---> BDD-cost:   26
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:   26
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   26
c ---[ 126]---> BDD-cost:   26
c ---[ 125]---> BDD-cost:   26
c ---[ 124]---> BDD-cost:   26
c ---[ 123]---> BDD-cost:   26
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   26
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   26
c ---[ 117]---> BDD-cost:   26
c ---[ 116]---> BDD-cost:   26
c ---[ 115]---> BDD-cost:   26
c ---[ 114]---> BDD-cost:   26
c ---[ 113]---> BDD-cost:   26
c ---[ 112]---> BDD-cost:   26
c ---[ 111]---> BDD-cost:   26
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   26
c ---[ 108]---> BDD-cost:   26
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   26
c ---[ 105]---> BDD-cost:   26
c ---[ 104]---> BDD-cost:   26
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   26
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   26
c ---[  98]---> BDD-cost:   26
c ---[  97]---> BDD-cost:   26
c ---[  96]---> BDD-cost:   26
c ---[  95]---> BDD-cost:   26
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   26
c ---[  92]---> BDD-cost:   26
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   26
c ---[  88]---> BDD-cost:   26
c ---[  87]---> BDD-cost:   26
c ---[  86]---> BDD-cost:   26
c ---[  85]---> BDD-cost:   26
c ---[  84]---> BDD-cost:   26
c ---[  83]---> BDD-cost:   26
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   26
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   26
c ---[  76]---> BDD-cost:   26
c ---[  75]---> BDD-cost:   26
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   26
c ---[  70]---> BDD-cost:   26
c ---[  69]---> BDD-cost:   26
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   26
c ---[  65]---> BDD-cost:   26
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   26
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   26
c ---[  60]---> BDD-cost:   26
c ---[  59]---> BDD-cost:   26
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   26
c ---[  52]---> BDD-cost:   26
c ---[  51]---> BDD-cost:   26
c ---[  50]---> BDD-cost:   26
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   26
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:   26
c ---[  41]---> BDD-cost:   26
c ---[  40]---> BDD-cost:   26
c ---[  39]---> BDD-cost:   26
c ---[  38]---> BDD-cost:   26
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   26
c ---[  35]---> BDD-cost:   26
c ---[  34]---> BDD-cost:   26
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   26
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   26
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   26
c ---[  22]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   26
c ---[  20]---> BDD-cost:   26
c ---[  19]---> BDD-cost:   26
c ---[  18]---> BDD-cost:   26
c ---[  17]---> BDD-cost:   26
c ---[  16]---> BDD-cost:   26
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:   26
c ---[  12]---> BDD-cost:   26
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   26
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:   26
c ---[   5]---> BDD-cost:   26
c ---[   4]---> BDD-cost:   26
c ---[   3]---> BDD-cost:   26
c ---[   2]---> BDD-cost:   26
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  291264   779807 |   97088       0        0     nan |  0.000 % |
c |       100 |  291264   779807 |  106796     100     6975    69.8 |  1.052 % |
c |       250 |  291220   779719 |  117476     228     7390    32.4 |  1.068 % |
c |       475 |  291212   779703 |  129224     449     8405    18.7 |  1.070 % |
c |       812 |  291038   779355 |  142146     698    10215    14.6 |  1.134 % |
c ==============================================================================
c [1mFound solution: 100352[0m
c ---[   0]---> BDD-cost:  137
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1066 |  291339   780272 |   97113     944    12228    13.0 |  1.134 % |
c |      1166 |  291247   780088 |  106824     998    12683    12.7 |  1.173 % |
c |      1316 |  291185   779964 |  117506    1117    13860    12.4 |  1.196 % |
c |      1541 |  291117   779828 |  129257    1308    15160    11.6 |  1.221 % |
c |      1878 |  291063   779720 |  142183    1618    18135    11.2 |  1.240 % |
c ==============================================================================
c [1mFound solution: 98304[0m
c ---[   0]---> BDD-cost:   88
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2181 |  291285   780422 |   97095    1900    20111    10.6 |  1.240 % |
c |      2281 |  291251   780354 |  106804    1983    20451    10.3 |  1.267 % |
c |      2432 |  291247   780346 |  117484    2132    21872    10.3 |  1.268 % |
c |      2657 |  291235   780322 |  129233    2351    23709    10.1 |  1.273 % |
c ==============================================================================
c [1mFound solution: 97280[0m
c ---[   0]---> BDD-cost:   43
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2911 |  291333   780644 |   97111    2590    25555     9.9 |  1.273 % |
c |      3011 |  291331   780640 |  106822    2688    26760    10.0 |  1.285 % |
c |      3161 |  291331   780640 |  117504    2838    28259    10.0 |  1.285 % |
c |      3387 |  291331   780640 |  129254    3064    31289    10.2 |  1.285 % |
c |      3724 |  291169   780316 |  142180    3320    32992     9.9 |  1.343 % |
c ==============================================================================
c [1mFound solution: 86016[0m
c ---[   0]---> Sorter-cost:  766     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4165 |  291950   782166 |   97316    3755    38018    10.1 |  1.343 % |
c |      4265 |  291950   782166 |  107047    3855    39059    10.1 |  1.347 % |
c |      4416 |  291944   782154 |  117752    4003    40463    10.1 |  1.349 % |
c |      4643 |  291860   781986 |  129527    4188    42102    10.1 |  1.380 % |
c |      4981 |  291848   781962 |  142480    4520    45723    10.1 |  1.384 % |
c |      5488 |  291706   781678 |  156728    4956    50425    10.2 |  1.435 % |
c ==============================================================================
c [1mFound solution: 81920[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6059 |  291662   781615 |   97220    5488    54958    10.0 |  1.435 % |
c |      6159 |  291660   781611 |  106942    5587    56279    10.1 |  1.468 % |
c |      6310 |  291660   781611 |  117636    5738    57762    10.1 |  1.468 % |
c |      6536 |  291656   781603 |  129399    5962    60467    10.1 |  1.470 % |
c |      6874 |  291656   781603 |  142339    6300    65071    10.3 |  1.470 % |
c |      7380 |  291652   781595 |  156573    6804    71420    10.5 |  1.471 % |
c |      8140 |  291586   781463 |  172231    7530    78202    10.4 |  1.495 % |
c ==============================================================================
c [1mFound solution: 79872[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8828 |  291588   781465 |   97196    8213    85015    10.4 |  1.495 % |
c |      8928 |  291586   781461 |  106915    8312    85529    10.3 |  1.504 % |
c |      9078 |  291586   781461 |  117607    8462    86914    10.3 |  1.504 % |
c |      9303 |  291520   781329 |  129367    8652    88514    10.2 |  1.528 % |
c |      9641 |  291520   781329 |  142304    8990    91577    10.2 |  1.528 % |
c ==============================================================================
c [1mFound solution: 77824[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9940 |  291538   781379 |   97179    9289    95886    10.3 |  1.528 % |
c |     10042 |  291530   781363 |  106896    9387    96660    10.3 |  1.537 % |
c |     10192 |  291530   781363 |  117586    9537    98371    10.3 |  1.537 % |
c |     10417 |  291524   781351 |  129345    9759   100586    10.3 |  1.539 % |
c |     10754 |  291524   781351 |  142279   10096   108027    10.7 |  1.539 % |
c |     11260 |  291524   781351 |  156507   10602   114844    10.8 |  1.539 % |
c ==============================================================================
c [1mFound solution: 75776[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11404 |  291533   781371 |   97177   10745   116367    10.8 |  1.539 % |
c |     11504 |  291509   781323 |  106894   10833   117423    10.8 |  1.553 % |
c |     11654 |  291509   781323 |  117584   10983   118782    10.8 |  1.553 % |
c |     11879 |  291459   781223 |  129342   11181   121504    10.9 |  1.571 % |
c |     12216 |  291459   781223 |  142276   11518   124451    10.8 |  1.571 % |
c |     12722 |  291439   781183 |  156504   12014   130322    10.8 |  1.578 % |
c |     13481 |  291431   781167 |  172154   12769   141015    11.0 |  1.581 % |
c |     14620 |  291303   780911 |  189370   13844   155630    11.2 |  1.628 % |
c |     16329 |  291291   780887 |  208307   15547   191071    12.3 |  1.632 % |
c ==============================================================================
c [1mFound solution: 72704[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17677 |  291191   780707 |   97063   16829   206982    12.3 |  1.632 % |
c |     17777 |  291183   780691 |  106769   16925   207744    12.3 |  1.683 % |
c |     17927 |  291183   780691 |  117446   17075   209619    12.3 |  1.683 % |
c |     18152 |  291183   780691 |  129190   17300   212385    12.3 |  1.683 % |
c |     18489 |  291173   780671 |  142109   17632   218834    12.4 |  1.687 % |
c |     18995 |  291159   780643 |  156320   18131   223698    12.3 |  1.692 % |
c |     19754 |  291157   780639 |  171953   18889   237760    12.6 |  1.692 % |
c |     20893 |  291157   780639 |  189148   20028   252079    12.6 |  1.692 % |
c |     22602 |  291135   780595 |  208063   21726   270526    12.5 |  1.700 % |
c |     25164 |  291085   780495 |  228869   24263   343545    14.2 |  1.718 % |
c ==============================================================================
c [1mFound solution: 70656[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26576 |  291067   780474 |   97022   25657   363237    14.2 |  1.718 % |
c |     26676 |  291067   780474 |  106724   25757   364293    14.1 |  1.732 % |
c |     26827 |  291059   780458 |  117396   25904   366735    14.2 |  1.735 % |
c |     27052 |  291059   780458 |  129136   26129   368881    14.1 |  1.735 % |
c |     27389 |  291057   780454 |  142049   26465   380458    14.4 |  1.736 % |
c |     27895 |  291055   780450 |  156254   26970   389722    14.5 |  1.736 % |
c |     28655 |  291051   780442 |  171880   27728   405545    14.6 |  1.738 % |
c |     29794 |  290951   780242 |  189068   28817   430757    14.9 |  1.774 % |
c ==============================================================================
c [1mFound solution: 69632[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29932 |  290920   780155 |   96973   28935   430909    14.9 |  1.774 % |
c |     30033 |  290920   780155 |  106670   29036   432748    14.9 |  1.790 % |
c |     30184 |  290920   780155 |  117337   29187   434203    14.9 |  1.790 % |
c |     30409 |  290918   780151 |  129071   29411   436475    14.8 |  1.791 % |
c |     30746 |  290910   780135 |  141978   29744   440150    14.8 |  1.794 % |
c |     31252 |  290910   780135 |  156175   30250   450632    14.9 |  1.794 % |
c |     32011 |  290892   780099 |  171793   31000   468665    15.1 |  1.801 % |
c |     33150 |  290890   780095 |  188972   32138   486434    15.1 |  1.801 % |
c |     34859 |  290886   780087 |  207870   33845   518802    15.3 |  1.803 % |
c |     37421 |  290874   780063 |  228657   36401   590434    16.2 |  1.807 % |
c |     41265 |  290874   780063 |  251522   40245   722186    17.9 |  1.807 % |
c |     47031 |  290840   779995 |  276675   45994   841275    18.3 |  1.819 % |
c |     55680 |  290768   779851 |  304342   54607  1055832    19.3 |  1.845 % |
c ==============================================================================
c [1mFound solution: 68608[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67604 |  290684   779692 |   96894   66483  1344532    20.2 |  1.845 % |
c |     67706 |  290684   779692 |  106583   66585  1345536    20.2 |  1.881 % |
c |     67859 |  290684   779692 |  117241   66738  1348465    20.2 |  1.881 % |
c |     68084 |  290680   779684 |  128965   66961  1351270    20.2 |  1.882 % |
c |     68421 |  290680   779684 |  141862   67298  1357183    20.2 |  1.882 % |
c |     68927 |  290678   779680 |  156048   67803  1371923    20.2 |  1.883 % |
c ==============================================================================
c [1mFound solution: 67584[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69054 |  290664   779638 |   96888   67922  1373768    20.2 |  1.883 % |
c |     69154 |  290664   779638 |  106576   68022  1374812    20.2 |  1.892 % |
c |     69304 |  290664   779638 |  117234   68172  1380509    20.3 |  1.892 % |
c |     69529 |  290664   779638 |  128957   68397  1382796    20.2 |  1.892 % |
c |     69866 |  290664   779638 |  141853   68734  1388950    20.2 |  1.892 % |
c |     70373 |  290664   779638 |  156039   69241  1409047    20.3 |  1.892 % |
c |     71133 |  290660   779630 |  171643   69999  1434788    20.5 |  1.894 % |
c |     72272 |  290660   779630 |  188807   71138  1499513    21.1 |  1.894 % |
c |     73981 |  290658   779626 |  207688   72846  1573710    21.6 |  1.894 % |
c ==============================================================================
c [1mFound solution: 66560[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76094 |  290669   779657 |   96889   74958  1631886    21.8 |  1.894 % |
c |     76194 |  290669   779657 |  106577   75058  1633276    21.8 |  1.896 % |
c |     76345 |  290669   779657 |  117235   75209  1636013    21.8 |  1.896 % |
c |     76570 |  290669   779657 |  128959   75434  1640062    21.7 |  1.896 % |
c |     76907 |  290669   779657 |  141855   75771  1647899    21.7 |  1.896 % |
c |     77413 |  290669   779657 |  156040   76277  1700953    22.3 |  1.896 % |
c |     78173 |  290669   779657 |  171644   77037  1813865    23.5 |  1.896 % |
c |     79312 |  290669   779657 |  188809   78176  1929898    24.7 |  1.896 % |
c |     81022 |  290655   779629 |  207690   79879  2010094    25.2 |  1.901 % |
c |     83585 |  290597   779513 |  228459   82413  2130450    25.9 |  1.922 % |
c |     87429 |  290591   779501 |  251305   86254  2576979    29.9 |  1.924 % |
c |     93196 |  290569   779457 |  276435   92010  3041934    33.1 |  1.932 % |
c ==============================================================================
c [1mFound solution: 65536[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93466 |  290535   779370 |   96845   92249  3045569    33.0 |  1.932 % |
c |     93568 |  290535   779370 |  106529   92351  3047043    33.0 |  1.950 % |
c |     93719 |  290535   779370 |  117182   92502  3052379    33.0 |  1.950 % |
c |     93944 |  290535   779370 |  128900   92727  3055608    33.0 |  1.950 % |
c |     94281 |  290535   779370 |  141790   93064  3064272    32.9 |  1.950 % |
c |     94787 |  290533   779366 |  155969   93569  3078272    32.9 |  1.951 % |
c ==============================================================================
c [1mFound solution: 64512[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95210 |  290544   779393 |   96848   93992  3102556    33.0 |  1.951 % |
c |     95311 |  290544   779393 |  106532   94093  3104093    33.0 |  1.951 % |
c |     95461 |  290544   779393 |  117186   94243  3105912    33.0 |  1.951 % |
c |     95686 |  290544   779393 |  128904   94468  3110222    32.9 |  1.951 % |
c |     96023 |  290544   779393 |  141795   94805  3138709    33.1 |  1.951 % |
c |     96529 |  290544   779393 |  155974   95311  3148811    33.0 |  1.951 % |
c |     97288 |  290544   779393 |  171572   96070  3250713    33.8 |  1.951 % |
c |     98427 |  290544   779393 |  188729   97209  3286637    33.8 |  1.951 % |
c |    100136 |  290544   779393 |  207602   98918  3363663    34.0 |  1.951 % |
c |    102698 |  290544   779393 |  228362  101480  3618611    35.7 |  1.951 % |
c |    106542 |  290542   779389 |  251198  105323  3845264    36.5 |  1.952 % |
c |    112309 |  290536   779377 |  276318  111087  4007898    36.1 |  1.954 % |
c |    120959 |  290536   779377 |  303950  119737  5019663    41.9 |  1.954 % |
c |    133934 |  290534   779373 |  334345  132711  6674430    50.3 |  1.955 % |
c |    153395 |  290516   779337 |  367780  152163  8492890    55.8 |  1.961 % |
c |    182587 |  290506   779317 |  404558  181350 11734717    64.7 |  1.965 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 26884 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.95 0.90 2/54 26880
Raw data (stat): 26880 (runsolver) R 26879 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841948102 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+9.99952 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.0023 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26884
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.07 0.99 0.91 3/58 26921
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 26937
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 26937
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 26937
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 26937
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 26937
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26937
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26939
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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 0.99 0.91 1/53 26941
Raw data (stat): 26880 (minisat+_script) S 26879 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841948102 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.88
CPU user time (s): 1228.88
CPU system time (s): 0.998848
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####