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 32144

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        897216 kB
Buffers:         22988 kB
Cached:          94064 kB
SwapCached:        656 kB
Active:          22076 kB
Inactive:        97144 kB
HighTotal:      131008 kB
HighFree:        34020 kB
LowTotal:       903652 kB
LowFree:        863196 kB
SwapTotal:     2097136 kB
SwapFree:      2095672 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5584 kB
Slab:            12588 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 08:35:59 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23504 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]---> Sorter-cost:  768     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1066 |  291645   780808 |   97215     944    12228    13.0 |  1.134 % |
c |      1166 |  291553   780624 |  106936     997    12645    12.7 |  1.173 % |
c |      1316 |  291491   780500 |  117630    1117    13755    12.3 |  1.195 % |
c |      1541 |  291491   780500 |  129393    1342    15374    11.5 |  1.195 % |
c |      1879 |  291479   780476 |  142332    1674    19184    11.5 |  1.199 % |
c ==============================================================================
c [1mFound solution: 86016[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2381 |  291666   780936 |   97222    2176    24803    11.4 |  1.199 % |
c |      2481 |  291664   780932 |  106944    2275    26008    11.4 |  1.203 % |
c |      2631 |  291650   780904 |  117638    2417    26932    11.1 |  1.208 % |
c |      2857 |  291634   780872 |  129402    2635    29054    11.0 |  1.214 % |
c |      3194 |  291580   780764 |  142342    2944    31690    10.8 |  1.234 % |
c ==============================================================================
c [1mFound solution: 80896[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3555 |  291622   780879 |   97207    3300    35632    10.8 |  1.234 % |
c |      3655 |  291622   780879 |  106927    3400    36637    10.8 |  1.236 % |
c |      3807 |  291560   780755 |  117620    3521    37409    10.6 |  1.259 % |
c |      4032 |  291556   780747 |  129382    3744    41109    11.0 |  1.260 % |
c |      4369 |  291496   780627 |  142320    4051    45585    11.3 |  1.282 % |
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 |      4700 |  291472   780569 |   97157    4373    48743    11.1 |  1.282 % |
c |      4800 |  291468   780561 |  106872    4471    49513    11.1 |  1.296 % |
c |      4951 |  291468   780561 |  117559    4622    51395    11.1 |  1.296 % |
c |      5177 |  291468   780561 |  129315    4848    55343    11.4 |  1.296 % |
c ==============================================================================
c [1mFound solution: 78848[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5468 |  291478   780603 |   97159    5131    57356    11.2 |  1.296 % |
c |      5569 |  291468   780583 |  106874    5227    58708    11.2 |  1.306 % |
c |      5720 |  291464   780575 |  117562    5376    59593    11.1 |  1.307 % |
c |      5945 |  291448   780543 |  129318    5593    60911    10.9 |  1.313 % |
c |      6283 |  291390   780427 |  142250    5902    63555    10.8 |  1.334 % |
c ==============================================================================
c [1mFound solution: 74752[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6701 |  291357   780382 |   97119    6287    68083    10.8 |  1.334 % |
c |      6801 |  291357   780382 |  106830    6387    72068    11.3 |  1.358 % |
c |      6951 |  291337   780342 |  117513    6527    73012    11.2 |  1.366 % |
c |      7176 |  291335   780338 |  129265    6751    76731    11.4 |  1.366 % |
c |      7515 |  291327   780322 |  142191    7086    83689    11.8 |  1.369 % |
c |      8021 |  291327   780322 |  156411    7592    93369    12.3 |  1.369 % |
c |      8782 |  291279   780226 |  172052    8329   108477    13.0 |  1.387 % |
c |      9923 |  291239   780146 |  189257    9450   121068    12.8 |  1.401 % |
c |     11633 |  291149   779966 |  208183   11115   140431    12.6 |  1.434 % |
c ==============================================================================
c [1mFound solution: 73728[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12574 |  291078   779816 |   97026   12022   149611    12.4 |  1.434 % |
c |     12675 |  291076   779812 |  106728   12122   150602    12.4 |  1.463 % |
c |     12825 |  291076   779812 |  117401   12272   151840    12.4 |  1.463 % |
c |     13050 |  290936   779532 |  129141   12427   153651    12.4 |  1.514 % |
c |     13390 |  290934   779528 |  142055   12766   156865    12.3 |  1.515 % |
c |     13896 |  290910   779480 |  156261   13259   162467    12.3 |  1.523 % |
c |     14656 |  290896   779452 |  171887   14012   171618    12.2 |  1.528 % |
c |     15796 |  290864   779388 |  189076   15135   210996    13.9 |  1.540 % |
c |     17505 |  290696   779052 |  207983   16758   251409    15.0 |  1.601 % |
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 |     19716 |  290700   779072 |   96900   18962   288246    15.2 |  1.601 % |
c |     19817 |  290654   778980 |  106590   19040   288780    15.2 |  1.622 % |
c |     19967 |  290644   778960 |  117249   19185   290323    15.1 |  1.626 % |
c |     20197 |  290632   778936 |  128973   19409   292297    15.1 |  1.630 % |
c |     20535 |  290630   778932 |  141871   19746   297623    15.1 |  1.631 % |
c |     21041 |  290630   778932 |  156058   20252   303096    15.0 |  1.631 % |
c |     21801 |  290630   778932 |  171664   21012   316038    15.0 |  1.631 % |
c |     22941 |  290606   778884 |  188830   22140   335227    15.1 |  1.640 % |
c ==============================================================================
c [1mFound solution: 71680[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23177 |  290598   778855 |   96866   22374   338422    15.1 |  1.640 % |
c |     23279 |  290598   778855 |  106552   22476   339332    15.1 |  1.646 % |
c |     23429 |  290594   778847 |  117207   22624   340899    15.1 |  1.648 % |
c |     23656 |  290594   778847 |  128928   22851   344205    15.1 |  1.648 % |
c |     23993 |  290592   778843 |  141821   23187   349793    15.1 |  1.648 % |
c |     24500 |  290586   778831 |  156003   23691   357798    15.1 |  1.651 % |
c |     25259 |  290570   778799 |  171604   24442   369227    15.1 |  1.656 % |
c |     26400 |  290562   778783 |  188764   25579   385079    15.1 |  1.659 % |
c |     28108 |  290532   778723 |  207640   27272   407333    14.9 |  1.670 % |
c |     30672 |  290428   778515 |  228404   29784   457928    15.4 |  1.708 % |
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 |     34029 |  290416   778506 |   96805   33126   506822    15.3 |  1.708 % |
c |     34131 |  290416   778506 |  106485   33228   507968    15.3 |  1.719 % |
c |     34283 |  290416   778506 |  117134   33380   509702    15.3 |  1.719 % |
c |     34510 |  290416   778506 |  128847   33607   512892    15.3 |  1.719 % |
c |     34847 |  290412   778498 |  141732   33942   517675    15.3 |  1.721 % |
c |     35353 |  290384   778442 |  155905   34434   525171    15.3 |  1.731 % |
c |     36113 |  290384   778442 |  171495   35194   539205    15.3 |  1.731 % |
c |     37253 |  290382   778438 |  188645   36333   560129    15.4 |  1.732 % |
c |     38961 |  290342   778358 |  207510   38021   586356    15.4 |  1.746 % |
c |     41526 |  290332   778338 |  228261   40581   630215    15.5 |  1.750 % |
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 |     42175 |  290342   778367 |   96780   41229   640212    15.5 |  1.750 % |
c |     42276 |  290336   778355 |  106458   41327   641011    15.5 |  1.753 % |
c |     42426 |  290320   778323 |  117103   41469   642189    15.5 |  1.759 % |
c |     42652 |  290314   778311 |  128814   41692   646447    15.5 |  1.761 % |
c |     42989 |  290312   778307 |  141695   42028   653341    15.5 |  1.762 % |
c |     43496 |  290308   778299 |  155865   42533   719518    16.9 |  1.763 % |
c |     44255 |  290250   778183 |  171451   43263   729651    16.9 |  1.784 % |
c |     45395 |  290250   778183 |  188596   44403   749267    16.9 |  1.784 % |
c |     47103 |  290232   778147 |  207456   46102   781037    16.9 |  1.791 % |
c |     49665 |  290210   778103 |  228202   48653   826022    17.0 |  1.799 % |
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 |     50269 |  290191   778046 |   96730   49221   838785    17.0 |  1.799 % |
c |     50369 |  290191   778046 |  106403   49321   842191    17.1 |  1.810 % |
c |     50520 |  290191   778046 |  117043   49472   846101    17.1 |  1.810 % |
c |     50749 |  290191   778046 |  128747   49701   849199    17.1 |  1.810 % |
c |     51086 |  290183   778030 |  141622   50034   856220    17.1 |  1.812 % |
c |     51593 |  290179   778022 |  155784   50539   863020    17.1 |  1.814 % |
c |     52353 |  290175   778014 |  171363   51297   877572    17.1 |  1.815 % |
c |     53492 |  290173   778010 |  188499   52435   927420    17.7 |  1.816 % |
c |     55202 |  290169   778002 |  207349   54143   990763    18.3 |  1.818 % |
c |     57764 |  290163   777990 |  228084   56702  1069802    18.9 |  1.820 % |
c |     61608 |  290121   777906 |  250892   60525  1168071    19.3 |  1.835 % |
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 |     66765 |  290124   777921 |   96708   65677  1897164    28.9 |  1.835 % |
c |     66865 |  290124   777921 |  106378   65777  1897821    28.9 |  1.839 % |
c |     67015 |  290124   777921 |  117016   65927  1899427    28.8 |  1.839 % |
c |     67240 |  290124   777921 |  128718   66152  1906580    28.8 |  1.839 % |
c |     67580 |  290122   777917 |  141590   66491  1911773    28.8 |  1.840 % |
c |     68086 |  290122   777917 |  155749   66997  1958458    29.2 |  1.840 % |
c |     68846 |  290122   777917 |  171324   67757  1976091    29.2 |  1.840 % |
c |     69985 |  290122   777917 |  188456   68896  2130684    30.9 |  1.840 % |
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 |     71129 |  290081   777802 |   96693   69993  2158343    30.8 |  1.840 % |
c |     71229 |  290081   777802 |  106362   70093  2159802    30.8 |  1.859 % |
c |     71381 |  290081   777802 |  116998   70245  2162178    30.8 |  1.859 % |
c |     71606 |  290081   777802 |  128698   70470  2165762    30.7 |  1.859 % |
c |     71943 |  290079   777798 |  141568   70806  2171705    30.7 |  1.860 % |
c |     72449 |  290079   777798 |  155725   71312  2239602    31.4 |  1.860 % |
c |     73208 |  290079   777798 |  171297   72071  2276484    31.6 |  1.860 % |
c |     74347 |  290079   777798 |  188427   73210  2322780    31.7 |  1.860 % |
c |     76058 |  290075   777790 |  207270   74919  2449335    32.7 |  1.862 % |
c |     78620 |  290069   777778 |  227997   77478  2652813    34.2 |  1.864 % |
c |     82464 |  290065   777770 |  250796   81320  2836721    34.9 |  1.865 % |
c |     88230 |  290065   777770 |  275876   87086  4365016    50.1 |  1.865 % |
c |     96879 |  290047   777734 |  303464   95726  5420429    56.6 |  1.872 % |
c |    109853 |  290033   777706 |  333810  108693  6146174    56.5 |  1.877 % |
c |    129314 |  290003   777646 |  367191  128139  7293758    56.9 |  1.888 % |
c |    158506 |  289935   777510 |  403910  157297  9727153    61.8 |  1.912 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 25350 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.97 0.98 0.94 2/54 25346
Raw data (stat): 25346 (runsolver) R 25345 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796430179 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0012 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0012 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0015 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0111 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0123 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0124 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0161 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0163 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 0.99 0.98 0.94 2/55 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 0.99 0.98 0.94 1/53 25350
Raw data (stat): 25346 (minisat+_script) S 25345 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796430179 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.91
CPU system time (s): 0.970852
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####