| Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-fit1p.opb |
| MD5SUM | 466386fc28c4adb9c70eb7384ea57208 |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | |
| (Un)Satisfiability was proved | |
| Best value of the objective function | |
| Optimality of the best value was proved | |
| Number of terms in the objective function | 20520 |
| Biggest coefficient in the objective function | 1572864 |
| Number of bits for the biggest coefficient in the objective function | 21 |
| Sum of the numbers in the objective function | 1553988150 |
| Number of bits of the sum of numbers in the objective function | 31 |
| Biggest number in a constraint | 58038681600 |
| Number of bits of the biggest number in a constraint | 36 |
| Biggest sum of numbers in a constraint | 204926279575 |
| Number of bits of the biggest sum of numbers | 38 |
| Best result obtained on this benchmark | |
| Best CPU time to get the best result obtained on this benchmark | |
| Number of variables | 31508 |
| Total number of constraints | 1026 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 0 |
| Number of constraints which are nor clauses,nor cardinality constraints | 1026 |
| Minimum length of a constraint | 14 |
| Maximum length of a constraint | 416 |
LAUNCH ON wulflinc24 THE 2005-09-20 02:38:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3157 boxname=wulflinc24 idbench=813 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 466386fc28c4adb9c70eb7384ea57208 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fit1p.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fit1p.opb IDLAUNCH: 3157 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 919572 kB Buffers: 2480 kB Cached: 84688 kB SwapCached: 756 kB Active: 24540 kB Inactive: 65260 kB HighTotal: 131008 kB HighFree: 42112 kB LowTotal: 903652 kB LowFree: 877460 kB SwapTotal: 2097892 kB SwapFree: 2096608 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 19508 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:58:44 (client local time) WITH STATUS 0 IN 1208.31 SECONDS stats: 3157 7 1208.31 0
c Parsing PB file... c Converting 1653 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[1714]---> BDD-cost: 15 c ---[1713]---> BDD-cost: 14 c ---[1712]---> BDD-cost: 14 c ---[1710]---> BDD-cost: 14 c ---[1709]---> BDD-cost: 15 c ---[1708]---> BDD-cost: 13 c ---[1707]---> BDD-cost: 13 c ---[1706]---> BDD-cost: 14 c ---[1705]---> BDD-cost: 14 c ---[1703]---> BDD-cost: 13 c ---[1702]---> BDD-cost: 14 c ---[1701]---> BDD-cost: 14 c ---[1700]---> BDD-cost: 13 c ---[1699]---> BDD-cost: 13 c ---[1698]---> BDD-cost: 14 c ---[1697]---> BDD-cost: 14 c ---[1695]---> BDD-cost: 13 c ---[1694]---> BDD-cost: 13 c ---[1693]---> BDD-cost: 15 c ---[1691]---> BDD-cost: 13 c ---[1690]---> BDD-cost: 15 c ---[1689]---> BDD-cost: 15 c ---[1688]---> BDD-cost: 14 c ---[1687]---> BDD-cost: 14 c ---[1686]---> BDD-cost: 13 c ---[1685]---> BDD-cost: 15 c ---[1683]---> BDD-cost: 14 c ---[1681]---> BDD-cost: 15 c ---[1680]---> BDD-cost: 14 c ---[1679]---> BDD-cost: 14 c ---[1678]---> BDD-cost: 15 c ---[1677]---> BDD-cost: 13 c ---[1676]---> BDD-cost: 13 c ---[1674]---> BDD-cost: 15 c ---[1673]---> BDD-cost: 13 c ---[1672]---> BDD-cost: 14 c ---[1671]---> BDD-cost: 14 c ---[1670]---> BDD-cost: 13 c ---[1669]---> BDD-cost: 15 c ---[1667]---> BDD-cost: 15 c ---[1666]---> BDD-cost: 14 c ---[1665]---> BDD-cost: 13 c ---[1664]---> BDD-cost: 16 c ---[1663]---> BDD-cost: 16 c ---[1662]---> BDD-cost: 13 c ---[1661]---> BDD-cost: 13 c ---[1660]---> BDD-cost: 15 c ---[1659]---> BDD-cost: 14 c ---[1658]---> BDD-cost: 14 c ---[1657]---> BDD-cost: 13 c ---[1656]---> BDD-cost: 14 c ---[1655]---> BDD-cost: 15 c ---[1652]---> BDD-cost: 13 c ---[1651]---> BDD-cost: 13 c ---[1650]---> BDD-cost: 15 c ---[1649]---> BDD-cost: 13 c ---[1648]---> BDD-cost: 13 c ---[1647]---> BDD-cost: 13 c ---[1646]---> BDD-cost: 15 c ---[1645]---> BDD-cost: 15 c ---[1644]---> BDD-cost: 15 c ---[1641]---> BDD-cost: 13 c ---[1639]---> BDD-cost: 13 c ---[1638]---> BDD-cost: 13 c ---[1636]---> BDD-cost: 14 c ---[1633]---> BDD-cost: 15 c ---[1632]---> BDD-cost: 13 c ---[1631]---> BDD-cost: 13 c ---[1630]---> BDD-cost: 14 c ---[1629]---> BDD-cost: 15 c ---[1628]---> BDD-cost: 14 c ---[1627]---> BDD-cost: 13 c ---[1626]---> BDD-cost: 13 c ---[1625]---> BDD-cost: 15 c ---[1624]---> BDD-cost: 14 c ---[1623]---> BDD-cost: 14 c ---[1622]---> BDD-cost: 15 c ---[1621]---> BDD-cost: 15 c ---[1620]---> BDD-cost: 15 c ---[1619]---> BDD-cost: 13 c ---[1617]---> BDD-cost: 13 c ---[1616]---> BDD-cost: 15 c ---[1615]---> BDD-cost: 13 c ---[1614]---> BDD-cost: 13 c ---[1613]---> BDD-cost: 14 c ---[1612]---> BDD-cost: 14 c ---[1611]---> BDD-cost: 15 c ---[1610]---> BDD-cost: 13 c ---[1609]---> BDD-cost: 15 c ---[1608]---> BDD-cost: 15 c ---[1606]---> BDD-cost: 14 c ---[1605]---> BDD-cost: 15 c ---[1604]---> BDD-cost: 13 c ---[1602]---> BDD-cost: 14 c ---[1601]---> BDD-cost: 15 c ---[1600]---> BDD-cost: 15 c ---[1599]---> BDD-cost: 14 c ---[1597]---> BDD-cost: 15 c ---[1596]---> BDD-cost: 14 c ---[1595]---> BDD-cost: 15 c ---[1594]---> BDD-cost: 14 c ---[1593]---> BDD-cost: 14 c ---[1592]---> BDD-cost: 14 c ---[1590]---> BDD-cost: 13 c ---[1589]---> BDD-cost: 13 c ---[1588]---> BDD-cost: 13 c ---[1587]---> BDD-cost: 13 c ---[1586]---> BDD-cost: 13 c ---[1585]---> BDD-cost: 14 c ---[1584]---> BDD-cost: 15 c ---[1583]---> BDD-cost: 13 c ---[1582]---> BDD-cost: 13 c ---[1581]---> BDD-cost: 13 c ---[1580]---> BDD-cost: 13 c ---[1579]---> BDD-cost: 14 c ---[1577]---> BDD-cost: 13 c ---[1575]---> BDD-cost: 15 c ---[1572]---> BDD-cost: 15 c ---[1571]---> BDD-cost: 15 c ---[1570]---> BDD-cost: 13 c ---[1569]---> BDD-cost: 14 c ---[1568]---> BDD-cost: 14 c ---[1567]---> BDD-cost: 15 c ---[1566]---> BDD-cost: 13 c ---[1564]---> BDD-cost: 13 c ---[1563]---> BDD-cost: 13 c ---[1562]---> BDD-cost: 14 c ---[1559]---> BDD-cost: 14 c ---[1558]---> BDD-cost: 14 c ---[1557]---> BDD-cost: 14 c ---[1555]---> BDD-cost: 14 c ---[1554]---> BDD-cost: 13 c ---[1553]---> BDD-cost: 16 c ---[1552]---> BDD-cost: 13 c ---[1551]---> BDD-cost: 13 c ---[1550]---> BDD-cost: 13 c ---[1549]---> BDD-cost: 15 c ---[1548]---> BDD-cost: 14 c ---[1546]---> BDD-cost: 14 c ---[1545]---> BDD-cost: 15 c ---[1544]---> BDD-cost: 13 c ---[1543]---> BDD-cost: 14 c ---[1542]---> BDD-cost: 14 c ---[1541]---> BDD-cost: 14 c ---[1539]---> BDD-cost: 13 c ---[1538]---> BDD-cost: 13 c ---[1537]---> BDD-cost: 13 c ---[1536]---> BDD-cost: 14 c ---[1534]---> BDD-cost: 14 c ---[1533]---> BDD-cost: 13 c ---[1532]---> BDD-cost: 14 c ---[1531]---> BDD-cost: 14 c ---[1530]---> BDD-cost: 13 c ---[1529]---> BDD-cost: 13 c ---[1528]---> BDD-cost: 13 c ---[1527]---> BDD-cost: 15 c ---[1526]---> BDD-cost: 15 c ---[1525]---> BDD-cost: 14 c ---[1524]---> BDD-cost: 14 c ---[1523]---> BDD-cost: 14 c ---[1522]---> BDD-cost: 13 c ---[1521]---> BDD-cost: 13 c ---[1520]---> BDD-cost: 15 c ---[1519]---> BDD-cost: 14 c ---[1518]---> BDD-cost: 13 c ---[1517]---> BDD-cost: 13 c ---[1514]---> BDD-cost: 14 c ---[1513]---> BDD-cost: 15 c ---[1511]---> BDD-cost: 13 c ---[1510]---> BDD-cost: 15 c ---[1509]---> BDD-cost: 13 c ---[1508]---> BDD-cost: 13 c ---[1507]---> BDD-cost: 13 c ---[1506]---> BDD-cost: 13 c ---[1505]---> BDD-cost: 13 c ---[1504]---> BDD-cost: 14 c ---[1503]---> BDD-cost: 14 c ---[1502]---> BDD-cost: 15 c ---[1501]---> BDD-cost: 15 c ---[1500]---> BDD-cost: 14 c ---[1498]---> BDD-cost: 15 c ---[1497]---> BDD-cost: 13 c ---[1493]---> BDD-cost: 14 c ---[1492]---> BDD-cost: 14 c ---[1491]---> BDD-cost: 14 c ---[1490]---> BDD-cost: 15 c ---[1489]---> BDD-cost: 15 c ---[1488]---> BDD-cost: 13 c ---[1487]---> BDD-cost: 13 c ---[1485]---> BDD-cost: 14 c ---[1484]---> BDD-cost: 13 c ---[1483]---> BDD-cost: 14 c ---[1482]---> BDD-cost: 13 c ---[1481]---> BDD-cost: 15 c ---[1480]---> BDD-cost: 14 c ---[1479]---> BDD-cost: 14 c ---[1478]---> BDD-cost: 14 c ---[1476]---> BDD-cost: 13 c ---[1475]---> BDD-cost: 15 c ---[1473]---> BDD-cost: 15 c ---[1472]---> BDD-cost: 15 c ---[1471]---> BDD-cost: 13 c ---[1470]---> BDD-cost: 14 c ---[1469]---> BDD-cost: 14 c ---[1468]---> BDD-cost: 14 c ---[1466]---> BDD-cost: 13 c ---[1465]---> BDD-cost: 14 c ---[1464]---> BDD-cost: 15 c ---[1463]---> BDD-cost: 13 c ---[1462]---> BDD-cost: 14 c ---[1461]---> BDD-cost: 15 c ---[1460]---> BDD-cost: 13 c ---[1459]---> BDD-cost: 14 c ---[1458]---> BDD-cost: 15 c ---[1456]---> BDD-cost: 16 c ---[1455]---> BDD-cost: 14 c ---[1454]---> BDD-cost: 13 c ---[1453]---> BDD-cost: 13 c ---[1451]---> BDD-cost: 15 c ---[1450]---> BDD-cost: 14 c ---[1448]---> BDD-cost: 13 c ---[1446]---> BDD-cost: 14 c ---[1444]---> BDD-cost: 14 c ---[1443]---> BDD-cost: 14 c ---[1442]---> BDD-cost: 15 c ---[1441]---> BDD-cost: 14 c ---[1440]---> BDD-cost: 13 c ---[1439]---> BDD-cost: 13 c ---[1438]---> BDD-cost: 13 c ---[1437]---> BDD-cost: 14 c ---[1436]---> BDD-cost: 13 c ---[1435]---> BDD-cost: 15 c ---[1434]---> BDD-cost: 13 c ---[1433]---> BDD-cost: 13 c ---[1432]---> BDD-cost: 13 c ---[1431]---> BDD-cost: 14 c ---[1429]---> BDD-cost: 15 c ---[1428]---> BDD-cost: 14 c ---[1427]---> BDD-cost: 14 c ---[1426]---> BDD-cost: 14 c ---[1425]---> BDD-cost: 14 c ---[1424]---> BDD-cost: 13 c ---[1423]---> BDD-cost: 14 c ---[1422]---> BDD-cost: 14 c ---[1421]---> BDD-cost: 14 c ---[1420]---> BDD-cost: 14 c ---[1419]---> BDD-cost: 14 c ---[1418]---> BDD-cost: 15 c ---[1417]---> BDD-cost: 13 c ---[1416]---> BDD-cost: 13 c ---[1415]---> BDD-cost: 15 c ---[1414]---> BDD-cost: 13 c ---[1413]---> BDD-cost: 15 c ---[1412]---> BDD-cost: 14 c ---[1411]---> BDD-cost: 13 c ---[1410]---> BDD-cost: 13 c ---[1409]---> BDD-cost: 15 c ---[1408]---> BDD-cost: 15 c ---[1406]---> BDD-cost: 13 c ---[1405]---> BDD-cost: 14 c ---[1404]---> BDD-cost: 14 c ---[1403]---> BDD-cost: 13 c ---[1402]---> BDD-cost: 15 c ---[1400]---> BDD-cost: 14 c ---[1398]---> BDD-cost: 13 c ---[1397]---> BDD-cost: 14 c ---[1396]---> BDD-cost: 15 c ---[1395]---> BDD-cost: 13 c ---[1394]---> BDD-cost: 14 c ---[1392]---> BDD-cost: 13 c ---[1391]---> BDD-cost: 15 c ---[1390]---> BDD-cost: 14 c ---[1389]---> BDD-cost: 15 c ---[1388]---> BDD-cost: 14 c ---[1387]---> BDD-cost: 15 c ---[1385]---> BDD-cost: 13 c ---[1383]---> BDD-cost: 15 c ---[1382]---> BDD-cost: 13 c ---[1381]---> BDD-cost: 13 c ---[1380]---> BDD-cost: 13 c ---[1377]---> BDD-cost: 14 c ---[1376]---> BDD-cost: 13 c ---[1375]---> BDD-cost: 14 c ---[1374]---> BDD-cost: 15 c ---[1373]---> BDD-cost: 13 c ---[1372]---> BDD-cost: 14 c ---[1371]---> BDD-cost: 16 c ---[1370]---> BDD-cost: 13 c ---[1368]---> BDD-cost: 13 c ---[1367]---> BDD-cost: 14 c ---[1366]---> BDD-cost: 13 c ---[1364]---> BDD-cost: 15 c ---[1363]---> BDD-cost: 15 c ---[1362]---> BDD-cost: 13 c ---[1361]---> BDD-cost: 14 c ---[1360]---> BDD-cost: 15 c ---[1359]---> BDD-cost: 15 c ---[1358]---> BDD-cost: 14 c ---[1357]---> BDD-cost: 16 c ---[1356]---> BDD-cost: 14 c ---[1355]---> BDD-cost: 15 c ---[1354]---> BDD-cost: 13 c ---[1353]---> BDD-cost: 14 c ---[1352]---> BDD-cost: 14 c ---[1350]---> BDD-cost: 15 c ---[1349]---> BDD-cost: 14 c ---[1348]---> BDD-cost: 13 c ---[1347]---> BDD-cost: 13 c ---[1346]---> BDD-cost: 14 c ---[1345]---> BDD-cost: 14 c ---[1344]---> BDD-cost: 14 c ---[1343]---> BDD-cost: 15 c ---[1342]---> BDD-cost: 13 c ---[1341]---> BDD-cost: 17 c ---[1340]---> BDD-cost: 14 c ---[1339]---> BDD-cost: 13 c ---[1337]---> BDD-cost: 13 c ---[1336]---> BDD-cost: 14 c ---[1335]---> BDD-cost: 13 c ---[1334]---> BDD-cost: 14 c ---[1333]---> BDD-cost: 13 c ---[1332]---> BDD-cost: 15 c ---[1331]---> BDD-cost: 14 c ---[1330]---> BDD-cost: 13 c ---[1329]---> BDD-cost: 13 c ---[1328]---> BDD-cost: 14 c ---[1327]---> BDD-cost: 13 c ---[1325]---> BDD-cost: 14 c ---[1324]---> BDD-cost: 13 c ---[1323]---> BDD-cost: 13 c ---[1322]---> BDD-cost: 15 c ---[1321]---> BDD-cost: 14 c ---[1320]---> BDD-cost: 14 c ---[1319]---> BDD-cost: 13 c ---[1318]---> BDD-cost: 14 c ---[1317]---> BDD-cost: 14 c ---[1315]---> Sorter-cost:14715 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1313]---> Sorter-cost:18418 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1311]---> Sorter-cost:15328 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1309]---> Adder-cost: 474 maxlim: 5010336 bits: 24/23 c ---[1307]---> Adder-cost: 1418 maxlim: 83939090 bits: 28/27 c ---[1305]---> Adder-cost: 522 maxlim: 5911281 bits: 24/23 c ---[1303]---> Sorter-cost:19611 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1301]---> Adder-cost: 744 maxlim: 9189328 bits: 24/24 c ---[1299]---> Sorter-cost:19206 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1297]---> Sorter-cost:19874 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1295]---> Sorter-cost:19540 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1293]---> Sorter-cost:14751 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1291]---> Sorter-cost:15525 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1289]---> Sorter-cost:20285 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1287]---> Sorter-cost:19975 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1285]---> Adder-cost: 512 maxlim: 7288903 bits: 24/23 c ---[1283]---> Adder-cost: 1367 maxlim: 140370820 bits: 28/28 c ---[1281]---> Adder-cost: 2130 maxlim: 323768400 bits: 30/29 c ---[1279]---> Adder-cost: 1590 maxlim: 47250815 bits: 27/26 c ---[1277]---> Adder-cost: 1448 maxlim: 158305020 bits: 29/28 c ---[1275]---> Sorter-cost:21017 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1273]---> Adder-cost: 510 maxlim: 6912054 bits: 24/23 c ---[1271]---> Adder-cost: 1482 maxlim: 48898480 bits: 27/26 c ---[1269]---> Sorter-cost:19235 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1267]---> Sorter-cost:17969 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1265]---> Adder-cost: 1312 maxlim: 207920160 bits: 29/28 c ---[1263]---> Sorter-cost:14874 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1261]---> Adder-cost: 1656 maxlim: 251559140 bits: 29/28 c ---[1259]---> Adder-cost: 438 maxlim: 8499817 bits: 24/24 c ---[1257]---> Sorter-cost:11919 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1255]---> Sorter-cost:16524 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1253]---> Adder-cost: 1430 maxlim: 131286560 bits: 28/27 c ---[1251]---> Adder-cost: 1274 maxlim: 76966160 bits: 27/27 c ---[1249]---> Adder-cost: 1474 maxlim: 46886720 bits: 27/26 c ---[1247]---> Adder-cost: 864 maxlim: 9168634 bits: 24/24 c ---[1245]---> Sorter-cost:16176 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1243]---> Adder-cost: 708 maxlim: 7205654 bits: 24/23 c ---[1241]---> Sorter-cost:20587 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1239]---> Sorter-cost:14577 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1237]---> Sorter-cost:16245 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1235]---> Sorter-cost:14388 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1233]---> Sorter-cost:20993 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1231]---> Adder-cost: 1362 maxlim: 112367180 bits: 28/27 c ---[1229]---> Sorter-cost:14651 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1227]---> Adder-cost: 1530 maxlim: 38115715 bits: 27/26 c ---[1225]---> Sorter-cost:12584 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1223]---> Adder-cost: 1530 maxlim: 86063400 bits: 28/27 c ---[1221]---> Sorter-cost:15609 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1219]---> Sorter-cost:19598 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1217]---> Sorter-cost:15646 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1215]---> Sorter-cost:15280 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1213]---> Sorter-cost:20566 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1211]---> Sorter-cost:16723 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1209]---> Sorter-cost:15857 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1207]---> Adder-cost: 580 maxlim: 13268802 bits: 24/24 c ---[1205]---> Sorter-cost:13552 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1203]---> Adder-cost: 738 maxlim: 8057506 bits: 24/23 c ---[1201]---> Adder-cost: 1240 maxlim: 78510020 bits: 28/27 c ---[1199]---> Adder-cost: 1974 maxlim: 547025700 bits: 31/30 c ---[1197]---> Adder-cost: 582 maxlim: 4713535 bits: 24/23 c ---[1195]---> Sorter-cost:15706 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1193]---> Adder-cost: 1048 maxlim: 111291980 bits: 28/27 c ---[1191]---> Sorter-cost:15973 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1189]---> Sorter-cost:11624 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1187]---> Adder-cost: 404 maxlim: 6977193 bits: 24/23 c ---[1185]---> Sorter-cost:15109 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1183]---> Adder-cost: 426 maxlim: 7600156 bits: 24/23 c ---[1181]---> Sorter-cost:16336 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1179]---> Sorter-cost:15442 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1177]---> Sorter-cost:14605 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1175]---> Adder-cost: 1828 maxlim: 255759650 bits: 29/28 c ---[1173]---> Sorter-cost:17448 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1171]---> Adder-cost: 1726 maxlim: 209167150 bits: 29/28 c ---[1169]---> Sorter-cost:15783 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1167]---> Adder-cost: 642 maxlim: 9844609 bits: 24/24 c ---[1165]---> Adder-cost: 1608 maxlim: 129311730 bits: 28/27 c ---[1163]---> Adder-cost: 656 maxlim: 7501732 bits: 24/23 c ---[1161]---> Adder-cost: 908 maxlim: 43376224 bits: 27/26 c ---[1159]---> Adder-cost: 862 maxlim: 24433288 bits: 26/25 c ---[1157]---> Adder-cost: 1304 maxlim: 74169520 bits: 28/27 c ---[1155]---> Sorter-cost:17637 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1153]---> Adder-cost: 606 maxlim: 6220584 bits: 24/23 c ---[1151]---> Sorter-cost:17720 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1149]---> Adder-cost: 1226 maxlim: 47082420 bits: 27/26 c ---[1147]---> Adder-cost: 1724 maxlim: 294353375 bits: 30/29 c ---[1145]---> Sorter-cost:13564 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1143]---> Adder-cost: 1826 maxlim: 285337660 bits: 29/29 c ---[1141]---> Sorter-cost:14665 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1139]---> Sorter-cost:20008 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1137]---> Sorter-cost:15201 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1135]---> Sorter-cost:20836 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1133]---> Adder-cost: 1320 maxlim: 185403220 bits: 29/28 c ---[1131]---> Adder-cost: 828 maxlim: 23710612 bits: 26/25 c ---[1129]---> Sorter-cost:16253 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1127]---> Sorter-cost:22350 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1125]---> Sorter-cost:16425 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1123]---> Sorter-cost:12434 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1121]---> Sorter-cost:10742 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1119]---> Sorter-cost:21555 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1117]---> Sorter-cost:14443 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1115]---> Sorter-cost:11069 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1113]---> Adder-cost: 598 maxlim: 8263687 bits: 24/23 c ---[1111]---> Sorter-cost:14303 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1109]---> Adder-cost: 1374 maxlim: 76307190 bits: 28/27 c ---[1107]---> Adder-cost: 1148 maxlim: 132524060 bits: 28/27 c ---[1105]---> Sorter-cost:19664 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1103]---> Sorter-cost:21647 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1101]---> Sorter-cost:15685 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1099]---> Sorter-cost:16204 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1097]---> Sorter-cost:15595 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1095]---> Sorter-cost:17150 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1093]---> Sorter-cost:10426 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1091]---> Adder-cost: 1768 maxlim: 81247815 bits: 27/27 c ---[1089]---> Adder-cost: 772 maxlim: 12202373 bits: 24/24 c ---[1087]---> Adder-cost: 522 maxlim: 7204395 bits: 24/23 c ---[1085]---> Sorter-cost:17102 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1083]---> Adder-cost: 346 maxlim: 7597084 bits: 24/23 c ---[1081]---> Sorter-cost:15083 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1079]---> Sorter-cost:12535 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1077]---> Sorter-cost:17326 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1075]---> Adder-cost: 884 maxlim: 37262720 bits: 26/26 c ---[1073]---> Adder-cost: 2066 maxlim: 854072400 bits: 31/30 c ---[1071]---> Sorter-cost:15111 Base: 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1069]---> Sorter-cost:11786 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1067]---> Adder-cost: 514 maxlim: 4815363 bits: 24/23 c ---[1065]---> Sorter-cost:12839 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1063]---> Adder-cost: 604 maxlim: 7157787 bits: 24/23 c ---[1061]---> Sorter-cost:21978 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1059]---> Adder-cost: 1152 maxlim: 275525920 bits: 29/29 c ---[1057]---> Sorter-cost:15137 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1055]---> Adder-cost: 1591 maxlim: 127380050 bits: 28/27 c ---[1053]---> Sorter-cost:21358 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1051]---> Sorter-cost:13014 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1049]---> Sorter-cost:11686 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1047]---> Sorter-cost:14540 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1045]---> Adder-cost: 662 maxlim: 8795920 bits: 24/24 c ---[1043]---> Sorter-cost:14810 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1041]---> Adder-cost: 600 maxlim: 10024167 bits: 24/24 c ---[1039]---> Adder-cost: 602 maxlim: 12367778 bits: 24/24 c ---[1037]---> Sorter-cost:15893 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1035]---> Sorter-cost:13096 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1033]---> Sorter-cost:14664 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1031]---> Sorter-cost:10115 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1029]---> Adder-cost: 1286 maxlim: 37712315 bits: 27/26 c ---[1027]---> Sorter-cost:15015 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1025]---> Adder-cost: 340 maxlim: 7600156 bits: 24/23 c ---[1023]---> Sorter-cost:13000 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1021]---> Adder-cost: 476 maxlim: 7302637 bits: 24/23 c ---[1019]---> Adder-cost: 630 maxlim: 5380477 bits: 24/23 c ---[1017]---> Sorter-cost:14088 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1015]---> Adder-cost: 600 maxlim: 5866535 bits: 24/23 c ---[1013]---> Adder-cost: 594 maxlim: 6792726 bits: 24/23 c ---[1011]---> Sorter-cost:23446 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1009]---> Adder-cost: 618 maxlim: 5981109 bits: 24/23 c ---[1007]---> Sorter-cost:12223 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1005]---> Adder-cost: 1200 maxlim: 140209990 bits: 28/28 c ---[1003]---> Sorter-cost:16415 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1001]---> Sorter-cost:22445 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 999]---> Sorter-cost:16794 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 997]---> Sorter-cost:21496 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 995]---> Adder-cost: 510 maxlim: 4444317 bits: 23/23 c ---[ 993]---> Sorter-cost:13232 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 991]---> Sorter-cost:16689 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 989]---> Adder-cost: 452 maxlim: 6551581 bits: 23/23 c ---[ 987]---> Sorter-cost:11552 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 985]---> Adder-cost: 630 maxlim: 8632259 bits: 24/24 c ---[ 983]---> Sorter-cost:16568 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 981]---> Sorter-cost:14516 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 979]---> Sorter-cost:19466 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 977]---> Sorter-cost:15432 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 975]---> Sorter-cost:16349 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 973]---> Adder-cost: 618 maxlim: 14480336 bits: 24/24 c ---[ 971]---> Sorter-cost:17119 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 969]---> Adder-cost: 1010 maxlim: 74168390 bits: 27/27 c ---[ 967]---> Adder-cost: 1788 maxlim: 1031662200 bits: 31/30 c ---[ 965]---> Sorter-cost:18669 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 963]---> Adder-cost: 582 maxlim: 7759389 bits: 24/23 c ---[ 961]---> Adder-cost: 560 maxlim: 10962290 bits: 24/24 c ---[ 959]---> Sorter-cost:16538 Base: 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 957]---> Adder-cost: 1110 maxlim: 195870020 bits: 28/28 c ---[ 955]---> Adder-cost: 1432 maxlim: 83814780 bits: 28/27 c ---[ 953]---> Adder-cost: 548 maxlim: 7745798 bits: 24/23 c ---[ 951]---> Sorter-cost:21680 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 949]---> Sorter-cost:15857 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 947]---> Sorter-cost:12792 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 945]---> Adder-cost: 1680 maxlim: 442619625 bits: 30/29 c ---[ 943]---> Sorter-cost:15749 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 941]---> Sorter-cost:16430 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 939]---> Sorter-cost:23337 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 937]---> Adder-cost: 1132 maxlim: 61838340 bits: 27/26 c ---[ 935]---> Sorter-cost:18570 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 933]---> Sorter-cost:15595 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 931]---> Sorter-cost:11804 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 929]---> Adder-cost: 652 maxlim: 10991511 bits: 24/24 c ---[ 927]---> Sorter-cost:14726 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 925]---> Sorter-cost:13482 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 923]---> Sorter-cost:12471 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 921]---> Adder-cost: 646 maxlim: 16283642 bits: 25/24 c ---[ 919]---> Adder-cost: 788 maxlim: 9648231 bits: 25/24 c ---[ 917]---> Sorter-cost:16275 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 915]---> Sorter-cost:13301 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 913]---> Adder-cost: 1108 maxlim: 121639020 bits: 28/27 c ---[ 911]---> Adder-cost: 1213 maxlim: 127375580 bits: 28/27 c ---[ 909]---> Adder-cost: 1202 maxlim: 31327455 bits: 26/25 c ---[ 907]---> Adder-cost: 620 maxlim: 4659101 bits: 24/23 c ---[ 905]---> Sorter-cost:16232 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 903]---> Sorter-cost:14634 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 901]---> Adder-cost: 626 maxlim: 8865496 bits: 24/24 c ---[ 899]---> Sorter-cost:14377 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 897]---> Adder-cost: 646 maxlim: 8103412 bits: 24/23 c ---[ 895]---> Adder-cost: 1686 maxlim: 662431950 bits: 31/30 c ---[ 893]---> Adder-cost: 648 maxlim: 8990898 bits: 24/24 c ---[ 891]---> Sorter-cost:17165 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 889]---> Sorter-cost:20453 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 887]---> Adder-cost: 1194 maxlim: 134188380 bits: 28/27 c ---[ 885]---> Sorter-cost:15487 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 883]---> Sorter-cost:11161 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 881]---> Sorter-cost:19695 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 879]---> Adder-cost: 598 maxlim: 8575027 bits: 24/24 c ---[ 877]---> Sorter-cost:11713 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 875]---> Sorter-cost:18964 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 873]---> Sorter-cost:18195 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 871]---> Sorter-cost:13389 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 869]---> Adder-cost: 552 maxlim: 8631134 bits: 24/24 c ---[ 867]---> Sorter-cost:13865 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 865]---> Sorter-cost:12953 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 863]---> Sorter-cost:20043 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 861]---> Sorter-cost:15407 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 859]---> Sorter-cost:10260 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 857]---> Sorter-cost:11642 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 855]---> Sorter-cost:11885 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 853]---> Adder-cost: 410 maxlim: 6912054 bits: 24/23 c ---[ 851]---> Sorter-cost:13532 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 849]---> Adder-cost: 632 maxlim: 11711990 bits: 24/24 c ---[ 847]---> Sorter-cost:19835 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 845]---> Adder-cost: 476 maxlim: 9040731 bits: 24/24 c ---[ 843]---> Sorter-cost:15336 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 841]---> Sorter-cost:13898 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 839]---> Sorter-cost:22701 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 837]---> Sorter-cost:10886 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 835]---> Sorter-cost:12436 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 833]---> Adder-cost: 680 maxlim: 9939599 bits: 24/24 c ---[ 831]---> Sorter-cost:14926 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 829]---> Adder-cost: 592 maxlim: 7894414 bits: 24/23 c ---[ 827]---> Adder-cost: 1313 maxlim: 107439320 bits: 28/27 c ---[ 825]---> Sorter-cost:18693 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 823]---> Sorter-cost:23219 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 821]---> Sorter-cost:15915 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 819]---> Adder-cost: 650 maxlim: 12596464 bits: 24/24 c ---[ 817]---> Sorter-cost:16768 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 815]---> Adder-cost: 1062 maxlim: 106756940 bits: 28/27 c ---[ 813]---> Sorter-cost:20134 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 811]---> Adder-cost: 1224 maxlim: 146098520 bits: 28/28 c ---[ 809]---> Sorter-cost:14521 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 807]---> Sorter-cost:22617 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 805]---> Adder-cost: 1166 maxlim: 33945635 bits: 26/26 c ---[ 803]---> Sorter-cost:23793 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 801]---> Sorter-cost:11912 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 799]---> Sorter-cost:16346 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 797]---> Adder-cost: 1470 maxlim: 227477240 bits: 29/28 c ---[ 795]---> Adder-cost: 734 maxlim: 11505975 bits: 24/24 c ---[ 793]---> Adder-cost: 378 maxlim: 5863095 bits: 24/23 c ---[ 791]---> Sorter-cost:11508 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 789]---> Adder-cost: 418 maxlim: 6219703 bits: 23/23 c ---[ 787]---> Adder-cost: 584 maxlim: 8878231 bits: 24/24 c ---[ 785]---> Sorter-cost:13081 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 783]---> Sorter-cost:14020 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 781]---> Adder-cost: 592 maxlim: 9340552 bits: 24/24 c ---[ 779]---> Sorter-cost:15379 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 777]---> Sorter-cost:17482 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 775]---> Adder-cost: 1164 maxlim: 37668740 bits: 27/26 c ---[ 773]---> Adder-cost: 408 maxlim: 5992797 bits: 23/23 c ---[ 771]---> Adder-cost: 1330 maxlim: 78935040 bits: 28/27 c ---[ 769]---> Sorter-cost:15854 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 767]---> Sorter-cost:18093 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 765]---> Sorter-cost:21759 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 763]---> Adder-cost: 1494 maxlim: 359452825 bits: 29/29 c ---[ 761]---> Adder-cost: 1814 maxlim: 1084401900 bits: 31/31 c ---[ 759]---> Adder-cost: 1352 maxlim: 241413960 bits: 29/28 c ---[ 757]---> Sorter-cost:20532 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 755]---> Sorter-cost:15010 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 753]---> Sorter-cost:13857 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 751]---> Adder-cost: 608 maxlim: 10057674 bits: 24/24 c ---[ 749]---> Adder-cost: 570 maxlim: 11188154 bits: 24/24 c ---[ 747]---> Sorter-cost:14904 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 745]---> Adder-cost: 736 maxlim: 8008902 bits: 24/23 c ---[ 743]---> Adder-cost: 1860 maxlim: 1205776200 bits: 31/31 c ---[ 741]---> Sorter-cost:18349 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 739]---> Adder-cost: 1146 maxlim: 171962180 bits: 28/28 c ---[ 737]---> Sorter-cost:15862 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 735]---> Sorter-cost:13669 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 733]---> Sorter-cost:15341 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 731]---> Sorter-cost:20629 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 729]---> Adder-cost: 1042 maxlim: 46575600 bits: 27/26 c ---[ 727]---> Sorter-cost:17353 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 725]---> Sorter-cost:15390 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 723]---> Sorter-cost:13211 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 721]---> Sorter-cost:15793 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 719]---> Adder-cost: 562 maxlim: 6141981 bits: 24/23 c ---[ 717]---> Sorter-cost:22664 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 715]---> Adder-cost: 636 maxlim: 4368127 bits: 24/23 c ---[ 713]---> Sorter-cost:18663 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 711]---> Sorter-cost:14890 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 709]---> Sorter-cost:15933 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 707]---> Sorter-cost:16610 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 705]---> Sorter-cost:12859 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 703]---> Sorter-cost:12932 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 701]---> Sorter-cost:12612 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 699]---> Adder-cost: 1240 maxlim: 71864780 bits: 28/27 c ---[ 697]---> Sorter-cost:15055 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 695]---> Sorter-cost:14583 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 693]---> Sorter-cost:14137 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 691]---> Adder-cost: 1412 maxlim: 42137960 bits: 27/26 c ---[ 689]---> Sorter-cost:15583 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 687]---> Adder-cost: 1402 maxlim: 300916080 bits: 29/29 c ---[ 685]---> Adder-cost: 1192 maxlim: 35368780 bits: 26/26 c ---[ 683]---> Sorter-cost:12654 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 681]---> Adder-cost: 470 maxlim: 5699280 bits: 24/23 c ---[ 679]---> Adder-cost: 462 maxlim: 5894121 bits: 24/23 c ---[ 677]---> Sorter-cost:15044 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 675]---> Sorter-cost:21299 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 673]---> Sorter-cost:18716 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 671]---> Sorter-cost:14529 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 669]---> Adder-cost: 530 maxlim: 12858856 bits: 24/24 c ---[ 667]---> Sorter-cost:19395 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 665]---> Adder-cost: 774 maxlim: 38059524 bits: 27/26 c ---[ 663]---> Sorter-cost:21969 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 661]---> Adder-cost: 468 maxlim: 6669281 bits: 24/23 c ---[ 659]---> Sorter-cost:22021 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 657]---> Adder-cost: 554 maxlim: 8088196 bits: 24/23 c ---[ 655]---> Sorter-cost:17103 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 653]---> Adder-cost: 568 maxlim: 5925058 bits: 24/23 c ---[ 651]---> Sorter-cost:13938 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 649]---> Sorter-cost:14636 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 647]---> Sorter-cost:16451 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 645]---> Adder-cost: 508 maxlim: 6952802 bits: 24/23 c ---[ 643]---> Sorter-cost:14839 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 641]---> Sorter-cost:21518 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 639]---> Adder-cost: 1572 maxlim: 98629925 bits: 28/27 c ---[ 637]---> Sorter-cost:15301 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 635]---> Sorter-cost:20375 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 633]---> Sorter-cost:15158 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 631]---> Sorter-cost:14147 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 629]---> Sorter-cost:15357 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 627]---> Sorter-cost:20224 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 625]---> Sorter-cost:19905 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 623]---> Adder-cost: 644 maxlim: 11528673 bits: 24/24 c ---[ 621]---> Sorter-cost:14242 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 619]---> Sorter-cost:14624 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 617]---> Adder-cost: 1056 maxlim: 156259740 bits: 28/28 c ---[ 615]---> Adder-cost: 1832 maxlim: 707112450 bits: 31/30 c ---[ 613]---> Sorter-cost:21078 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 611]---> Sorter-cost:19844 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 609]---> Adder-cost: 540 maxlim: 6117409 bits: 24/23 c ---[ 607]---> Adder-cost: 1694 maxlim: 550772150 bits: 31/30 c ---[ 605]---> Sorter-cost:16571 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 603]---> Adder-cost: 488 maxlim: 10381005 bits: 24/24 c ---[ 601]---> Sorter-cost:10588 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 599]---> Sorter-cost:17255 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 597]---> Sorter-cost:10942 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 595]---> Sorter-cost:15619 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 593]---> Sorter-cost:10773 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 591]---> Sorter-cost:14043 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 589]---> Sorter-cost:19191 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 587]---> Adder-cost: 1206 maxlim: 127362000 bits: 28/27 c ---[ 585]---> Adder-cost: 1676 maxlim: 807251500 bits: 31/30 c ---[ 583]---> Sorter-cost:13566 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 581]---> Sorter-cost:10605 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 579]---> Sorter-cost:15794 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 577]---> Adder-cost: 1252 maxlim: 99222680 bits: 28/27 c ---[ 575]---> Sorter-cost:16029 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 573]---> Sorter-cost:14797 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 571]---> Adder-cost: 1402 maxlim: 253434920 bits: 29/28 c ---[ 569]---> Adder-cost: 680 maxlim: 10022178 bits: 25/24 c ---[ 567]---> Adder-cost: 2186 maxlim: 609654725 bits: 30/30 c ---[ 565]---> Sorter-cost:14714 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 563]---> Adder-cost: 530 maxlim: 14267708 bits: 24/24 c ---[ 561]---> Adder-cost: 622 maxlim: 6681824 bits: 24/23 c ---[ 559]---> Sorter-cost:18812 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 557]---> Sorter-cost:14191 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 555]---> Adder-cost: 548 maxlim: 6060048 bits: 24/23 c ---[ 553]---> Adder-cost: 1068 maxlim: 39141200 bits: 27/26 c ---[ 551]---> Adder-cost: 570 maxlim: 6719579 bits: 24/23 c ---[ 549]---> Sorter-cost:12549 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 547]---> Adder-cost: 1952 maxlim: 569964000 bits: 30/30 c ---[ 545]---> Sorter-cost:13195 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 543]---> Adder-cost: 588 maxlim: 15250983 bits: 24/24 c ---[ 541]---> Sorter-cost:12148 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 539]---> Sorter-cost:19345 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 537]---> Adder-cost: 1142 maxlim: 193428560 bits: 29/28 c ---[ 535]---> Adder-cost: 488 maxlim: 6909749 bits: 24/23 c ---[ 533]---> Sorter-cost:13891 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 531]---> Sorter-cost:16016 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 529]---> Sorter-cost:19291 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 527]---> Sorter-cost:16957 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 525]---> Adder-cost: 1456 maxlim: 92041660 bits: 28/27 c ---[ 523]---> Adder-cost: 1776 maxlim: 465198700 bits: 30/29 c ---[ 521]---> Sorter-cost:22638 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 519]---> Adder-cost: 1694 maxlim: 380706625 bits: 30/29 c ---[ 517]---> Sorter-cost:15209 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 515]---> Sorter-cost:16850 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 513]---> Adder-cost: 1806 maxlim: 425357125 bits: 30/29 c ---[ 511]---> Sorter-cost:15879 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 509]---> Sorter-cost:17918 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 507]---> Sorter-cost:18711 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 505]---> Adder-cost: 1291 maxlim: 24200915 bits: 26/25 c ---[ 503]---> Adder-cost: 1136 maxlim: 149395160 bits: 28/28 c ---[ 501]---> Sorter-cost:13910 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 499]---> Sorter-cost:14119 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 497]---> Sorter-cost:15193 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 495]---> Adder-cost: 1452 maxlim: 143908340 bits: 29/28 c ---[ 493]---> Adder-cost: 1156 maxlim: 167417620 bits: 29/28 c ---[ 491]---> Sorter-cost:14223 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 489]---> Adder-cost: 582 maxlim: 6355710 bits: 24/23 c ---[ 487]---> Adder-cost: 512 maxlim: 6290110 bits: 24/23 c ---[ 485]---> Adder-cost: 1182 maxlim: 136452120 bits: 28/28 c ---[ 483]---> Adder-cost: 978 maxlim: 167087300 bits: 28/28 c ---[ 481]---> Adder-cost: 498 maxlim: 4602657 bits: 24/23 c ---[ 479]---> Adder-cost: 1469 maxlim: 488107800 bits: 30/29 c ---[ 477]---> Sorter-cost:19809 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 475]---> Sorter-cost:14507 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 473]---> Sorter-cost:16581 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 471]---> Sorter-cost:15972 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 469]---> Sorter-cost:13167 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 467]---> Sorter-cost:11362 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 465]---> Adder-cost: 1638 maxlim: 357104750 bits: 30/29 c ---[ 463]---> Sorter-cost:11803 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 461]---> Adder-cost: 624 maxlim: 25422784 bits: 26/25 c ---[ 459]---> Adder-cost: 1190 maxlim: 44106955 bits: 27/26 c ---[ 457]---> Sorter-cost:11882 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 455]---> Adder-cost: 728 maxlim: 7928502 bits: 24/23 c ---[ 453]---> Sorter-cost:15069 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 451]---> Sorter-cost:16676 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 449]---> Adder-cost: 554 maxlim: 9452246 bits: 24/24 c ---[ 447]---> Sorter-cost:17914 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 445]---> Sorter-cost:13819 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 443]---> Sorter-cost:15298 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 441]---> Sorter-cost:14224 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 439]---> Sorter-cost:15766 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 437]---> Sorter-cost:20649 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 435]---> Sorter-cost:22644 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 433]---> Sorter-cost:11292 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 431]---> Sorter-cost:14289 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 429]---> Sorter-cost:11248 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 427]---> Sorter-cost:11758 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 425]---> Sorter-cost:22158 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 423]---> Adder-cost: 528 maxlim: 5905134 bits: 24/23 c ---[ 421]---> Sorter-cost:25349 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 419]---> Sorter-cost:19798 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 417]---> Sorter-cost:17602 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 415]---> Adder-cost: 1258 maxlim: 219514200 bits: 29/28 c ---[ 413]---> Adder-cost: 1126 maxlim: 118265280 bits: 28/27 c ---[ 411]---> Adder-cost: 1214 maxlim: 27641475 bits: 26/25 c ---[ 409]---> Sorter-cost:16259 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 407]---> Sorter-cost:11205 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 405]---> Sorter-cost:13572 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 403]---> Adder-cost: 1131 maxlim: 19981915 bits: 26/25 c ---[ 401]---> Adder-cost: 468 maxlim: 6978296 bits: 24/23 c ---[ 399]---> Adder-cost: 822 maxlim: 20933712 bits: 26/25 c ---[ 397]---> Sorter-cost:14853 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 395]---> Adder-cost: 1768 maxlim: 620820800 bits: 31/30 c ---[ 393]---> Sorter-cost:13952 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 391]---> Adder-cost: 444 maxlim: 4422283 bits: 23/23 c ---[ 389]---> Sorter-cost:13681 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 387]---> Adder-cost: 480 maxlim: 5815043 bits: 24/23 c ---[ 385]---> Sorter-cost:17190 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 383]---> Adder-cost: 338 maxlim: 5864183 bits: 23/23 c ---[ 381]---> Sorter-cost:13695 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 379]---> Sorter-cost:17359 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 377]---> Adder-cost: 640 maxlim: 25684968 bits: 26/25 c ---[ 375]---> Sorter-cost:10971 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 373]---> Adder-cost: 1939 maxlim: 801030500 bits: 31/30 c ---[ 371]---> Adder-cost: 568 maxlim: 7060146 bits: 24/23 c ---[ 369]---> Sorter-cost:11569 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 367]---> Sorter-cost:16695 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 365]---> Sorter-cost:14840 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 363]---> Sorter-cost:16364 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 361]---> Sorter-cost:14386 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 359]---> Sorter-cost:16453 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 357]---> Adder-cost: 1046 maxlim: 151033200 bits: 28/28 c ---[ 355]---> Sorter-cost:16231 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 353]---> Sorter-cost:14138 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 351]---> Sorter-cost:14649 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 349]---> Sorter-cost:16440 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 347]---> Sorter-cost:14219 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 345]---> Sorter-cost:18546 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 343]---> Adder-cost: 496 maxlim: 6322856 bits: 24/23 c ---[ 341]---> Adder-cost: 1738 maxlim: 557215650 bits: 31/30 c ---[ 339]---> Adder-cost: 640 maxlim: 4979440 bits: 24/23 c ---[ 337]---> Adder-cost: 566 maxlim: 6331152 bits: 24/23 c ---[ 335]---> Sorter-cost:21408 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 333]---> Sorter-cost:15140 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 331]---> Sorter-cost:16161 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 329]---> Sorter-cost: 9351 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 327]---> Sorter-cost:13784 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 325]---> Adder-cost: 430 maxlim: 4533030 bits: 24/23 c ---[ 323]---> Adder-cost: 452 maxlim: 8305364 bits: 24/23 c ---[ 321]---> Sorter-cost:15558 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 319]---> Sorter-cost:19328 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 317]---> Adder-cost: 1000 maxlim: 44387430 bits: 27/26 c ---[ 315]---> Adder-cost: 1642 maxlim: 251779300 bits: 29/28 c ---[ 313]---> Sorter-cost:15384 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 311]---> Sorter-cost:16317 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 309]---> Adder-cost: 986 maxlim: 67487810 bits: 27/27 c ---[ 307]---> Sorter-cost:16806 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 305]---> Adder-cost: 1662 maxlim: 885422300 bits: 31/30 c ---[ 303]---> Adder-cost: 702 maxlim: 7846397 bits: 24/23 c ---[ 301]---> Sorter-cost:12434 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 299]---> Sorter-cost:16774 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 297]---> Sorter-cost:16427 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 295]---> Adder-cost: 1875 maxlim: 854289700 bits: 31/30 c ---[ 293]---> Sorter-cost:12970 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 291]---> Sorter-cost:13766 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 289]---> Adder-cost: 518 maxlim: 4659992 bits: 24/23 c ---[ 287]---> Sorter-cost:15200 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 285]---> Sorter-cost:20079 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 283]---> Adder-cost: 1020 maxlim: 21989070 bits: 26/25 c ---[ 281]---> Adder-cost: 594 maxlim: 6425317 bits: 24/23 c ---[ 279]---> Adder-cost: 598 maxlim: 5323463 bits: 24/23 c ---[ 277]---> Sorter-cost:13501 Base: 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 275]---> Sorter-cost:19539 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 273]---> Adder-cost: 650 maxlim: 8698449 bits: 24/24 c ---[ 271]---> Sorter-cost:15362 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 269]---> Sorter-cost:15701 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 267]---> Sorter-cost:21023 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 265]---> Adder-cost: 1610 maxlim: 461371850 bits: 30/29 c ---[ 263]---> Sorter-cost:13836 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 261]---> Sorter-cost:13332 Base: 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 259]---> Adder-cost: 836 maxlim: 22148568 bits: 26/25 c ---[ 257]---> Sorter-cost:12902 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 255]---> Sorter-cost:15836 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 253]---> Adder-cost: 1628 maxlim: 318246375 bits: 30/29 c ---[ 251]---> Sorter-cost:18086 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 249]---> Adder-cost: 547 maxlim: 3807998 bits: 23/22 c ---[ 247]---> Sorter-cost:20016 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 245]---> Sorter-cost:16049 Base: 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 243]---> Sorter-cost:22934 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 241]-
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/5962/stat): 5962 (minisat+_script) R 5961 5962 20728 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854999333 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/5962/statm): 174 3 169 147 0 27 0 [pid=5962] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=5963 New process pid=5964 New process pid=5965 execve syscall for /bin/sed executable One traced child (pid=5964) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=5965) exited with status: 0 One traced child (pid=5963) exited with status: 0 New process pid=5966 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fit1p.opb [startup+10.0044 s] Raw data (loadavg): 0.93 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 6211 0 0 0 929 32 0 0 25 0 1 0 1854999338 24944640 5920 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 6090 5920 145 145 0 5945 0 [pid=5966] vsize: 24360 Current children cumulated CPU time (s) 9.62 Current children cumulated vsize (Kb) 26484 [startup+20.0051 s] Raw data (loadavg): 0.94 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 6930 0 0 0 1927 34 0 0 25 0 1 0 1854999338 27267072 6474 4294967295 134512640 135094434 3221224432 3221220564 134600159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 6657 6474 145 145 0 6512 0 [pid=5966] vsize: 26628 Current children cumulated CPU time (s) 19.62 Current children cumulated vsize (Kb) 28752 [startup+30.0048 s] Raw data (loadavg): 0.95 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 7476 0 0 0 2924 36 0 0 25 0 1 0 1854999338 30089216 6936 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 7346 6936 145 145 0 7201 0 [pid=5966] vsize: 29384 Current children cumulated CPU time (s) 29.61 Current children cumulated vsize (Kb) 31508 [startup+40.0055 s] Raw data (loadavg): 0.96 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 8897 0 0 0 3917 41 0 0 25 0 1 0 1854999338 32722944 7782 4294967295 134512640 135094434 3221224432 3221220928 134676601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 7989 7782 145 145 0 7844 0 [pid=5966] vsize: 31956 Current children cumulated CPU time (s) 39.59 Current children cumulated vsize (Kb) 34080 [startup+50.0062 s] Raw data (loadavg): 0.96 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 9007 0 0 0 4916 42 0 0 25 0 1 0 1854999338 32923648 7860 4294967295 134512640 135094434 3221224432 3221221264 134600162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 8038 7860 145 145 0 7893 0 [pid=5966] vsize: 32152 Current children cumulated CPU time (s) 49.59 Current children cumulated vsize (Kb) 34276 [startup+60.0068 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 9551 0 0 0 5913 44 0 0 25 0 1 0 1854999338 37269504 8325 4294967295 134512640 135094434 3221224432 3221222512 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 9099 8325 145 145 0 8954 0 [pid=5966] vsize: 36396 Current children cumulated CPU time (s) 59.58 Current children cumulated vsize (Kb) 38520 [startup+70.0075 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 11324 0 0 0 6906 49 0 0 25 0 1 0 1854999338 41058304 9407 4294967295 134512640 135094434 3221224432 3221220400 134677351 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 10024 9407 145 145 0 9879 0 [pid=5966] vsize: 40096 Current children cumulated CPU time (s) 69.56 Current children cumulated vsize (Kb) 42220 [startup+80.0082 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 11821 0 0 0 7903 52 0 0 25 0 1 0 1854999338 42405888 9904 4294967295 134512640 135094434 3221224432 3221220208 134600241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 10353 9904 145 145 0 10208 0 [pid=5966] vsize: 41412 Current children cumulated CPU time (s) 79.56 Current children cumulated vsize (Kb) 43536 [startup+90.0089 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 12333 0 0 0 8900 54 0 0 25 0 1 0 1854999338 43548672 10377 4294967295 134512640 135094434 3221224432 3221220376 134676241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 10632 10377 145 145 0 10487 0 [pid=5966] vsize: 42528 Current children cumulated CPU time (s) 89.55 Current children cumulated vsize (Kb) 44652 [startup+100.009 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 12724 0 0 0 9897 55 0 0 25 0 1 0 1854999338 44531712 10726 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 10872 10726 145 145 0 10727 0 [pid=5966] vsize: 43488 Current children cumulated CPU time (s) 99.53 Current children cumulated vsize (Kb) 45612 [startup+110.011 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 13332 0 0 0 10894 57 0 0 25 0 1 0 1854999338 52150272 11250 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 12732 11250 145 145 0 12587 0 [pid=5966] vsize: 50928 Current children cumulated CPU time (s) 109.52 Current children cumulated vsize (Kb) 53052 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 13760 0 0 0 11892 58 0 0 25 0 1 0 1854999338 52834304 11539 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 12899 11539 145 145 0 12754 0 [pid=5966] vsize: 51596 Current children cumulated CPU time (s) 119.51 Current children cumulated vsize (Kb) 53720 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 14217 0 0 0 12890 59 0 0 25 0 1 0 1854999338 53768192 11889 4294967295 134512640 135094434 3221224432 3221219168 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 13127 11889 145 145 0 12982 0 [pid=5966] vsize: 52508 Current children cumulated CPU time (s) 129.5 Current children cumulated vsize (Kb) 54632 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 17375 0 0 0 13879 68 0 0 25 0 1 0 1854999338 60293120 13617 4294967295 134512640 135094434 3221224432 3221220996 134677085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 14720 13617 145 145 0 14575 0 [pid=5966] vsize: 58880 Current children cumulated CPU time (s) 139.48 Current children cumulated vsize (Kb) 61004 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 17721 0 0 0 14876 70 0 0 25 0 1 0 1854999338 60829696 13848 4294967295 134512640 135094434 3221224432 3221221012 134677077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 14851 13848 145 145 0 14706 0 [pid=5966] vsize: 59404 Current children cumulated CPU time (s) 149.47 Current children cumulated vsize (Kb) 61528 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 18228 0 0 0 15873 71 0 0 25 0 1 0 1854999338 61718528 14204 4294967295 134512640 135094434 3221224432 3221220548 134676380 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 15068 14204 145 145 0 14923 0 [pid=5966] vsize: 60272 Current children cumulated CPU time (s) 159.45 Current children cumulated vsize (Kb) 62396 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 18685 0 0 0 16871 72 0 0 25 0 1 0 1854999338 62824448 14622 4294967295 134512640 135094434 3221224432 3221221788 134676988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 15338 14622 145 145 0 15193 0 [pid=5966] vsize: 61352 Current children cumulated CPU time (s) 169.44 Current children cumulated vsize (Kb) 63476 [startup+180.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 19091 0 0 0 17869 73 0 0 25 0 1 0 1854999338 63328256 14799 4294967295 134512640 135094434 3221224432 3221221436 134676988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 15461 14799 145 145 0 15316 0 [pid=5966] vsize: 61844 Current children cumulated CPU time (s) 179.43 Current children cumulated vsize (Kb) 63968 [startup+190.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 19668 0 0 0 18866 75 0 0 25 0 1 0 1854999338 64507904 15251 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 15749 15251 145 145 0 15604 0 [pid=5966] vsize: 62996 Current children cumulated CPU time (s) 189.42 Current children cumulated vsize (Kb) 65120 [startup+200.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 20167 0 0 0 19863 77 0 0 25 0 1 0 1854999338 65638400 15708 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 16025 15708 145 145 0 15880 0 [pid=5966] vsize: 64100 Current children cumulated CPU time (s) 199.41 Current children cumulated vsize (Kb) 66224 [startup+210.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 20874 0 0 0 20858 80 0 0 25 0 1 0 1854999338 67092480 16281 4294967295 134512640 135094434 3221224432 3221221456 134677290 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 16380 16281 145 145 0 16235 0 [pid=5966] vsize: 65520 Current children cumulated CPU time (s) 209.39 Current children cumulated vsize (Kb) 67644 [startup+220.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 21220 0 0 0 21856 81 0 0 25 0 1 0 1854999338 80535552 16585 4294967295 134512640 135094434 3221224432 3221221024 134676294 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 19662 16585 145 145 0 19517 0 [pid=5966] vsize: 78648 Current children cumulated CPU time (s) 219.38 Current children cumulated vsize (Kb) 80772 [startup+230.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 21828 0 0 0 22852 83 0 0 25 0 1 0 1854999338 81952768 17151 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 20008 17151 145 145 0 19863 0 [pid=5966] vsize: 80032 Current children cumulated CPU time (s) 229.36 Current children cumulated vsize (Kb) 82156 [startup+240.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 22425 0 0 0 23849 84 0 0 25 0 1 0 1854999338 83148800 17588 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 20300 17588 145 145 0 20155 0 [pid=5966] vsize: 81200 Current children cumulated CPU time (s) 239.34 Current children cumulated vsize (Kb) 83324 [startup+250.017 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) T 5962 5962 20728 0 -1 0 22682 0 0 0 24848 85 0 0 25 0 1 0 1854999338 83521536 17766 4294967295 134512640 135094434 3221224432 3221219356 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5966/statm): 20391 17766 145 145 0 20246 0 [pid=5966] vsize: 81564 Current children cumulated CPU time (s) 249.34 Current children cumulated vsize (Kb) 83688 [startup+260.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 23441 0 0 0 25842 88 0 0 25 0 1 0 1854999338 84951040 18308 4294967295 134512640 135094434 3221224432 3221221728 134677049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 20740 18308 145 145 0 20595 0 [pid=5966] vsize: 82960 Current children cumulated CPU time (s) 259.31 Current children cumulated vsize (Kb) 85084 [startup+270.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 23869 0 0 0 26840 89 0 0 25 0 1 0 1854999338 85749760 18624 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 20935 18624 145 145 0 20790 0 [pid=5966] vsize: 83740 Current children cumulated CPU time (s) 269.3 Current children cumulated vsize (Kb) 85864 [startup+280.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 29715 0 0 0 27823 104 0 0 25 0 1 0 1854999338 97533952 21641 4294967295 134512640 135094434 3221224432 3221220576 134600151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 23812 21641 145 145 0 23667 0 [pid=5966] vsize: 95248 Current children cumulated CPU time (s) 279.28 Current children cumulated vsize (Kb) 97372 [startup+290.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 30269 0 0 0 28820 105 0 0 25 0 1 0 1854999338 98877440 22153 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 24140 22153 145 145 0 23995 0 [pid=5966] vsize: 96560 Current children cumulated CPU time (s) 289.26 Current children cumulated vsize (Kb) 98684 [startup+300.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 30919 0 0 0 29815 108 0 0 25 0 1 0 1854999338 100134912 22644 4294967295 134512640 135094434 3221224432 3221220732 134676382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 24447 22644 145 145 0 24302 0 [pid=5966] vsize: 97788 Current children cumulated CPU time (s) 299.24 Current children cumulated vsize (Kb) 99912 [startup+310.021 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) T 5962 5962 20728 0 -1 0 31644 0 0 0 30810 110 0 0 25 0 1 0 1854999338 101990400 23290 4294967295 134512640 135094434 3221224432 3221177452 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5966/statm): 24900 23290 145 145 0 24755 0 [pid=5966] vsize: 99600 Current children cumulated CPU time (s) 309.21 Current children cumulated vsize (Kb) 101724 [startup+320.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 32066 0 0 0 31808 111 0 0 25 0 1 0 1854999338 102445056 23506 4294967295 134512640 135094434 3221224432 3221220848 134676376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 25011 23506 145 145 0 24866 0 [pid=5966] vsize: 100044 Current children cumulated CPU time (s) 319.2 Current children cumulated vsize (Kb) 102168 [startup+330.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 32513 0 0 0 32805 113 0 0 25 0 1 0 1854999338 103550976 23953 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 25281 23953 145 145 0 25136 0 [pid=5966] vsize: 101124 Current children cumulated CPU time (s) 329.19 Current children cumulated vsize (Kb) 103248 [startup+340.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 33288 0 0 0 33799 116 0 0 25 0 1 0 1854999338 105050112 24549 4294967295 134512640 135094434 3221224432 3221219520 134677340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 25647 24549 145 145 0 25502 0 [pid=5966] vsize: 102588 Current children cumulated CPU time (s) 339.16 Current children cumulated vsize (Kb) 104712 [startup+350.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 33422 0 0 0 34799 116 0 0 25 0 1 0 1854999338 105312256 24644 4294967295 134512640 135094434 3221224432 3221221456 134677320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 25711 24644 145 145 0 25566 0 [pid=5966] vsize: 102844 Current children cumulated CPU time (s) 349.16 Current children cumulated vsize (Kb) 104968 [startup+360.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 33930 0 0 0 35797 117 0 0 25 0 1 0 1854999338 106491904 25069 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 25999 25069 145 145 0 25854 0 [pid=5966] vsize: 103996 Current children cumulated CPU time (s) 359.15 Current children cumulated vsize (Kb) 106120 [startup+370.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 34279 0 0 0 36795 118 0 0 25 0 1 0 1854999338 107212800 25379 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 26175 25379 145 145 0 26030 0 [pid=5966] vsize: 104700 Current children cumulated CPU time (s) 369.14 Current children cumulated vsize (Kb) 106824 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 34568 0 0 0 37793 119 0 0 25 0 1 0 1854999338 107839488 25584 4294967295 134512640 135094434 3221224432 3221219848 134676989 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 26328 25584 145 145 0 26183 0 [pid=5966] vsize: 105312 Current children cumulated CPU time (s) 379.13 Current children cumulated vsize (Kb) 107436 [startup+390.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 35015 0 0 0 38791 120 0 0 25 0 1 0 1854999338 108802048 25989 4294967295 134512640 135094434 3221224432 3221221168 134676341 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 26563 25989 145 145 0 26418 0 [pid=5966] vsize: 106252 Current children cumulated CPU time (s) 389.12 Current children cumulated vsize (Kb) 108376 [startup+400.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 35671 0 0 0 39787 122 0 0 25 0 1 0 1854999338 110284800 26562 4294967295 134512640 135094434 3221224432 3221219936 134677086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 26925 26562 145 145 0 26780 0 [pid=5966] vsize: 107700 Current children cumulated CPU time (s) 399.1 Current children cumulated vsize (Kb) 109824 [startup+410.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 36014 0 0 0 40783 124 0 0 25 0 1 0 1854999338 111136768 26873 4294967295 134512640 135094434 3221224432 3221221104 134677366 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 27133 26873 145 145 0 26988 0 [pid=5966] vsize: 108532 Current children cumulated CPU time (s) 409.08 Current children cumulated vsize (Kb) 110656 [startup+420.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 36472 0 0 0 41780 126 0 0 25 0 1 0 1854999338 112087040 27252 4294967295 134512640 135094434 3221224432 3221220848 134677049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 27365 27252 145 145 0 27220 0 [pid=5966] vsize: 109460 Current children cumulated CPU time (s) 419.07 Current children cumulated vsize (Kb) 111584 [startup+430.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 36800 0 0 0 42777 127 0 0 25 0 1 0 1854999338 137973760 27541 4294967295 134512640 135094434 3221224432 3221221024 134677056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 33685 27541 145 145 0 33540 0 [pid=5966] vsize: 134740 Current children cumulated CPU time (s) 429.05 Current children cumulated vsize (Kb) 136864 [startup+440.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 37392 0 0 0 43774 129 0 0 25 0 1 0 1854999338 139472896 28091 4294967295 134512640 135094434 3221224432 3221220672 134677028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 34051 28091 145 145 0 33906 0 [pid=5966] vsize: 136204 Current children cumulated CPU time (s) 439.04 Current children cumulated vsize (Kb) 138328 [startup+450.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 38129 0 0 0 44770 131 0 0 25 0 1 0 1854999338 141189120 28786 4294967295 134512640 135094434 3221224432 3221220216 134600234 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 34470 28786 145 145 0 34325 0 [pid=5966] vsize: 137880 Current children cumulated CPU time (s) 449.02 Current children cumulated vsize (Kb) 140004 [startup+460.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 38877 0 0 0 45765 134 0 0 25 0 1 0 1854999338 142659584 29359 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 34829 29359 145 145 0 34684 0 [pid=5966] vsize: 139316 Current children cumulated CPU time (s) 459 Current children cumulated vsize (Kb) 141440 [startup+470.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 39647 0 0 0 46759 136 0 0 25 0 1 0 1854999338 144359424 30004 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 35244 30004 145 145 0 35099 0 [pid=5966] vsize: 140976 Current children cumulated CPU time (s) 468.96 Current children cumulated vsize (Kb) 143100 [startup+480.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 39940 0 0 0 47757 138 0 0 25 0 1 0 1854999338 145018880 30258 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 35405 30258 145 145 0 35260 0 [pid=5966] vsize: 141620 Current children cumulated CPU time (s) 478.96 Current children cumulated vsize (Kb) 143744 [startup+490.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 40580 0 0 0 48753 140 0 0 25 0 1 0 1854999338 146382848 30785 4294967295 134512640 135094434 3221224432 3221220848 134677028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 35738 30785 145 145 0 35593 0 [pid=5966] vsize: 142952 Current children cumulated CPU time (s) 488.94 Current children cumulated vsize (Kb) 145076 [startup+500.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 40905 0 0 0 49751 141 0 0 25 0 1 0 1854999338 147206144 31068 4294967295 134512640 135094434 3221224432 3221221336 134677377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 35939 31068 145 145 0 35794 0 [pid=5966] vsize: 143756 Current children cumulated CPU time (s) 498.93 Current children cumulated vsize (Kb) 145880 [startup+510.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 41522 0 0 0 50748 143 0 0 25 0 1 0 1854999338 148500480 31604 4294967295 134512640 135094434 3221224432 3221221808 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 36255 31604 145 145 0 36110 0 [pid=5966] vsize: 145020 Current children cumulated CPU time (s) 508.92 Current children cumulated vsize (Kb) 147144 [startup+520.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 42048 0 0 0 51744 145 0 0 25 0 1 0 1854999338 149753856 32088 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 36561 32088 145 145 0 36416 0 [pid=5966] vsize: 146244 Current children cumulated CPU time (s) 518.9 Current children cumulated vsize (Kb) 148368 [startup+530.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 52922 0 0 0 52719 171 0 0 25 0 1 0 1854999338 172093440 37650 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 42015 37650 145 145 0 41870 0 [pid=5966] vsize: 168060 Current children cumulated CPU time (s) 528.91 Current children cumulated vsize (Kb) 170184 [startup+540.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 53584 0 0 0 53715 172 0 0 25 0 1 0 1854999338 173162496 38074 4294967295 134512640 135094434 3221224432 3221220120 134677084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 42276 38074 145 145 0 42131 0 [pid=5966] vsize: 169104 Current children cumulated CPU time (s) 538.88 Current children cumulated vsize (Kb) 171228 [startup+550.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 53714 0 0 0 54714 173 0 0 25 0 1 0 1854999338 173563904 38204 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 42374 38204 145 145 0 42229 0 [pid=5966] vsize: 169496 Current children cumulated CPU time (s) 548.88 Current children cumulated vsize (Kb) 171620 [startup+560.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 54310 0 0 0 55710 175 0 0 25 0 1 0 1854999338 174456832 38573 4294967295 134512640 135094434 3221224432 3221221528 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 42592 38573 145 145 0 42447 0 [pid=5966] vsize: 170368 Current children cumulated CPU time (s) 558.86 Current children cumulated vsize (Kb) 172492 [startup+570.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 54659 0 0 0 56708 177 0 0 25 0 1 0 1854999338 175194112 38850 4294967295 134512640 135094434 3221224432 3221219872 134600337 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 42772 38850 145 145 0 42627 0 [pid=5966] vsize: 171088 Current children cumulated CPU time (s) 568.86 Current children cumulated vsize (Kb) 173212 [startup+580.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 55202 0 0 0 57705 178 0 0 25 0 1 0 1854999338 176369664 39310 4294967295 134512640 135094434 3221224432 3221220576 134676471 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 43059 39310 145 145 0 42914 0 [pid=5966] vsize: 172236 Current children cumulated CPU time (s) 578.84 Current children cumulated vsize (Kb) 174360 [startup+590.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 55818 0 0 0 58701 180 0 0 25 0 1 0 1854999338 177545216 39768 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 43346 39768 145 145 0 43201 0 [pid=5966] vsize: 173384 Current children cumulated CPU time (s) 588.82 Current children cumulated vsize (Kb) 175508 [startup+600.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 56139 0 0 0 59699 181 0 0 25 0 1 0 1854999338 178397184 40089 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 43554 40089 145 145 0 43409 0 [pid=5966] vsize: 174216 Current children cumulated CPU time (s) 598.81 Current children cumulated vsize (Kb) 176340 [startup+610.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 56657 0 0 0 60696 183 0 0 25 0 1 0 1854999338 179630080 40565 4294967295 134512640 135094434 3221224432 3221221200 134676999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 43855 40565 145 145 0 43710 0 [pid=5966] vsize: 175420 Current children cumulated CPU time (s) 608.8 Current children cumulated vsize (Kb) 177544 [startup+620.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 57156 0 0 0 61693 185 0 0 25 0 1 0 1854999338 180822016 41024 4294967295 134512640 135094434 3221224432 3221221280 134676595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 44146 41024 145 145 0 44001 0 [pid=5966] vsize: 176584 Current children cumulated CPU time (s) 618.79 Current children cumulated vsize (Kb) 178708 [startup+630.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 57710 0 0 0 62691 185 0 0 25 0 1 0 1854999338 182317056 41578 4294967295 134512640 135094434 3221224432 3221221200 134677138 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 44511 41578 145 145 0 44366 0 [pid=5966] vsize: 178044 Current children cumulated CPU time (s) 628.77 Current children cumulated vsize (Kb) 180168 [startup+640.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 58156 0 0 0 63688 187 0 0 25 0 1 0 1854999338 183291904 41984 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 44749 41984 145 145 0 44604 0 [pid=5966] vsize: 178996 Current children cumulated CPU time (s) 638.76 Current children cumulated vsize (Kb) 181120 [startup+650.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 58733 0 0 0 64683 190 0 0 25 0 1 0 1854999338 184713216 42529 4294967295 134512640 135094434 3221224432 3221221168 134676336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 45096 42529 145 145 0 44951 0 [pid=5966] vsize: 180384 Current children cumulated CPU time (s) 648.74 Current children cumulated vsize (Kb) 182508 [startup+660.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 59264 0 0 0 65679 192 0 0 25 0 1 0 1854999338 185769984 42912 4294967295 134512640 135094434 3221224432 3221221104 134676589 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 45354 42912 145 145 0 45209 0 [pid=5966] vsize: 181416 Current children cumulated CPU time (s) 658.72 Current children cumulated vsize (Kb) 183540 [startup+670.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 59645 0 0 0 66677 193 0 0 25 0 1 0 1854999338 186703872 43293 4294967295 134512640 135094434 3221224432 3221222308 134676992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 45582 43293 145 145 0 45437 0 [pid=5966] vsize: 182328 Current children cumulated CPU time (s) 668.71 Current children cumulated vsize (Kb) 184452 [startup+680.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 60262 0 0 0 67673 195 0 0 25 0 1 0 1854999338 188252160 43868 4294967295 134512640 135094434 3221224432 3221220752 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 45960 43868 145 145 0 45815 0 [pid=5966] vsize: 183840 Current children cumulated CPU time (s) 678.69 Current children cumulated vsize (Kb) 185964 [startup+690.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 60755 0 0 0 68671 196 0 0 25 0 1 0 1854999338 189358080 44319 4294967295 134512640 135094434 3221224432 3221220472 134677084 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 46230 44319 145 145 0 46085 0 [pid=5966] vsize: 184920 Current children cumulated CPU time (s) 688.68 Current children cumulated vsize (Kb) 187044 [startup+700.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 61183 0 0 0 69669 197 0 0 25 0 1 0 1854999338 190271488 44668 4294967295 134512640 135094434 3221224432 3221220048 134676503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 46453 44668 145 145 0 46308 0 [pid=5966] vsize: 185812 Current children cumulated CPU time (s) 698.67 Current children cumulated vsize (Kb) 187936 [startup+710.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 61412 0 0 0 70667 198 0 0 25 0 1 0 1854999338 190853120 44897 4294967295 134512640 135094434 3221224432 3221220848 134677065 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 46595 44897 145 145 0 46450 0 [pid=5966] vsize: 186380 Current children cumulated CPU time (s) 708.66 Current children cumulated vsize (Kb) 188504 [startup+720.048 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) T 5962 5962 20728 0 -1 0 61894 0 0 0 71665 200 0 0 25 0 1 0 1854999338 192061440 45379 4294967295 134512640 135094434 3221224432 3221219436 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5966/statm): 46890 45379 145 145 0 46745 0 [pid=5966] vsize: 187560 Current children cumulated CPU time (s) 718.66 Current children cumulated vsize (Kb) 189684 [startup+730.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 62501 0 0 0 72661 201 0 0 25 0 1 0 1854999338 193478656 45907 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 47236 45907 145 145 0 47091 0 [pid=5966] vsize: 188944 Current children cumulated CPU time (s) 728.63 Current children cumulated vsize (Kb) 191068 [startup+740.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 62796 0 0 0 73659 202 0 0 25 0 1 0 1854999338 194043904 46137 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 47374 46137 145 145 0 47229 0 [pid=5966] vsize: 189496 Current children cumulated CPU time (s) 738.62 Current children cumulated vsize (Kb) 191620 [startup+750.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 63381 0 0 0 74656 204 0 0 25 0 1 0 1854999338 195059712 46530 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 47622 46530 145 145 0 47477 0 [pid=5966] vsize: 190488 Current children cumulated CPU time (s) 748.61 Current children cumulated vsize (Kb) 192612 [startup+760.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 63558 0 0 0 75654 205 0 0 25 0 1 0 1854999338 195346432 46629 4294967295 134512640 135094434 3221224432 3221221200 134676294 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 47692 46629 145 145 0 47547 0 [pid=5966] vsize: 190768 Current children cumulated CPU time (s) 758.6 Current children cumulated vsize (Kb) 192892 [startup+770.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 64027 0 0 0 76651 207 0 0 25 0 1 0 1854999338 196395008 47017 4294967295 134512640 135094434 3221224432 3221220400 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 47948 47017 145 145 0 47803 0 [pid=5966] vsize: 191792 Current children cumulated CPU time (s) 768.59 Current children cumulated vsize (Kb) 193916 [startup+780.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 64347 0 0 0 77650 208 0 0 25 0 1 0 1854999338 197144576 47337 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 48131 47337 145 145 0 47986 0 [pid=5966] vsize: 192524 Current children cumulated CPU time (s) 778.59 Current children cumulated vsize (Kb) 194648 [startup+790.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 64816 0 0 0 78646 210 0 0 25 0 1 0 1854999338 198262784 47764 4294967295 134512640 135094434 3221224432 3221219968 134676321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 48404 47764 145 145 0 48259 0 [pid=5966] vsize: 193616 Current children cumulated CPU time (s) 788.57 Current children cumulated vsize (Kb) 195740 [startup+800.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 65383 0 0 0 79643 213 0 0 25 0 1 0 1854999338 199151616 48108 4294967295 134512640 135094434 3221224432 3221220308 134677077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 48621 48108 145 145 0 48476 0 [pid=5966] vsize: 194484 Current children cumulated CPU time (s) 798.57 Current children cumulated vsize (Kb) 196608 [startup+810.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 65608 0 0 0 80642 213 0 0 25 0 1 0 1854999338 199692288 48291 4294967295 134512640 135094434 3221224432 3221222316 134676240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 48753 48291 145 145 0 48608 0 [pid=5966] vsize: 195012 Current children cumulated CPU time (s) 808.56 Current children cumulated vsize (Kb) 197136 [startup+820.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 65976 0 0 0 81641 214 0 0 25 0 1 0 1854999338 200282112 48538 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 48897 48538 145 145 0 48752 0 [pid=5966] vsize: 195588 Current children cumulated CPU time (s) 818.56 Current children cumulated vsize (Kb) 197712 [startup+830.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 66528 0 0 0 82638 216 0 0 25 0 1 0 1854999338 201453568 48979 4294967295 134512640 135094434 3221224432 3221220904 134677149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 49183 48979 145 145 0 49038 0 [pid=5966] vsize: 196732 Current children cumulated CPU time (s) 828.55 Current children cumulated vsize (Kb) 198856 [startup+840.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 67010 0 0 0 83635 218 0 0 25 0 1 0 1854999338 252862464 49420 4294967295 134512640 135094434 3221224432 3221222080 134677049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 61734 49420 145 145 0 61589 0 [pid=5966] vsize: 246936 Current children cumulated CPU time (s) 838.54 Current children cumulated vsize (Kb) 249060 [startup+850.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 67428 0 0 0 84631 220 0 0 25 0 1 0 1854999338 253370368 49584 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 61858 49584 145 145 0 61713 0 [pid=5966] vsize: 247432 Current children cumulated CPU time (s) 848.52 Current children cumulated vsize (Kb) 249556 [startup+860.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 67890 0 0 0 85629 221 0 0 25 0 1 0 1854999338 254545920 50046 4294967295 134512640 135094434 3221224432 3221220632 134676609 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 62145 50046 145 145 0 62000 0 [pid=5966] vsize: 248580 Current children cumulated CPU time (s) 858.51 Current children cumulated vsize (Kb) 250704 [startup+870.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 68302 0 0 0 86628 221 0 0 25 0 1 0 1854999338 255340544 50377 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 62339 50377 145 145 0 62194 0 [pid=5966] vsize: 249356 Current children cumulated CPU time (s) 868.5 Current children cumulated vsize (Kb) 251480 [startup+880.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 68634 0 0 0 87626 223 0 0 25 0 1 0 1854999338 255987712 50627 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 62497 50627 145 145 0 62352 0 [pid=5966] vsize: 249988 Current children cumulated CPU time (s) 878.5 Current children cumulated vsize (Kb) 252112 [startup+890.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 69052 0 0 0 88624 224 0 0 25 0 1 0 1854999338 257015808 51003 4294967295 134512640 135094434 3221224432 3221221632 134676510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 62748 51003 145 145 0 62603 0 [pid=5966] vsize: 250992 Current children cumulated CPU time (s) 888.49 Current children cumulated vsize (Kb) 253116 [startup+900.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 69562 0 0 0 89621 226 0 0 25 0 1 0 1854999338 258142208 51429 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 63023 51429 145 145 0 62878 0 [pid=5966] vsize: 252092 Current children cumulated CPU time (s) 898.48 Current children cumulated vsize (Kb) 254216 [startup+910.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 70253 0 0 0 90618 227 0 0 25 0 1 0 1854999338 259600384 51994 4294967295 134512640 135094434 3221224432 3221220752 134676480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 63379 51994 145 145 0 63234 0 [pid=5966] vsize: 253516 Current children cumulated CPU time (s) 908.46 Current children cumulated vsize (Kb) 255640 [startup+920.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 70859 0 0 0 91614 230 0 0 25 0 1 0 1854999338 260546560 52366 4294967295 134512640 135094434 3221224432 3221220400 134600307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 63610 52366 145 145 0 63465 0 [pid=5966] vsize: 254440 Current children cumulated CPU time (s) 918.45 Current children cumulated vsize (Kb) 256564 [startup+930.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 71290 0 0 0 92612 231 0 0 25 0 1 0 1854999338 261505024 52755 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 63844 52755 145 145 0 63699 0 [pid=5966] vsize: 255376 Current children cumulated CPU time (s) 928.44 Current children cumulated vsize (Kb) 257500 [startup+940.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 71704 0 0 0 93611 232 0 0 25 0 1 0 1854999338 262258688 53058 4294967295 134512640 135094434 3221224432 3221221456 134677363 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 64028 53058 145 145 0 63883 0 [pid=5966] vsize: 256112 Current children cumulated CPU time (s) 938.44 Current children cumulated vsize (Kb) 258236 [startup+950.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 72103 0 0 0 94608 233 0 0 25 0 1 0 1854999338 263061504 53332 4294967295 134512640 135094434 3221224432 3221220400 134600267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 64224 53332 145 145 0 64079 0 [pid=5966] vsize: 256896 Current children cumulated CPU time (s) 948.42 Current children cumulated vsize (Kb) 259020 [startup+960.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 72621 0 0 0 95605 235 0 0 25 0 1 0 1854999338 263966720 53682 4294967295 134512640 135094434 3221224432 3221220484 134677077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 64445 53682 145 145 0 64300 0 [pid=5966] vsize: 257780 Current children cumulated CPU time (s) 958.41 Current children cumulated vsize (Kb) 259904 [startup+970.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 72991 0 0 0 96603 236 0 0 25 0 1 0 1854999338 264724480 54010 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 64630 54010 145 145 0 64485 0 [pid=5966] vsize: 258520 Current children cumulated CPU time (s) 968.4 Current children cumulated vsize (Kb) 260644 [startup+980.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 73285 0 0 0 97601 237 0 0 25 0 1 0 1854999338 265457664 54265 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 64809 54265 145 145 0 64664 0 [pid=5966] vsize: 259236 Current children cumulated CPU time (s) 978.39 Current children cumulated vsize (Kb) 261360 [startup+990.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 73588 0 0 0 98600 238 0 0 25 0 1 0 1854999338 266149888 54526 4294967295 134512640 135094434 3221224432 3221220928 134600215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 64978 54526 145 145 0 64833 0 [pid=5966] vsize: 259912 Current children cumulated CPU time (s) 988.39 Current children cumulated vsize (Kb) 262036 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 74028 0 0 0 99597 239 0 0 25 0 1 0 1854999338 267112448 54902 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 65213 54902 145 145 0 65068 0 [pid=5966] vsize: 260852 Current children cumulated CPU time (s) 998.37 Current children cumulated vsize (Kb) 262976 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 74541 0 0 0 100594 241 0 0 25 0 1 0 1854999338 268275712 55383 4294967295 134512640 135094434 3221224432 3221220928 134677278 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5966/statm): 65497 55383 145 145 0 65352 0 [pid=5966] vsize: 261988 Current children cumulated CPU time (s) 1008.36 Current children cumulated vsize (Kb) 264112 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 74793 0 0 0 101591 242 0 0 25 0 1 0 1854999338 268632064 55519 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 65584 55519 145 145 0 65439 0 [pid=5966] vsize: 262336 Current children cumulated CPU time (s) 1018.34 Current children cumulated vsize (Kb) 264460 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 75183 0 0 0 102589 244 0 0 25 0 1 0 1854999338 269668352 55909 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 65837 55909 145 145 0 65692 0 [pid=5966] vsize: 263348 Current children cumulated CPU time (s) 1028.34 Current children cumulated vsize (Kb) 265472 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 75624 0 0 0 103587 245 0 0 25 0 1 0 1854999338 270475264 56197 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 66034 56197 145 145 0 65889 0 [pid=5966] vsize: 264136 Current children cumulated CPU time (s) 1038.33 Current children cumulated vsize (Kb) 266260 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 76145 0 0 0 104584 247 0 0 25 0 1 0 1854999338 271224832 56492 4294967295 134512640 135094434 3221224432 3221221536 134676328 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 66217 56492 145 145 0 66072 0 [pid=5966] vsize: 264868 Current children cumulated CPU time (s) 1048.32 Current children cumulated vsize (Kb) 266992 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 76724 0 0 0 105580 249 0 0 25 0 1 0 1854999338 271978496 56776 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 66401 56776 145 145 0 66256 0 [pid=5966] vsize: 265604 Current children cumulated CPU time (s) 1058.3 Current children cumulated vsize (Kb) 267728 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 77022 0 0 0 106578 250 0 0 25 0 1 0 1854999338 272650240 57036 4294967295 134512640 135094434 3221224432 3221221104 134599964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 66565 57036 145 145 0 66420 0 [pid=5966] vsize: 266260 Current children cumulated CPU time (s) 1068.29 Current children cumulated vsize (Kb) 268384 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 77674 0 0 0 107574 252 0 0 25 0 1 0 1854999338 273702912 57398 4294967295 134512640 135094434 3221224432 3221221632 134600254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 66822 57398 145 145 0 66677 0 [pid=5966] vsize: 267288 Current children cumulated CPU time (s) 1078.27 Current children cumulated vsize (Kb) 269412 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 78181 0 0 0 108572 254 0 0 25 0 1 0 1854999338 274681856 57821 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 67061 57821 145 145 0 66916 0 [pid=5966] vsize: 268244 Current children cumulated CPU time (s) 1088.27 Current children cumulated vsize (Kb) 270368 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 78553 0 0 0 109570 255 0 0 25 0 1 0 1854999338 275316736 58078 4294967295 134512640 135094434 3221224432 3221222512 134600002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 67216 58078 145 145 0 67071 0 [pid=5966] vsize: 268864 Current children cumulated CPU time (s) 1098.26 Current children cumulated vsize (Kb) 270988 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 78950 0 0 0 110567 257 0 0 25 0 1 0 1854999338 276303872 58475 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 67457 58475 145 145 0 67312 0 [pid=5966] vsize: 269828 Current children cumulated CPU time (s) 1108.25 Current children cumulated vsize (Kb) 271952 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 79296 0 0 0 111566 258 0 0 25 0 1 0 1854999338 277004288 58725 4294967295 134512640 135094434 3221224432 3221222160 134676532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 67628 58725 145 145 0 67483 0 [pid=5966] vsize: 270512 Current children cumulated CPU time (s) 1118.25 Current children cumulated vsize (Kb) 272636 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 100640 0 0 0 112515 308 0 0 25 0 1 0 1854999338 320679936 69484 4294967295 134512640 135094434 3221224432 3221220400 134677278 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 78291 69484 145 145 0 78146 0 [pid=5966] vsize: 313164 Current children cumulated CPU time (s) 1128.24 Current children cumulated vsize (Kb) 315288 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 101221 0 0 0 113512 311 0 0 25 0 1 0 1854999338 321896448 69901 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 78588 69901 145 145 0 78443 0 [pid=5966] vsize: 314352 Current children cumulated CPU time (s) 1138.24 Current children cumulated vsize (Kb) 316476 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 101631 0 0 0 114510 312 0 0 25 0 1 0 1854999338 322727936 70269 4294967295 134512640 135094434 3221224432 3221220224 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 78791 70269 145 145 0 78646 0 [pid=5966] vsize: 315164 Current children cumulated CPU time (s) 1148.23 Current children cumulated vsize (Kb) 317288 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 102063 0 0 0 115507 313 0 0 25 0 1 0 1854999338 323706880 70619 4294967295 134512640 135094434 3221224432 3221221356 134676331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 79030 70619 145 145 0 78885 0 [pid=5966] vsize: 316120 Current children cumulated CPU time (s) 1158.21 Current children cumulated vsize (Kb) 318244 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 102257 0 0 0 116507 314 0 0 25 0 1 0 1854999338 323956736 70742 4294967295 134512640 135094434 3221224432 3221221260 134676240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 79091 70742 145 145 0 78946 0 [pid=5966] vsize: 316364 Current children cumulated CPU time (s) 1168.22 Current children cumulated vsize (Kb) 318488 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 102624 0 0 0 117504 316 0 0 25 0 1 0 1854999338 324501504 70962 4294967295 134512640 135094434 3221224432 3221222608 134676301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 79224 70962 145 145 0 79079 0 [pid=5966] vsize: 316896 Current children cumulated CPU time (s) 1178.21 Current children cumulated vsize (Kb) 319020 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 102985 0 0 0 118502 317 0 0 25 0 1 0 1854999338 325251072 71258 4294967295 134512640 135094434 3221224432 3221221328 134677233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 79407 71258 145 145 0 79262 0 [pid=5966] vsize: 317628 Current children cumulated CPU time (s) 1188.2 Current children cumulated vsize (Kb) 319752 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 103363 0 0 0 119499 319 0 0 25 0 1 0 1854999338 326057984 71558 4294967295 134512640 135094434 3221224432 3221221376 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 79604 71558 145 145 0 79459 0 [pid=5966] vsize: 318416 Current children cumulated CPU time (s) 1198.19 Current children cumulated vsize (Kb) 320540 [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 103950 0 0 0 120495 320 0 0 25 0 1 0 1854999338 327405568 72061 4294967295 134512640 135094434 3221224432 3221220672 134677007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 79933 72061 145 145 0 79788 0 [pid=5966] vsize: 319732 Current children cumulated CPU time (s) 1208.16 Current children cumulated vsize (Kb) 321856 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5966 Raw data (/proc/5962/stat): 5962 (minisat+_script) S 5961 5962 20728 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854999333 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5962/statm): 531 226 485 147 0 384 0 [pid=5962] vsize: 2124 Raw data (/proc/5966/stat): 5966 (minisat+_64-bit) R 5962 5962 20728 0 -1 0 103950 0 0 0 120495 320 0 0 25 0 1 0 1854999338 327405568 72061 4294967295 134512640 135094434 3221224432 3221220652 134676331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5966/statm): 79933 72061 145 145 0 79788 0 [pid=5966] vsize: 319732 Current children cumulated CPU time (s) 1208.16 Current children cumulated vsize (Kb) 321856 Sending SIGTERM to -5962 Sleeping 2 seconds One traced child (pid=5962) ended because it received signal 15 (SIGTERM) One traced child (pid=5966) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.21 CPU time (s): 1208.31 CPU user time (s): 1204.96 CPU system time (s): 3.34549 CPU usage (%): 99.8423 Max. virtual memory (cumulated for all children) (Kb): 321856
ERROR: no interpretation found !