Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-sp98ar.opb
MD5SUM9565d6b3010c78b37c39352cc9731cb7
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 7346652384
Optimality of the best value was proved NO
Number of terms in the objective function 15085
Biggest coefficient in the objective function 504328818
Number of bits for the biggest coefficient in the objective function 29
Sum of the numbers in the objective function 2067304124713
Number of bits of the sum of numbers in the objective function 41
Biggest number in a constraint 504328818
Number of bits of the biggest number in a constraint 29
Biggest sum of numbers in a constraint 2067304124713
Number of bits of the biggest sum of numbers41
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1206.67
Number of variables15085
Total number of constraints16520
Number of constraints which are clauses181
Number of constraints which are cardinality constraints (but not clauses)15927
Number of constraints which are nor clauses,nor cardinality constraints412
Minimum length of a constraint1
Maximum length of a constraint4222

Trace number 5947

Launcher Data

LAUNCH ON wulflinc26 THE 2005-09-20 02:14:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3116 boxname=wulflinc26 idbench=772 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9565d6b3010c78b37c39352cc9731cb7  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-sp98ar.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-sp98ar.opb
IDLAUNCH: 3116
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890360 kB
Buffers:         13540 kB
Cached:         101804 kB
SwapCached:        868 kB
Active:          44692 kB
Inactive:        73336 kB
HighTotal:      131008 kB
HighFree:        26768 kB
LowTotal:       903652 kB
LowFree:        863592 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5704 kB
Slab:            20420 kB
Committed_AS:    64152 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:34:10 (client local time) WITH STATUS 0 IN 1207.85 SECONDS
stats: 3116 7 1207.85 0

Solver Data

c Parsing PB file...
c Converting 1430 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===
c   -- Clauses(.)/Splits(s): sssssss.sss..ss...s.....s...s.....ss.s..s...s.s..s.s.....s.s..sssss.......s....s........ss...s..sssssssss.ssssssss.sss..sss.ss..s.sssssss.ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssssssssssssssss.sssssssssssssssssssssssssss.sss.sssss..s.s...sssss..s.s..s..sssss.ss.ss...s..s.....s..ss.ssssss.s.ssssssss.s..sss.sssss.s.s..sssss.s.sss..sss.s.ssssssssssss..ssss........ss..s.s.sssssssssssssss.ssss.sssssssssssssssss.s.s.sss..s..ss.s.ssss.ssssssssssssssssss.ssssssssssssssssssssss.ss..ss.s.ssssssss.....sss..ss.......s.......ssss.....ssssss..ss
c ---[1816]---> BDD-cost:   19
c ---[1815]---> BDD-cost:    5
c ---[1814]---> BDD-cost:    3
c ---[1813]---> BDD-cost:    7
c ---[1812]---> BDD-cost:    5
c ---[1811]---> BDD-cost:   47
c ---[1810]---> BDD-cost:   45
c ---[1809]---> BDD-cost:   17
c ---[1808]---> BDD-cost:   17
c ---[1807]---> BDD-cost:   17
c ---[1805]---> BDD-cost:    3
c ---[1804]---> BDD-cost:   17
c ---[1803]---> BDD-cost:   47
c ---[1802]---> BDD-cost:   45
c ---[1801]---> BDD-cost:   45
c ---[1800]---> BDD-cost:   17
c ---[1799]---> BDD-cost:   17
c ---[1798]---> BDD-cost:   17
c ---[1797]---> BDD-cost:   17
c ---[1796]---> BDD-cost:   17
c ---[1794]---> BDD-cost:   17
c ---[1793]---> BDD-cost:   17
c ---[1792]---> BDD-cost:   45
c ---[1791]---> BDD-cost:   45
c ---[1790]---> BDD-cost:    3
c ---[1789]---> BDD-cost:   19
c ---[1788]---> BDD-cost:   19
c ---[1787]---> BDD-cost:   59
c ---[1786]---> BDD-cost:   59
c ---[1785]---> BDD-cost:   19
c ---[1783]---> BDD-cost:    7
c ---[1782]---> BDD-cost:   59
c ---[1781]---> BDD-cost:   59
c ---[1780]---> BDD-cost:   59
c ---[1779]---> BDD-cost:   59
c ---[1778]---> BDD-cost:   59
c ---[1777]---> BDD-cost:   59
c ---[1776]---> BDD-cost:    9
c ---[1775]---> BDD-cost:    9
c ---[1774]---> BDD-cost:    3
c ---[1772]---> BDD-cost:    3
c ---[1770]---> BDD-cost:    3
c ---[1769]---> BDD-cost:   19
c ---[1768]---> BDD-cost:   19
c ---[1767]---> BDD-cost:   11
c ---[1766]---> BDD-cost:   11
c ---[1765]---> BDD-cost:   19
c ---[1763]---> BDD-cost:   19
c ---[1762]---> BDD-cost:   11
c ---[1761]---> BDD-cost:    5
c ---[1760]---> BDD-cost:   11
c ---[1759]---> BDD-cost:   19
c ---[1758]---> BDD-cost:    5
c ---[1757]---> BDD-cost:   11
c ---[1756]---> BDD-cost:    5
c ---[1755]---> BDD-cost:   23
c ---[1754]---> BDD-cost:   17
c ---[1752]---> BDD-cost:   39
c ---[1751]---> BDD-cost:   53
c ---[1750]---> BDD-cost:   53
c ---[1749]---> BDD-cost:   59
c ---[1748]---> BDD-cost:   47
c ---[1747]---> BDD-cost:   41
c ---[1746]---> BDD-cost:   47
c ---[1745]---> BDD-cost:   39
c ---[1744]---> BDD-cost:   53
c ---[1743]---> BDD-cost:   25
c ---[1741]---> BDD-cost:   39
c ---[1740]---> BDD-cost:   43
c ---[1739]---> BDD-cost:   41
c ---[1738]---> BDD-cost:   47
c ---[1737]---> BDD-cost:   29
c ---[1736]---> BDD-cost:   39
c ---[1735]---> BDD-cost:   53
c ---[1734]---> BDD-cost:   53
c ---[1733]---> BDD-cost:   59
c ---[1732]---> BDD-cost:   39
c ---[1731]---> Adder-cost: 928   maxlim: 9   bits: 5/4
c ---[1730]---> BDD-cost:   37
c ---[1729]---> BDD-cost:   39
c ---[1728]---> BDD-cost:   43
c ---[1727]---> BDD-cost:   53
c ---[1726]---> BDD-cost:   29
c ---[1725]---> BDD-cost:   21
c ---[1724]---> BDD-cost:   43
c ---[1723]---> BDD-cost:   41
c ---[1722]---> BDD-cost:   49
c ---[1721]---> BDD-cost:   43
c ---[1720]---> Adder-cost: 1283   maxlim: 26   bits: 6/5
c ---[1719]---> BDD-cost:   47
c ---[1718]---> BDD-cost:   53
c ---[1717]---> BDD-cost:   53
c ---[1716]---> BDD-cost:   59
c ---[1715]---> BDD-cost:   59
c ---[1712]---> BDD-cost:    7
c ---[1711]---> BDD-cost:    7
c ---[1710]---> BDD-cost:   29
c ---[1707]---> BDD-cost:   47
c ---[1706]---> BDD-cost:   39
c ---[1704]---> BDD-cost:    7
c ---[1703]---> BDD-cost:   47
c ---[1702]---> BDD-cost:   19
c ---[1699]---> BDD-cost:   13
c ---[1698]---> BDD-cost:   13
c ---[1693]---> BDD-cost:    3
c ---[1692]---> BDD-cost:    3
c ---[1691]---> BDD-cost:   11
c ---[1689]---> BDD-cost:    9
c ---[1688]---> BDD-cost:   11
c ---[1685]---> BDD-cost:    9
c ---[1684]---> BDD-cost:    9
c ---[1681]---> BDD-cost:    9
c ---[1679]---> BDD-cost:    9
c ---[1678]---> BDD-cost:    9
c ---[1677]---> BDD-cost:   53
c ---[1676]---> BDD-cost:   53
c ---[1674]---> BDD-cost:   43
c ---[1671]---> BDD-cost:    7
c ---[1670]---> BDD-cost:    7
c ---[1669]---> BDD-cost:   27
c ---[1668]---> BDD-cost:   39
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:   19
c ---[1665]---> BDD-cost:   53
c ---[1663]---> BDD-cost:   53
c ---[1662]---> BDD-cost:   43
c ---[1661]---> BDD-cost:   53
c ---[1658]---> BDD-cost:    7
c ---[1657]---> BDD-cost:    7
c ---[1656]---> BDD-cost:   29
c ---[1655]---> BDD-cost:   41
c ---[1654]---> BDD-cost:   19
c ---[1652]---> BDD-cost:   27
c ---[1651]---> BDD-cost:   51
c ---[1650]---> BDD-cost:   49
c ---[1649]---> BDD-cost:   35
c ---[1648]---> BDD-cost:   53
c ---[1647]---> BDD-cost:   53
c ---[1646]---> BDD-cost:   49
c ---[1645]---> BDD-cost:   37
c ---[1644]---> BDD-cost:   53
c ---[1643]---> BDD-cost:   51
c ---[1641]---> BDD-cost:   49
c ---[1640]---> BDD-cost:   49
c ---[1639]---> BDD-cost:   37
c ---[1638]---> BDD-cost:   37
c ---[1637]---> BDD-cost:   49
c ---[1636]---> BDD-cost:   49
c ---[1635]---> BDD-cost:   49
c ---[1634]---> BDD-cost:   53
c ---[1633]---> BDD-cost:   53
c ---[1632]---> BDD-cost:   35
c ---[1630]---> BDD-cost:   53
c ---[1629]---> BDD-cost:   37
c ---[1628]---> BDD-cost:   49
c ---[1627]---> BDD-cost:   49
c ---[1626]---> BDD-cost:   49
c ---[1625]---> BDD-cost:   49
c ---[1624]---> BDD-cost:   37
c ---[1623]---> BDD-cost:   33
c ---[1622]---> BDD-cost:   49
c ---[1621]---> BDD-cost:   53
c ---[1619]---> BDD-cost:   53
c ---[1618]---> BDD-cost:   29
c ---[1617]---> BDD-cost:    5
c ---[1616]---> BDD-cost:   35
c ---[1615]---> BDD-cost:   53
c ---[1614]---> BDD-cost:   43
c ---[1613]---> BDD-cost:   53
c ---[1612]---> BDD-cost:   53
c ---[1611]---> BDD-cost:   53
c ---[1610]---> BDD-cost:   53
c ---[1608]---> BDD-cost:   17
c ---[1607]---> BDD-cost:   19
c ---[1606]---> BDD-cost:   19
c ---[1605]---> BDD-cost:   11
c ---[1604]---> BDD-cost:   11
c ---[1603]---> BDD-cost:   19
c ---[1602]---> BDD-cost:   19
c ---[1601]---> BDD-cost:   11
c ---[1599]---> BDD-cost:   11
c ---[1596]---> BDD-cost:   19
c ---[1594]---> BDD-cost:   11
c ---[1592]---> BDD-cost:    3
c ---[1591]---> BDD-cost:    3
c ---[1590]---> BDD-cost:   43
c ---[1589]---> BDD-cost:    9
c ---[1588]---> BDD-cost:   41
c ---[1587]---> BDD-cost:   53
c ---[1584]---> BDD-cost:   43
c ---[1583]---> BDD-cost:   35
c ---[1582]---> BDD-cost:   43
c ---[1581]---> BDD-cost:   53
c ---[1580]---> BDD-cost:   43
c ---[1579]---> BDD-cost:   47
c ---[1578]---> BDD-cost:   41
c ---[1577]---> BDD-cost:    5
c ---[1576]---> BDD-cost:   39
c ---[1574]---> BDD-cost:   53
c ---[1573]---> BDD-cost:   43
c ---[1572]---> BDD-cost:   35
c ---[1571]---> BDD-cost:   41
c ---[1569]---> BDD-cost:   13
c ---[1567]---> BDD-cost:   13
c ---[1566]---> BDD-cost:   53
c ---[1565]---> BDD-cost:   53
c ---[1563]---> BDD-cost:   53
c ---[1562]---> BDD-cost:   53
c ---[1561]---> BDD-cost:   53
c ---[1560]---> BDD-cost:   53
c ---[1559]---> BDD-cost:   53
c ---[1558]---> BDD-cost:   53
c ---[1557]---> BDD-cost:   53
c ---[1556]---> BDD-cost:   53
c ---[1555]---> BDD-cost:   53
c ---[1554]---> BDD-cost:   53
c ---[1552]---> BDD-cost:    5
c ---[1551]---> BDD-cost:   53
c ---[1550]---> BDD-cost:   53
c ---[1549]---> BDD-cost:   53
c ---[1548]---> BDD-cost:    3
c ---[1547]---> BDD-cost:   17
c ---[1546]---> BDD-cost:   17
c ---[1545]---> BDD-cost:   17
c ---[1544]---> BDD-cost:   45
c ---[1543]---> BDD-cost:   59
c ---[1541]---> BDD-cost:   59
c ---[1540]---> BDD-cost:   59
c ---[1539]---> BDD-cost:   59
c ---[1538]---> BDD-cost:   59
c ---[1537]---> BDD-cost:   59
c ---[1536]---> BDD-cost:   59
c ---[1535]---> BDD-cost:   59
c ---[1534]---> BDD-cost:   59
c ---[1533]---> BDD-cost:   59
c ---[1532]---> BDD-cost:   59
c ---[1530]---> BDD-cost:   59
c ---[1529]---> BDD-cost:   59
c ---[1527]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    3
c ---[1524]---> BDD-cost:    5
c ---[1519]---> BDD-cost:   47
c ---[1518]---> BDD-cost:   39
c ---[1517]---> BDD-cost:   41
c ---[1516]---> BDD-cost:   43
c ---[1515]---> BDD-cost:   47
c ---[1514]---> BDD-cost:    5
c ---[1513]---> BDD-cost:    7
c ---[1512]---> BDD-cost:   47
c ---[1511]---> BDD-cost:    9
c ---[1509]---> BDD-cost:    7
c ---[1508]---> BDD-cost:   29
c ---[1507]---> BDD-cost:   47
c ---[1504]---> BDD-cost:   37
c ---[1503]---> BDD-cost:   59
c ---[1502]---> BDD-cost:   43
c ---[1501]---> BDD-cost:   47
c ---[1500]---> BDD-cost:    7
c ---[1498]---> BDD-cost:   39
c ---[1497]---> BDD-cost:   17
c ---[1496]---> BDD-cost:   19
c ---[1495]---> BDD-cost:   19
c ---[1494]---> BDD-cost:   49
c ---[1493]---> BDD-cost:   19
c ---[1492]---> BDD-cost:   19
c ---[1491]---> BDD-cost:   53
c ---[1490]---> BDD-cost:   47
c ---[1489]---> BDD-cost:   41
c ---[1486]---> BDD-cost:   39
c ---[1485]---> BDD-cost:   43
c ---[1484]---> BDD-cost:   43
c ---[1483]---> BDD-cost:   11
c ---[1482]---> BDD-cost:   43
c ---[1481]---> BDD-cost:    3
c ---[1480]---> BDD-cost:   11
c ---[1479]---> BDD-cost:    5
c ---[1478]---> BDD-cost:    3
c ---[1477]---> BDD-cost:    7
c ---[1475]---> BDD-cost:   35
c ---[1474]---> BDD-cost:   37
c ---[1473]---> BDD-cost:   39
c ---[1472]---> BDD-cost:   53
c ---[1471]---> BDD-cost:   51
c ---[1470]---> BDD-cost:   25
c ---[1469]---> BDD-cost:   35
c ---[1468]---> BDD-cost:   59
c ---[1467]---> BDD-cost:   53
c ---[1466]---> BDD-cost:    9
c ---[1464]---> BDD-cost:   11
c ---[1462]---> BDD-cost:    9
c ---[1458]---> BDD-cost:    9
c ---[1457]---> BDD-cost:   33
c ---[1456]---> BDD-cost:   39
c ---[1455]---> BDD-cost:   37
c ---[1453]---> BDD-cost:   43
c ---[1451]---> BDD-cost:   43
c ---[1450]---> BDD-cost:   39
c ---[1449]---> BDD-cost:   41
c ---[1448]---> BDD-cost:    5
c ---[1447]---> BDD-cost:    3
c ---[1445]---> BDD-cost:    5
c ---[1444]---> BDD-cost:    7
c ---[1442]---> BDD-cost:   31
c ---[1441]---> BDD-cost:   19
c ---[1440]---> BDD-cost:    7
c ---[1438]---> BDD-cost:   41
c ---[1436]---> BDD-cost:    7
c ---[1433]---> BDD-cost:   33
c ---[1431]---> BDD-cost:   39
c ---[1429]---> BDD-cost:   37
c ---[1428]---> BDD-cost:   39
c ---[1427]---> BDD-cost:   17
c ---[1426]---> BDD-cost:   19
c ---[1425]---> BDD-cost:   19
c ---[1424]---> BDD-cost:   19
c ---[1423]---> BDD-cost:   19
c ---[1422]---> BDD-cost:   33
c ---[1420]---> BDD-cost:   39
c ---[1418]---> BDD-cost:   19
c ---[1417]---> BDD-cost:   19
c ---[1416]---> BDD-cost:   19
c ---[1415]---> BDD-cost:   43
c ---[1414]---> BDD-cost:   43
c ---[1413]---> BDD-cost:    3
c ---[1412]---> BDD-cost:   11
c ---[1411]---> BDD-cost:   35
c ---[1408]---> BDD-cost:   11
c ---[1406]---> BDD-cost:   43
c ---[1404]---> BDD-cost:   11
c ---[1403]---> BDD-cost:   41
c ---[1402]---> BDD-cost:   33
c ---[1401]---> BDD-cost:   19
c ---[1399]---> BDD-cost:   27
c ---[1398]---> BDD-cost:    5
c ---[1397]---> BDD-cost:   53
c ---[1396]---> BDD-cost:    7
c ---[1395]---> BDD-cost:   43
c ---[1394]---> BDD-cost:   39
c ---[1393]---> BDD-cost:   43
c ---[1392]---> BDD-cost:    3
c ---[1391]---> BDD-cost:   43
c ---[1390]---> BDD-cost:   25
c ---[1388]---> BDD-cost:   53
c ---[1387]---> BDD-cost:   29
c ---[1386]---> BDD-cost:   47
c ---[1385]---> BDD-cost:   41
c ---[1384]---> BDD-cost:   59
c ---[1383]---> BDD-cost:   33
c ---[1382]---> BDD-cost:   31
c ---[1381]---> BDD-cost:   41
c ---[1380]---> BDD-cost:   53
c ---[1379]---> BDD-cost:   49
c ---[1376]---> BDD-cost:   39
c ---[1375]---> BDD-cost:   43
c ---[1374]---> BDD-cost:    5
c ---[1373]---> BDD-cost:   13
c ---[1371]---> BDD-cost:   39
c ---[1369]---> BDD-cost:   19
c ---[1368]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   47
c ---[1365]---> BDD-cost:   19
c ---[1364]---> BDD-cost:   59
c ---[1363]---> BDD-cost:   59
c ---[1362]---> BDD-cost:   41
c ---[1361]---> BDD-cost:   19
c ---[1360]---> BDD-cost:   45
c ---[1359]---> BDD-cost:   43
c ---[1358]---> BDD-cost:   37
c ---[1357]---> BDD-cost:   43
c ---[1356]---> BDD-cost:   49
c ---[1355]---> Adder-cost: 515   maxlim: 9   bits: 5/4
c ---[1354]---> BDD-cost:   37
c ---[1353]---> BDD-cost:   43
c ---[1352]---> BDD-cost:   53
c ---[1351]---> BDD-cost:   53
c ---[1350]---> BDD-cost:    5
c ---[1348]---> BDD-cost:   19
c ---[1347]---> BDD-cost:   19
c ---[1346]---> BDD-cost:   43
c ---[1345]---> BDD-cost:   41
c ---[1344]---> Adder-cost: 761   maxlim: 19   bits: 6/5
c ---[1343]---> BDD-cost:   19
c ---[1342]---> BDD-cost:   13
c ---[1341]---> BDD-cost:   19
c ---[1339]---> BDD-cost:    3
c ---[1338]---> BDD-cost:   11
c ---[1333]---> BDD-cost:  771
c ---[1302]---> Adder-cost: 3666   maxlim: 9   bits: 5/4
c ---[1301]---> Adder-cost: 5783   maxlim: 27   bits: 6/5
c ---[1300]---> Adder-cost: 2769   maxlim: 7   bits: 4/3
c ---[1296]---> Adder-cost: 5328   maxlim: 9   bits: 5/4
c ---[1275]---> BDD-cost:18365
c ---[1253]---> Adder-cost: 7051   maxlim: 7   bits: 4/3
c ---[1242]---> Adder-cost: 10495   maxlim: 29   bits: 6/5
c ---[1214]---> Adder-cost: 3777   maxlim: 17   bits: 6/5
c ---[1189]---> BDD-cost:   27
c ---[1184]---> BDD-cost:   27
c ---[1176]---> BDD-cost: 8536
c ---[1164]---> Adder-cost: 5657   maxlim: 29   bits: 6/5
c ---[1054]---> BDD-cost: 6713
c ---[1043]---> BDD-cost:  823
c ---[ 916]---> BDD-cost:   37
c ---[ 915]---> BDD-cost:   27
c ---[ 914]---> BDD-cost:   43
c ---[ 913]---> BDD-cost:   47
c ---[ 912]---> BDD-cost:   43
c ---[ 911]---> BDD-cost:   49
c ---[ 910]---> BDD-cost:   39
c ---[ 908]---> BDD-cost:   49
c ---[ 907]---> BDD-cost:   59
c ---[ 906]---> BDD-cost:   47
c ---[ 905]---> BDD-cost:   37
c ---[ 904]---> BDD-cost:   47
c ---[ 903]---> BDD-cost:   43
c ---[ 902]---> BDD-cost:   31
c ---[ 901]---> BDD-cost:   29
c ---[ 900]---> BDD-cost:   23
c ---[ 899]---> BDD-cost:    5
c ---[ 897]---> BDD-cost:   25
c ---[ 896]---> BDD-cost:   19
c ---[ 895]---> BDD-cost:   19
c ---[ 894]---> BDD-cost:   37
c ---[ 893]---> BDD-cost:   43
c ---[ 892]---> BDD-cost:    3
c ---[ 891]---> BDD-cost:    5
c ---[ 890]---> BDD-cost:    3
c ---[ 889]---> BDD-cost:   15
c ---[ 888]---> BDD-cost:   15
c ---[ 886]---> BDD-cost:    3
c ---[ 885]---> BDD-cost:    9
c ---[ 884]---> BDD-cost:   21
c ---[ 883]---> BDD-cost:   17
c ---[ 882]---> BDD-cost:   17
c ---[ 881]---> BDD-cost:   19
c ---[ 880]---> BDD-cost:   19
c ---[ 879]---> BDD-cost:    3
c ---[ 878]---> BDD-cost:   17
c ---[ 877]---> BDD-cost:   17
c ---[ 875]---> BDD-cost:   19
c ---[ 874]---> BDD-cost:   41
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:    3
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    3
c ---[ 869]---> BDD-cost:   49
c ---[ 868]---> BDD-cost:   49
c ---[ 867]---> BDD-cost:   19
c ---[ 866]---> BDD-cost:   53
c ---[ 865]---> BDD-cost:12879
c ---[ 864]---> BDD-cost:   17
c ---[ 863]---> BDD-cost:   17
c ---[ 862]---> BDD-cost:    9
c ---[ 861]---> BDD-cost:    3
c ---[ 860]---> BDD-cost:   27
c ---[ 859]---> BDD-cost:   37
c ---[ 858]---> BDD-cost:   33
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:    3
c ---[ 855]---> BDD-cost:   25
c ---[ 853]---> BDD-cost:   19
c ---[ 852]---> BDD-cost:    5
c ---[ 851]---> BDD-cost:    3
c ---[ 850]---> BDD-cost:   41
c ---[ 849]---> BDD-cost:    3
c ---[ 848]---> BDD-cost:    3
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:   33
c ---[ 845]---> BDD-cost:   41
c ---[ 844]---> BDD-cost:    3
c ---[ 842]---> BDD-cost:   37
c ---[ 841]---> BDD-cost:   17
c ---[ 840]---> BDD-cost:   19
c ---[ 839]---> BDD-cost:   19
c ---[ 838]---> BDD-cost:   25
c ---[ 837]---> BDD-cost:   19
c ---[ 836]---> BDD-cost:   33
c ---[ 835]---> BDD-cost:   19
c ---[ 834]---> BDD-cost:   19
c ---[ 833]---> BDD-cost:   43
c ---[ 830]---> BDD-cost:   19
c ---[ 829]---> BDD-cost:   19
c ---[ 828]---> BDD-cost:   19
c ---[ 827]---> BDD-cost:    5
c ---[ 826]---> BDD-cost:   49
c ---[ 825]---> BDD-cost:    5
c ---[ 824]---> BDD-cost:   53
c ---[ 823]---> BDD-cost:   19
c ---[ 822]---> BDD-cost:   19
c ---[ 821]---> BDD-cost:   19
c ---[ 819]---> BDD-cost:   41
c ---[ 818]---> BDD-cost:   37
c ---[ 817]---> BDD-cost:   43
c ---[ 816]---> BDD-cost:   19
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:    5
c ---[ 813]---> BDD-cost:   35
c ---[ 812]---> BDD-cost:    3
c ---[ 811]---> BDD-cost:   59
c ---[ 810]---> BDD-cost:   41
c ---[ 808]---> BDD-cost:   59
c ---[ 807]---> BDD-cost:   53
c ---[ 806]---> BDD-cost:   59
c ---[ 805]---> BDD-cost:   35
c ---[ 804]---> BDD-cost:   37
c ---[ 803]---> BDD-cost:   35
c ---[ 802]---> BDD-cost:   51
c ---[ 801]---> BDD-cost:   59
c ---[ 800]---> BDD-cost:   59
c ---[ 799]---> BDD-cost:   35
c ---[ 797]---> BDD-cost:   11
c ---[ 796]---> BDD-cost:   53
c ---[ 795]---> BDD-cost:   35
c ---[ 794]---> BDD-cost:   59
c ---[ 793]---> BDD-cost:   53
c ---[ 792]---> BDD-cost:   53
c ---[ 791]---> BDD-cost:   35
c ---[ 790]---> BDD-cost:   59
c ---[ 789]---> BDD-cost:   19
c ---[ 788]---> BDD-cost:   43
c ---[ 786]---> BDD-cost:   43
c ---[ 785]---> BDD-cost:   23
c ---[ 784]---> BDD-cost:    7
c ---[ 782]---> BDD-cost:   47
c ---[ 781]---> BDD-cost:   59
c ---[ 780]---> BDD-cost:    7
c ---[ 779]---> BDD-cost:   45
c ---[ 778]---> BDD-cost:   47
c ---[ 777]---> BDD-cost:   17
c ---[ 775]---> BDD-cost:   47
c ---[ 774]---> BDD-cost:   19
c ---[ 772]---> BDD-cost:   47
c ---[ 771]---> BDD-cost:   43
c ---[ 770]---> BDD-cost:   43
c ---[ 769]---> BDD-cost:   45
c ---[ 768]---> BDD-cost:   47
c ---[ 767]---> BDD-cost:   45
c ---[ 766]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   49
c ---[ 763]---> BDD-cost:   49
c ---[ 762]---> BDD-cost:   43
c ---[ 761]---> BDD-cost:   35
c ---[ 760]---> BDD-cost:   23
c ---[ 759]---> BDD-cost:   43
c ---[ 758]---> BDD-cost:   43
c ---[ 757]---> BDD-cost:   53
c ---[ 756]---> BDD-cost:   47
c ---[ 755]---> BDD-cost:   59
c ---[ 753]---> BDD-cost:   59
c ---[ 752]---> BDD-cost:   23
c ---[ 751]---> BDD-cost:   47
c ---[ 750]---> BDD-cost:   41
c ---[ 749]---> BDD-cost:   23
c ---[ 748]---> BDD-cost:   43
c ---[ 747]---> BDD-cost:   23
c ---[ 746]---> BDD-cost:   43
c ---[ 745]---> BDD-cost:    7
c ---[ 744]---> BDD-cost:    7
c ---[ 742]---> BDD-cost:   19
c ---[ 741]---> BDD-cost:   23
c ---[ 740]---> BDD-cost:    5
c ---[ 739]---> BDD-cost:   43
c ---[ 738]---> BDD-cost:   49
c ---[ 737]---> BDD-cost:   47
c ---[ 736]---> BDD-cost:   45
c ---[ 735]---> BDD-cost:   43
c ---[ 734]---> BDD-cost:   47
c ---[ 733]---> BDD-cost:   43
c ---[ 731]---> BDD-cost:   59
c ---[ 730]---> BDD-cost:   43
c ---[ 729]---> BDD-cost:   43
c ---[ 728]---> BDD-cost:   47
c ---[ 727]---> BDD-cost:   23
c ---[ 726]---> BDD-cost:   19
c ---[ 725]---> BDD-cost:   49
c ---[ 724]---> BDD-cost:   19
c ---[ 723]---> BDD-cost:   53
c ---[ 722]---> BDD-cost:   43
c ---[ 719]---> BDD-cost:   45
c ---[ 718]---> BDD-cost:   47
c ---[ 717]---> BDD-cost:   47
c ---[ 716]---> BDD-cost:   49
c ---[ 715]---> BDD-cost:   43
c ---[ 714]---> BDD-cost:   29
c ---[ 713]---> BDD-cost:   43
c ---[ 712]---> BDD-cost:   53
c ---[ 711]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:   47
c ---[ 708]---> BDD-cost:   31
c ---[ 707]---> BDD-cost:   43
c ---[ 706]---> BDD-cost:   39
c ---[ 705]---> BDD-cost:   17
c ---[ 704]---> BDD-cost:   35
c ---[ 703]---> BDD-cost:    7
c ---[ 702]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:   19
c ---[ 700]---> BDD-cost:    5
c ---[ 699]---> BDD-cost:   19
c ---[ 697]---> BDD-cost:    7
c ---[ 696]---> BDD-cost:    5
c ---[ 695]---> BDD-cost:    7
c ---[ 694]---> BDD-cost:   57
c ---[ 693]---> BDD-cost:   11
c ---[ 692]---> BDD-cost:   59
c ---[ 691]---> BDD-cost:   59
c ---[ 690]---> BDD-cost:   59
c ---[ 689]---> BDD-cost:   59
c ---[ 688]---> BDD-cost:    5
c ---[ 685]---> BDD-cost:   19
c ---[ 684]---> BDD-cost:   19
c ---[ 683]---> BDD-cost:   37
c ---[ 681]---> BDD-cost:   11
c ---[ 679]---> BDD-cost:   43
c ---[ 678]---> BDD-cost:   39
c ---[ 677]---> BDD-cost:   43
c ---[ 675]---> BDD-cost:   45
c ---[ 674]---> BDD-cost:   59
c ---[ 673]---> BDD-cost:   37
c ---[ 672]---> BDD-cost:   17
c ---[ 671]---> BDD-cost:   39
c ---[ 670]---> BDD-cost:   53
c ---[ 669]---> BDD-cost:   53
c ---[ 668]---> BDD-cost:   59
c ---[ 667]---> BDD-cost:   39
c ---[ 666]---> BDD-cost:   37
c ---[ 664]---> BDD-cost:   39
c ---[ 663]---> BDD-cost:   39
c ---[ 662]---> BDD-cost:   43
c ---[ 661]---> BDD-cost:   25
c ---[ 660]---> BDD-cost:   31
c ---[ 659]---> BDD-cost:   25
c ---[ 658]---> BDD-cost:   43
c ---[ 657]---> BDD-cost:   41
c ---[ 656]---> BDD-cost:   43
c ---[ 655]---> BDD-cost:   43
c ---[ 653]---> BDD-cost:   47
c ---[ 652]---> BDD-cost:   47
c ---[ 651]---> BDD-cost:   57
c ---[ 650]---> BDD-cost:   49
c ---[ 649]---> BDD-cost:   45
c ---[ 648]---> BDD-cost:   43
c ---[ 647]---> BDD-cost:   43
c ---[ 646]---> BDD-cost:   47
c ---[ 645]---> BDD-cost:   59
c ---[ 644]---> BDD-cost:   43
c ---[ 642]---> BDD-cost:   43
c ---[ 641]---> BDD-cost:   47
c ---[ 640]---> BDD-cost:   47
c ---[ 639]---> BDD-cost:   47
c ---[ 638]---> BDD-cost:   47
c ---[ 637]---> BDD-cost:   47
c ---[ 636]---> BDD-cost:   47
c ---[ 635]---> BDD-cost:   43
c ---[ 634]---> BDD-cost:   43
c ---[ 633]---> BDD-cost:   53
c ---[ 631]---> BDD-cost:   59
c ---[ 630]---> BDD-cost:   59
c ---[ 629]---> BDD-cost:   47
c ---[ 628]---> BDD-cost:   47
c ---[ 627]---> BDD-cost:   41
c ---[ 626]---> BDD-cost:   43
c ---[ 625]---> BDD-cost:   41
c ---[ 624]---> BDD-cost:   43
c ---[ 623]---> BDD-cost:   43
c ---[ 622]---> BDD-cost:   47
c ---[ 620]---> BDD-cost:   43
c ---[ 619]---> BDD-cost:   47
c ---[ 618]---> BDD-cost:   43
c ---[ 617]---> BDD-cost:   43
c ---[ 616]---> BDD-cost:   43
c ---[ 615]---> BDD-cost:   49
c ---[ 614]---> BDD-cost:   47
c ---[ 613]---> BDD-cost:   45
c ---[ 612]---> BDD-cost:   47
c ---[ 611]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   43
c ---[ 607]---> BDD-cost:   43
c ---[ 606]---> BDD-cost:   55
c ---[ 605]---> BDD-cost:   43
c ---[ 604]---> BDD-cost:   43
c ---[ 603]---> BDD-cost:   49
c ---[ 602]---> BDD-cost:   43
c ---[ 601]---> BDD-cost:   49
c ---[ 599]---> BDD-cost:   19
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    3
c ---[ 595]---> BDD-cost:    9
c ---[ 594]---> BDD-cost:    5
c ---[ 593]---> BDD-cost:   53
c ---[ 592]---> BDD-cost:   43
c ---[ 591]---> BDD-cost:    7
c ---[ 589]---> BDD-cost:   27
c ---[ 588]---> BDD-cost:   43
c ---[ 586]---> BDD-cost:   39
c ---[ 584]---> BDD-cost:   17
c ---[ 583]---> BDD-cost:   17
c ---[ 582]---> BDD-cost:   19
c ---[ 581]---> BDD-cost:   19
c ---[ 579]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:    5
c ---[ 574]---> BDD-cost:   33
c ---[ 573]---> BDD-cost:   39
c ---[ 571]---> BDD-cost:   19
c ---[ 570]---> BDD-cost:   19
c ---[ 569]---> BDD-cost:   19
c ---[ 568]---> BDD-cost:   45
c ---[ 567]---> BDD-cost:   47
c ---[ 566]---> BDD-cost:   47
c ---[ 564]---> BDD-cost:   19
c ---[ 563]---> BDD-cost:   49
c ---[ 562]---> BDD-cost:   43
c ---[ 561]---> BDD-cost:   19
c ---[ 560]---> BDD-cost:   43
c ---[ 559]---> BDD-cost:   53
c ---[ 558]---> BDD-cost:   59
c ---[ 557]---> BDD-cost:   47
c ---[ 556]---> BDD-cost:    9
c ---[ 555]---> BDD-cost:    7
c ---[ 554]---> BDD-cost:14669
c ---[ 553]---> BDD-cost:   43
c ---[ 552]---> BDD-cost:   43
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:   19
c ---[ 549]---> BDD-cost:   19
c ---[ 548]---> BDD-cost:   25
c ---[ 547]---> BDD-cost:   19
c ---[ 544]---> BDD-cost:   13
c ---[ 543]---> BDD-cost:13317
c ---[ 542]---> BDD-cost:   13
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 537]---> BDD-cost:   19
c ---[ 536]---> BDD-cost:   45
c ---[ 535]---> BDD-cost:   47
c ---[ 534]---> BDD-cost:   47
c ---[ 533]---> BDD-cost:   49
c ---[ 531]---> BDD-cost:   43
c ---[ 530]---> BDD-cost:   43
c ---[ 529]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:   59
c ---[ 527]---> BDD-cost:   47
c ---[ 526]---> BDD-cost:   43
c ---[ 525]---> BDD-cost:   39
c ---[ 524]---> BDD-cost:   11
c ---[ 523]---> BDD-cost:   11
c ---[ 522]---> BDD-cost:   49
c ---[ 520]---> BDD-cost:   53
c ---[ 519]---> BDD-cost:    7
c ---[ 518]---> BDD-cost:    9
c ---[ 517]---> BDD-cost:   11
c ---[ 516]---> BDD-cost:   29
c ---[ 515]---> BDD-cost:   47
c ---[ 514]---> BDD-cost:   39
c ---[ 513]---> BDD-cost:   11
c ---[ 512]---> BDD-cost:   19
c ---[ 511]---> BDD-cost:   19
c ---[ 509]---> BDD-cost:    3
c ---[ 508]---> BDD-cost:   59
c ---[ 507]---> BDD-cost:   59
c ---[ 506]---> BDD-cost:   53
c ---[ 505]---> BDD-cost:   59
c ---[ 504]---> BDD-cost:   53
c ---[ 503]---> BDD-cost:   59
c ---[ 502]---> BDD-cost:   53
c ---[ 501]---> BDD-cost:    7
c ---[ 500]---> BDD-cost:   17
c ---[ 497]---> BDD-cost:   17
c ---[ 496]---> BDD-cost:   19
c ---[ 495]---> BDD-cost:   19
c ---[ 493]---> BDD-cost:    7
c ---[ 492]---> BDD-cost:    5
c ---[ 490]---> BDD-cost:   33
c ---[ 489]---> BDD-cost:   39
c ---[ 486]---> BDD-cost:   19
c ---[ 485]---> BDD-cost:   19
c ---[ 484]---> BDD-cost:   19
c ---[ 483]---> BDD-cost:   45
c ---[ 482]---> BDD-cost:   47
c ---[ 481]---> BDD-cost:   17
c ---[ 480]---> BDD-cost:   43
c ---[ 479]---> BDD-cost:   17
c ---[ 478]---> BDD-cost:   37
c ---[ 477]---> BDD-cost:   43
c ---[ 475]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:   53
c ---[ 471]---> BDD-cost:   53
c ---[ 470]---> BDD-cost:   53
c ---[ 469]---> BDD-cost:   43
c ---[ 468]---> BDD-cost:   43
c ---[ 467]---> BDD-cost:   53
c ---[ 466]---> BDD-cost:   17
c ---[ 464]---> BDD-cost:    7
c ---[ 463]---> BDD-cost:   43
c ---[ 462]---> BDD-cost:   47
c ---[ 461]---> BDD-cost:   53
c ---[ 460]---> BDD-cost:   41
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    7
c ---[ 455]---> BDD-cost:   43
c ---[ 453]---> BDD-cost:    3
c ---[ 452]---> BDD-cost:   21
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:   53
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:   43
c ---[ 447]---> BDD-cost:   39
c ---[ 446]---> BDD-cost:   39
c ---[ 445]---> BDD-cost:    5
c ---[ 444]---> BDD-cost:   43
c ---[ 442]---> BDD-cost:   19
c ---[ 441]---> BDD-cost:   47
c ---[ 440]---> BDD-cost:   59
c ---[ 439]---> BDD-cost:   49
c ---[ 438]---> BDD-cost:   43
c ---[ 437]---> BDD-cost:   43
c ---[ 436]---> BDD-cost:   53
c ---[ 435]---> BDD-cost:   59
c ---[ 434]---> BDD-cost:   47
c ---[ 433]---> BDD-cost:   21
c ---[ 431]---> BDD-cost:   45
c ---[ 430]---> BDD-cost:   47
c ---[ 429]---> BDD-cost:   43
c ---[ 428]---> BDD-cost:   35
c ---[ 427]---> BDD-cost:   33
c ---[ 426]---> BDD-cost:   23
c ---[ 425]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:   17
c ---[ 423]---> BDD-cost:   17
c ---[ 422]---> BDD-cost:   17
c ---[ 420]---> BDD-cost:   45
c ---[ 418]---> BDD-cost:   19
c ---[ 417]---> BDD-cost:   19
c ---[ 416]---> BDD-cost:   19
c ---[ 415]---> BDD-cost:   37
c ---[ 414]---> BDD-cost:   43
c ---[ 413]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:   11
c ---[ 409]---> BDD-cost:   11
c ---[ 408]---> BDD-cost:   11
c ---[ 407]---> BDD-cost:    5
c ---[ 406]---> BDD-cost:   19
c ---[ 405]---> BDD-cost:   17
c ---[ 404]---> BDD-cost:   19
c ---[ 403]---> BDD-cost:   49
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   41
c ---[ 399]---> BDD-cost:   53
c ---[ 398]---> BDD-cost:   59
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    7
c ---[ 395]---> BDD-cost:   41
c ---[ 394]---> BDD-cost:   33
c ---[ 393]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:   19
c ---[ 391]---> BDD-cost:   19
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost: 6553
c ---[ 388]---> BDD-cost:  914
c ---[ 387]---> BDD-cost:  710
c ---[ 386]---> BDD-cost:  122
c ---[ 385]---> BDD-cost:  716
c ---[ 384]---> BDD-cost:  232
c ---[ 383]---> BDD-cost:  147
c ---[ 382]---> BDD-cost:  127
c ---[ 381]---> BDD-cost:   14
c ---[ 380]---> BDD-cost:    1
c ---[ 379]---> BDD-cost: 4032
c ---[ 378]---> BDD-cost:  714
c ---[ 377]---> Adder-cost: 2947   maxlim: 19   bits: 6/5
c ---[ 376]---> BDD-cost: 1340
c ---[ 375]---> BDD-cost:   24
c ---[ 374]---> BDD-cost:  240
c ---[ 373]---> BDD-cost:   78
c ---[ 372]---> BDD-cost:   94
c ---[ 371]---> BDD-cost:  598
c ---[ 370]---> BDD-cost:  734
c ---[ 369]---> BDD-cost:   86
c ---[ 368]---> BDD-cost:   12
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:  126
c ---[ 365]---> BDD-cost:  358
c ---[ 364]---> BDD-cost: 1423
c ---[ 363]---> BDD-cost:   86
c ---[ 362]---> BDD-cost:  738
c ---[ 361]---> BDD-cost: 4656
c ---[ 360]---> BDD-cost:   23
c ---[ 359]---> BDD-cost:   18
c ---[ 358]---> BDD-cost:   12
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:  339
c ---[ 355]---> BDD-cost:   34
c ---[ 354]---> BDD-cost: 2048
c ---[ 353]---> BDD-cost: 1280
c ---[ 352]---> BDD-cost:  236
c ---[ 351]---> BDD-cost:   14
c ---[ 350]---> BDD-cost:   16
c ---[ 349]---> BDD-cost:  774
c ---[ 348]---> BDD-cost:    1
c ---[ 347]---> BDD-cost: 2988
c ---[ 346]---> BDD-cost:  374
c ---[ 345]---> BDD-cost: 3816
c ---[ 344]---> BDD-cost: 3452
c ---[ 343]---> BDD-cost: 1484
c ---[ 342]---> BDD-cost:   42
c ---[ 341]---> BDD-cost:   20
c ---[ 340]---> BDD-cost:  268
c ---[ 339]---> BDD-cost:   36
c ---[ 338]---> BDD-cost:   63
c ---[ 337]---> BDD-cost:   14
c ---[ 336]---> BDD-cost:  458
c ---[ 335]---> BDD-cost:  212
c ---[ 334]---> BDD-cost:   40
c ---[ 333]---> BDD-cost:   56
c ---[ 332]---> BDD-cost:    1
c ---[ 331]---> BDD-cost:   58
c ---[ 330]---> BDD-cost:   54
c ---[ 329]---> BDD-cost:   18
c ---[ 328]---> Adder-cost: 8674   maxlim: 27   bits: 6/5
c ---[ 327]---> BDD-cost:12445
c ---[ 326]---> BDD-cost:  194
c ---[ 325]---> BDD-cost:  104
c ---[ 324]---> BDD-cost:   14
c ---[ 323]---> BDD-cost:    4
c ---[ 322]---> BDD-cost:   82
c ---[ 321]---> BDD-cost:  214
c ---[ 320]---> BDD-cost: 6029
c ---[ 319]---> BDD-cost: 1476
c ---[ 318]---> BDD-cost: 1586
c ---[ 317]---> BDD-cost:  768
c ---[ 316]---> BDD-cost:  850
c ---[ 315]---> BDD-cost: 1317
c ---[ 314]---> BDD-cost:  402
c ---[ 313]---> BDD-cost:  681
c ---[ 312]---> BDD-cost: 6252
c ---[ 311]---> BDD-cost: 9408
c ---[ 310]---> BDD-cost: 2650
c ---[ 309]---> BDD-cost: 1034
c ---[ 308]---> BDD-cost: 1992
c ---[ 307]---> BDD-cost:  296
c ---[ 306]---> BDD-cost:  158
c ---[ 305]---> BDD-cost:  218
c ---[ 304]---> BDD-cost:   84
c ---[ 303]---> BDD-cost:  105
c ---[ 302]---> BDD-cost:  674
c ---[ 301]---> BDD-cost:  464
c ---[ 300]---> BDD-cost:  529
c ---[ 299]---> Adder-cost: 10512   maxlim: 20   bits: 6/5
c ---[ 298]---> BDD-cost: 1330
c ---[ 297]---> BDD-cost: 2050
c ---[ 296]---> BDD-cost: 4523
c ---[ 295]---> BDD-cost: 1380
c ---[ 294]---> BDD-cost: 2608
c ---[ 293]---> BDD-cost: 1264
c ---[ 292]---> BDD-cost: 1785
c ---[ 291]---> BDD-cost:  958
c ---[ 290]---> BDD-cost: 1203
c ---[ 289]---> BDD-cost:  262
c ---[ 288]---> BDD-cost:  346
c ---[ 287]---> BDD-cost: 1298
c ---[ 286]---> BDD-cost:   98
c ---[ 285]---> BDD-cost:  121
c ---[ 284]---> BDD-cost:  610
c ---[ 283]---> BDD-cost:  665
c ---[ 282]---> BDD-cost:  898
c ---[ 281]---> BDD-cost: 1025
c ---[ 280]---> BDD-cost:  201
c ---[ 279]---> BDD-cost: 2210
c ---[ 278]---> BDD-cost:  198
c ---[ 277]---> BDD-cost:   64
c ---[ 276]---> BDD-cost:  412
c ---[ 275]---> BDD-cost:  182
c ---[ 274]---> BDD-cost: 6136
c ---[ 273]---> BDD-cost: 9887
c ---[ 272]---> BDD-cost:  530
c ---[ 271]---> BDD-cost:  898
c ---[ 270]---> BDD-cost:  684
c ---[ 269]---> BDD-cost: 1314
c ---[ 268]---> BDD-cost: 9446
c ---[ 267]---> BDD-cost:  526
c ---[ 266]---> BDD-cost:  597
c ---[ 265]---> BDD-cost: 1898
c ---[ 264]---> BDD-cost:  352
c ---[ 263]---> BDD-cost:  437
c ---[ 262]---> BDD-cost: 4608
c ---[ 261]---> BDD-cost: 1452
c ---[ 260]---> BDD-cost: 2414
c ---[ 259]---> BDD-cost: 1628
c ---[ 258]---> BDD-cost:  810
c ---[ 257]---> BDD-cost:  168
c ---[ 256]---> BDD-cost:  181
c ---[ 255]---> Adder-cost: 4121   maxlim: 14   bits: 5/4
c ---[ 254]---> BDD-cost:  568
c ---[ 253]---> BDD-cost:  618
c ---[ 252]---> BDD-cost:   36
c ---[ 251]---> BDD-cost:   40
c ---[ 250]---> BDD-cost: 1808
c ---[ 249]---> BDD-cost: 3823
c ---[ 248]---> BDD-cost:   58
c ---[ 247]---> BDD-cost: 4462
c ---[ 246]---> Adder-cost: 2035   maxlim: 14   bits: 5/4
c ---[ 245]---> Adder-cost: 2163   maxlim: 11   bits: 5/4
c ---[ 244]---> BDD-cost: 2612
c ---[ 243]---> Adder-cost: 587   maxlim: 5   bits: 4/3
c ---[ 242]---> BDD-cost: 1609
c ---[ 241]---> BDD-cost: 7110
c ---[ 240]---> Adder-cost: 2371   maxlim: 6   bits: 4/3
c ---[ 239]---> Adder-cost: 279   maxlim: 4   bits: 4/3
c ---[ 238]---> BDD-cost:  386
c ---[ 237]---> Adder-cost: 1815   maxlim: 5   bits: 4/3
c ---[ 236]---> BDD-cost: 1174
c ---[ 235]---> Adder-cost: 7711   maxlim: 20   bits: 6/5
c ---[ 234]---> BDD-cost:  312
c ---[ 233]---> BDD-cost:  408
c ---[ 232]---> BDD-cost:19533
c ---[ 231]---> BDD-cost: 1819
c ---[ 230]---> BDD-cost:  437
c ---[ 229]---> BDD-cost: 2422
c ---[ 228]---> BDD-cost:   70
c ---[ 227]---> Adder-cost: 882   maxlim: 10   bits: 5/4
c ---[ 226]---> Adder-cost: 2457   maxlim: 13   bits: 5/4
c ---[ 225]---> BDD-cost: 3474
c ---[ 224]---> BDD-cost:   29
c ---[ 223]---> BDD-cost:  588
c ---[ 222]---> BDD-cost:  213
c ---[ 221]---> BDD-cost:   70
c ---[ 220]---> BDD-cost:   64
c ---[ 219]---> BDD-cost: 3375
c ---[ 218]---> BDD-cost:  742
c ---[ 217]---> BDD-cost:  536
c ---[ 216]---> BDD-cost:  294
c ---[ 215]---> BDD-cost:  338
c ---[ 214]---> BDD-cost:  820
c ---[ 213]---> BDD-cost: 1332
c ---[ 212]---> BDD-cost:  932
c ---[ 211]---> BDD-cost:   16
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost: 1220
c ---[ 208]---> BDD-cost:   40
c ---[ 207]---> BDD-cost: 2412
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost: 1270
c ---[ 204]---> BDD-cost:  208
c ---[ 203]---> BDD-cost:   38
c ---[ 202]---> BDD-cost:    4
c ---[ 201]---> BDD-cost: 1078
c ---[ 200]---> BDD-cost:  298
c ---[ 199]---> BDD-cost: 2278
c ---[ 198]---> BDD-cost:    2
c ---[ 197]---> BDD-cost:  506
c ---[ 196]---> BDD-cost:  130
c ---[ 195]---> BDD-cost:   12
c ---[ 194]---> BDD-cost: 1426
c ---[ 193]---> BDD-cost: 3402
c ---[ 192]---> BDD-cost:  238
c ---[ 191]---> BDD-cost:  308
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:  224
c ---[ 188]---> BDD-cost:  280
c ---[ 187]---> BDD-cost:   76
c ---[ 186]---> BDD-cost:  662
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:  410
c ---[ 183]---> BDD-cost: 1508
c ---[ 182]---> BDD-cost: 1882
c ---[ 181]---> BDD-cost:  250
c ---[ 180]---> BDD-cost:  974
c ---[ 179]---> BDD-cost: 4460
c ---[ 178]---> BDD-cost:  550
c ---[ 177]---> BDD-cost:  400
c ---[ 176]---> BDD-cost:  520
c ---[ 175]---> BDD-cost:  418
c ---[ 174]---> BDD-cost: 1538
c ---[ 173]---> BDD-cost: 2989
c ---[ 172]---> BDD-cost:  744
c ---[ 171]---> BDD-cost:  128
c ---[ 170]---> BDD-cost:   30
c ---[ 169]---> BDD-cost:  381
c ---[ 168]---> BDD-cost:  192
c ---[ 167]---> BDD-cost: 4854
c ---[ 166]---> BDD-cost: 2388
c ---[ 165]---> BDD-cost: 1773
c ---[ 164]---> BDD-cost: 1077
c ---[ 163]---> BDD-cost:  693
c ---[ 162]---> BDD-cost:  202
c ---[ 161]---> BDD-cost: 1231
c ---[ 160]---> BDD-cost:   54
c ---[ 159]---> BDD-cost:  220
c ---[ 158]---> BDD-cost:  100
c ---[ 157]---> BDD-cost: 1052
c ---[ 156]---> BDD-cost:  402
c ---[ 155]---> BDD-cost:  132
c ---[ 154]---> BDD-cost:  103
c ---[ 153]---> BDD-cost: 4879
c ---[ 152]---> BDD-cost:  979
c ---[ 151]---> BDD-cost:  747
c ---[ 150]---> BDD-cost:  229
c ---[ 149]---> BDD-cost:   74
c ---[ 148]---> BDD-cost:  861
c ---[ 147]---> BDD-cost: 1367
c ---[ 146]---> BDD-cost: 1764
c ---[ 145]---> BDD-cost:  176
c ---[ 144]---> BDD-cost:   64
c ---[ 143]---> BDD-cost:   16
c ---[ 142]---> BDD-cost:   46
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:  719
c ---[ 139]---> BDD-cost: 1247
c ---[ 138]---> BDD-cost: 5433
c ---[ 137]---> BDD-cost:   42
c ---[ 136]---> BDD-cost:  164
c ---[ 135]---> BDD-cost: 4280
c ---[ 134]---> BDD-cost:   26
c ---[ 133]---> BDD-cost:  495
c ---[ 132]---> Adder-cost: 2261   maxlim: 9   bits: 5/4
c ---[ 131]---> Adder-cost: 1869   maxlim: 16   bits: 6/5
c ---[ 130]---> BDD-cost:   28
c ---[ 129]---> BDD-cost:  712
c ---[ 128]---> BDD-cost:  642
c ---[ 127]---> BDD-cost:   10
c ---[ 126]---> BDD-cost: 1438
c ---[ 125]---> BDD-cost:   46
c ---[ 124]---> BDD-cost:  832
c ---[ 123]---> BDD-cost:   88
c ---[ 122]---> BDD-cost:   32
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:  330
c ---[ 119]---> BDD-cost:  204
c ---[ 118]---> BDD-cost:    6
c ---[ 117]---> BDD-cost:   42
c ---[ 116]---> BDD-cost:  242
c ---[ 115]---> BDD-cost:   96
c ---[ 114]---> BDD-cost:  328
c ---[ 113]---> BDD-cost: 1814
c ---[ 112]---> BDD-cost:  650
c ---[ 111]---> BDD-cost: 2914
c ---[ 110]---> BDD-cost:  393
c ---[ 109]---> BDD-cost: 1491
c ---[ 108]---> BDD-cost:  133
c ---[ 107]---> BDD-cost:  222
c ---[ 106]---> BDD-cost: 2917
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:  731
c ---[ 103]---> BDD-cost: 4814
c ---[ 102]---> BDD-cost:  242
c ---[ 101]---> BDD-cost:  860
c ---[ 100]---> BDD-cost:   42
c ---[  99]---> BDD-cost: 2263
c ---[  98]---> BDD-cost:  889
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:   46
c ---[  95]---> BDD-cost: 2502
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost: 1412
c ---[  92]---> BDD-cost:   40
c ---[  91]---> BDD-cost:  962
c ---[  90]---> BDD-cost:  593
c ---[  89]---> BDD-cost: 3603
c ---[  88]---> BDD-cost: 7334
c ---[  87]---> BDD-cost: 6232
c ---[  86]---> BDD-cost:   56
c ---[  85]---> BDD-cost:  854
c ---[  84]---> BDD-cost: 2132
c ---[  83]---> BDD-cost:  564
c ---[  82]---> BDD-cost:  530
c ---[  81]---> BDD-cost:  588
c ---[  80]---> BDD-cost: 1928
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost: 1526
c ---[  77]---> BDD-cost:  164
c ---[  76]---> BDD-cost:  836
c ---[  75]---> BDD-cost: 3300
c ---[  74]---> BDD-cost:  436
c ---[  73]---> BDD-cost: 1340
c ---[  72]---> BDD-cost: 1157
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:   30
c ---[  69]---> BDD-cost: 4103
c ---[  68]---> BDD-cost: 2830
c ---[  67]---> BDD-cost: 1784
c ---[  66]---> BDD-cost:  246
c ---[  65]---> BDD-cost:  362
c ---[  64]---> BDD-cost:  576
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:  358
c ---[  61]---> Adder-cost: 3827   maxlim: 14   bits: 5/4
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   40
c ---[  58]---> BDD-cost:  746
c ---[  57]---> BDD-cost:  962
c ---[  56]---> BDD-cost:  154
c ---[  55]---> BDD-cost: 3669
c ---[  54]---> BDD-cost: 2307
c ---[  53]---> BDD-cost: 1162
c ---[  52]---> BDD-cost: 1022
c ---[  51]---> BDD-cost:   88
c ---[  50]---> BDD-cost:  118
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost: 5703
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:   72
c ---[  45]---> BDD-cost:   84
c ---[  44]---> BDD-cost:   70
c ---[  43]---> BDD-cost: 2172
c ---[  42]---> BDD-cost:   52
c ---[  41]---> BDD-cost:   68
c ---[  40]---> BDD-cost: 1812
c ---[  39]---> BDD-cost:   34
c ---[  38]---> BDD-cost:   36
c ---[  37]---> BDD-cost: 5810
c ---[  36]---> BDD-cost: 5039
c ---[  35]---> BDD-cost:  306
c ---[  34]---> BDD-cost:  154
c ---[  33]---> BDD-cost: 1326
c ---[  32]---> Adder-cost: 3997   maxlim: 14   bits: 5/4
c ---[  31]---> Adder-cost: 6712   maxlim: 20   bits: 6/5
c ---[  30]---> BDD-cost: 2005
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:  140
c ---[  27]---> BDD-cost: 1014
c ---[  26]---> BDD-cost:  360
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:    6
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:  414
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:  774
c ---[  18]---> BDD-cost:  216
c ---[  17]---> BDD-cost:  144
c ---[  16]---> BDD-cost:   45
c ---[  15]---> BDD-cost:  222
c ---[  14]---> BDD-cost: 2136
c ---[  13]---> BDD-cost:  120
c ---[  12]---> BDD-cost:  502
c ---[  11]---> BDD-cost:  680
c ---[  10]---> BDD-cost: 2384
c ---[   9]---> BDD-cost: 7427
c ---[   8]---> Adder-cost: 1614   maxlim: 14   bits: 5/4
c ---[   7]---> BDD-cost: 1352
c ---[   6]---> BDD-cost:  398
c ---[   5]---> BDD-cost:  664
c ---[   4]---> BDD-cost:  246
c ---[   3]---> BDD-cost: 7708
c ---[   2]---> Adder-cost: 7609   maxlim: 18   bits: 6/5
c ---[   1]---> BDD-cost:   34
c ---[   0]---> BDD-cost:   28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1777845  6002235 |  592615       0        0     nan |  0.000 % |
c |       101 | 1777845  6002235 |  651876     101      459     4.5 |  0.218 % |
c |       251 | 1777845  6002235 |  717064     251     1530     6.1 |  0.218 % |
c |       476 | 1777835  6002207 |  788770     472     2460     5.2 |  0.218 % |
c |       813 | 1777835  6002207 |  867647     809     4480     5.5 |  0.218 % |
c |      1319 | 1777785  6002061 |  954412    1295     6907     5.3 |  0.221 % |
c |      2078 | 1777777  6002037 | 1049853    2047    11034     5.4 |  0.221 % |
c |      3217 | 1777626  6001604 | 1154838    3079    18141     5.9 |  0.228 % |
c |      4925 | 1777470  6001146 | 1270322    4743    29622     6.2 |  0.235 % |
c |      7487 | 1777250  6000416 | 1397355    7259    47300     6.5 |  0.240 % |
c |     11331 | 1777240  6000386 | 1537090   11099   149202    13.4 |  0.241 % |
c |     17097 | 1776649  5998585 | 1690799   16738   208091    12.4 |  0.263 % |
c |     25746 | 1775548  5995152 | 1859879   25098   277850    11.1 |  0.305 % |
c |     38720 | 1773964  5990312 | 2045867   37044   375587    10.1 |  0.376 % |
c |     58182 | 1772211  5984665 | 2250454   55726   533174     9.6 |  0.436 % |

Watcher Data

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/16143/stat): 16143 (minisat+_script) R 16142 16143 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854862191 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16143/statm): 174 3 169 147 0 27 0
[pid=16143] 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=16144
New process pid=16145
New process pid=16146
execve syscall for /bin/sed executable
One traced child (pid=16145) 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=16146) exited with status: 0
One traced child (pid=16144) exited with status: 0
New process pid=16147
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-sp98ar.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.97 0.98 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 13394 0 0 0 897 52 0 0 25 0 1 0 1854862196 49704960 9553 4294967295 134512640 135094434 3221224432 3221222320 134780558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 12135 9553 145 145 0 11990 0
[pid=16147] vsize: 48540
Current children cumulated CPU time (s) 9.5
Current children cumulated vsize (Kb) 50664

[startup+20.004 s]
Raw data (loadavg): 0.94 0.97 0.98 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 31878 0 0 0 1798 111 0 0 21 0 1 0 1854862196 113717248 25138 4294967295 134512640 135094434 3221224432 3221079708 134870330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 27763 25138 145 145 0 27618 0
[pid=16147] vsize: 111052
Current children cumulated CPU time (s) 19.1
Current children cumulated vsize (Kb) 113176

[startup+30.0047 s]
Raw data (loadavg): 1.03 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 58081 0 0 0 2562 225 0 0 25 0 1 0 1854862196 249634816 51341 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16147/statm): 60946 51341 145 145 0 60801 0
[pid=16147] vsize: 243784
Current children cumulated CPU time (s) 27.88
Current children cumulated vsize (Kb) 245908

[startup+40.0063 s]
Raw data (loadavg): 1.03 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 59374 0 0 0 3545 233 0 0 25 0 1 0 1854862196 254930944 52634 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16147/statm): 62239 52634 145 145 0 62094 0
[pid=16147] vsize: 248956
Current children cumulated CPU time (s) 37.79
Current children cumulated vsize (Kb) 251080

[startup+50.0071 s]
Raw data (loadavg): 1.02 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 59777 0 0 0 4539 235 0 0 25 0 1 0 1854862196 256581632 53037 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 62642 53037 145 145 0 62497 0
[pid=16147] vsize: 250568
Current children cumulated CPU time (s) 47.75
Current children cumulated vsize (Kb) 252692

[startup+60.0077 s]
Raw data (loadavg): 1.02 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60040 0 0 0 5536 237 0 0 25 0 1 0 1854862196 257658880 53300 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 62905 53300 145 145 0 62760 0
[pid=16147] vsize: 251620
Current children cumulated CPU time (s) 57.74
Current children cumulated vsize (Kb) 253744

[startup+70.0084 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60128 0 0 0 6534 237 0 0 25 0 1 0 1854862196 258019328 53388 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 62993 53388 145 145 0 62848 0
[pid=16147] vsize: 251972
Current children cumulated CPU time (s) 67.72
Current children cumulated vsize (Kb) 254096

[startup+80.0101 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60307 0 0 0 7532 238 0 0 25 0 1 0 1854862196 258867200 53567 4294967295 134512640 135094434 3221224432 3221223164 134554482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63200 53567 145 145 0 63055 0
[pid=16147] vsize: 252800
Current children cumulated CPU time (s) 77.71
Current children cumulated vsize (Kb) 254924

[startup+90.0108 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60450 0 0 0 8529 239 0 0 25 0 1 0 1854862196 259448832 53710 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63342 53710 145 145 0 63197 0
[pid=16147] vsize: 253368
Current children cumulated CPU time (s) 87.69
Current children cumulated vsize (Kb) 255492

[startup+100.011 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60517 0 0 0 9529 240 0 0 25 0 1 0 1854862196 259719168 53777 4294967295 134512640 135094434 3221224432 3221223044 134563107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63408 53777 145 145 0 63263 0
[pid=16147] vsize: 253632
Current children cumulated CPU time (s) 97.7
Current children cumulated vsize (Kb) 255756

[startup+110.012 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60691 0 0 0 10526 241 0 0 25 0 1 0 1854862196 260444160 53951 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63585 53951 145 145 0 63440 0
[pid=16147] vsize: 254340
Current children cumulated CPU time (s) 107.68
Current children cumulated vsize (Kb) 256464

[startup+120.013 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60727 0 0 0 11526 241 0 0 25 0 1 0 1854862196 260587520 53987 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63620 53987 145 145 0 63475 0
[pid=16147] vsize: 254480
Current children cumulated CPU time (s) 117.68
Current children cumulated vsize (Kb) 256604

[startup+130.014 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60782 0 0 0 12526 242 0 0 25 0 1 0 1854862196 260812800 54042 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63675 54042 145 145 0 63530 0
[pid=16147] vsize: 254700
Current children cumulated CPU time (s) 127.69
Current children cumulated vsize (Kb) 256824

[startup+140.014 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 60944 0 0 0 13523 243 0 0 25 0 1 0 1854862196 261423104 54204 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63824 54204 145 145 0 63679 0
[pid=16147] vsize: 255296
Current children cumulated CPU time (s) 137.67
Current children cumulated vsize (Kb) 257420

[startup+150.016 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61086 0 0 0 14521 244 0 0 25 0 1 0 1854862196 261939200 54346 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 63950 54346 145 145 0 63805 0
[pid=16147] vsize: 255800
Current children cumulated CPU time (s) 147.66
Current children cumulated vsize (Kb) 257924

[startup+160.017 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61234 0 0 0 15521 244 0 0 25 0 1 0 1854862196 262250496 54494 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64026 54494 145 145 0 63881 0
[pid=16147] vsize: 256104
Current children cumulated CPU time (s) 157.66
Current children cumulated vsize (Kb) 258228

[startup+170.017 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61389 0 0 0 16519 245 0 0 25 0 1 0 1854862196 263057408 54649 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64223 54649 145 145 0 64078 0
[pid=16147] vsize: 256892
Current children cumulated CPU time (s) 167.65
Current children cumulated vsize (Kb) 259016

[startup+180.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61499 0 0 0 17519 246 0 0 25 0 1 0 1854862196 263454720 54759 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64320 54759 145 145 0 64175 0
[pid=16147] vsize: 257280
Current children cumulated CPU time (s) 177.66
Current children cumulated vsize (Kb) 259404

[startup+190.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61515 0 0 0 18519 246 0 0 25 0 1 0 1854862196 263507968 54775 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64333 54775 145 145 0 64188 0
[pid=16147] vsize: 257332
Current children cumulated CPU time (s) 187.66
Current children cumulated vsize (Kb) 259456

[startup+200.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61532 0 0 0 19519 246 0 0 25 0 1 0 1854862196 263573504 54792 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64349 54792 145 145 0 64204 0
[pid=16147] vsize: 257396
Current children cumulated CPU time (s) 197.66
Current children cumulated vsize (Kb) 259520

[startup+210.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61554 0 0 0 20519 246 0 0 25 0 1 0 1854862196 263663616 54814 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64371 54814 145 145 0 64226 0
[pid=16147] vsize: 257484
Current children cumulated CPU time (s) 207.66
Current children cumulated vsize (Kb) 259608

[startup+220.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61571 0 0 0 21519 246 0 0 25 0 1 0 1854862196 263729152 54831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64387 54831 145 145 0 64242 0
[pid=16147] vsize: 257548
Current children cumulated CPU time (s) 217.66
Current children cumulated vsize (Kb) 259672

[startup+230.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61602 0 0 0 22518 246 0 0 25 0 1 0 1854862196 263852032 54862 4294967295 134512640 135094434 3221224432 3221223092 134553475 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64417 54862 145 145 0 64272 0
[pid=16147] vsize: 257668
Current children cumulated CPU time (s) 227.65
Current children cumulated vsize (Kb) 259792

[startup+240.022 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61636 0 0 0 23518 247 0 0 25 0 1 0 1854862196 263962624 54896 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64444 54896 145 145 0 64299 0
[pid=16147] vsize: 257776
Current children cumulated CPU time (s) 237.66
Current children cumulated vsize (Kb) 259900

[startup+250.023 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61673 0 0 0 24518 247 0 0 25 0 1 0 1854862196 264060928 54933 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64468 54933 145 145 0 64323 0
[pid=16147] vsize: 257872
Current children cumulated CPU time (s) 247.66
Current children cumulated vsize (Kb) 259996

[startup+260.023 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61687 0 0 0 25518 247 0 0 25 0 1 0 1854862196 264118272 54947 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64482 54947 145 145 0 64337 0
[pid=16147] vsize: 257928
Current children cumulated CPU time (s) 257.66
Current children cumulated vsize (Kb) 260052

[startup+270.024 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61739 0 0 0 26516 249 0 0 25 0 1 0 1854862196 264327168 54999 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64533 54999 145 145 0 64388 0
[pid=16147] vsize: 258132
Current children cumulated CPU time (s) 267.66
Current children cumulated vsize (Kb) 260256

[startup+280.025 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61765 0 0 0 27515 250 0 0 25 0 1 0 1854862196 264429568 55025 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64558 55025 145 145 0 64413 0
[pid=16147] vsize: 258232
Current children cumulated CPU time (s) 277.66
Current children cumulated vsize (Kb) 260356

[startup+290.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61774 0 0 0 28515 250 0 0 25 0 1 0 1854862196 264466432 55034 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64567 55034 145 145 0 64422 0
[pid=16147] vsize: 258268
Current children cumulated CPU time (s) 287.66
Current children cumulated vsize (Kb) 260392

[startup+300.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61831 0 0 0 29514 251 0 0 25 0 1 0 1854862196 264564736 55091 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64591 55091 145 145 0 64446 0
[pid=16147] vsize: 258364
Current children cumulated CPU time (s) 297.66
Current children cumulated vsize (Kb) 260488

[startup+310.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61845 0 0 0 30514 251 0 0 25 0 1 0 1854862196 264617984 55105 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64604 55105 145 145 0 64459 0
[pid=16147] vsize: 258416
Current children cumulated CPU time (s) 307.66
Current children cumulated vsize (Kb) 260540

[startup+320.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61866 0 0 0 31514 251 0 0 25 0 1 0 1854862196 264699904 55126 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64624 55126 145 145 0 64479 0
[pid=16147] vsize: 258496
Current children cumulated CPU time (s) 317.66
Current children cumulated vsize (Kb) 260620

[startup+330.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61878 0 0 0 32513 252 0 0 25 0 1 0 1854862196 264749056 55138 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64636 55138 145 145 0 64491 0
[pid=16147] vsize: 258544
Current children cumulated CPU time (s) 327.66
Current children cumulated vsize (Kb) 260668

[startup+340.031 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61890 0 0 0 33513 252 0 0 25 0 1 0 1854862196 264794112 55150 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64647 55150 145 145 0 64502 0
[pid=16147] vsize: 258588
Current children cumulated CPU time (s) 337.66
Current children cumulated vsize (Kb) 260712

[startup+350.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61903 0 0 0 34512 252 0 0 25 0 1 0 1854862196 264847360 55163 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64660 55163 145 145 0 64515 0
[pid=16147] vsize: 258640
Current children cumulated CPU time (s) 347.65
Current children cumulated vsize (Kb) 260764

[startup+360.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61912 0 0 0 35513 252 0 0 25 0 1 0 1854862196 264880128 55172 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64668 55172 145 145 0 64523 0
[pid=16147] vsize: 258672
Current children cumulated CPU time (s) 357.66
Current children cumulated vsize (Kb) 260796

[startup+370.033 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61914 0 0 0 36513 252 0 0 25 0 1 0 1854862196 264888320 55174 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64670 55174 145 145 0 64525 0
[pid=16147] vsize: 258680
Current children cumulated CPU time (s) 367.66
Current children cumulated vsize (Kb) 260804

[startup+380.034 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61919 0 0 0 37512 253 0 0 25 0 1 0 1854862196 264908800 55179 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64675 55179 145 145 0 64530 0
[pid=16147] vsize: 258700
Current children cumulated CPU time (s) 377.66
Current children cumulated vsize (Kb) 260824

[startup+390.035 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61985 0 0 0 38513 253 0 0 25 0 1 0 1854862196 264974336 55245 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64691 55245 145 145 0 64546 0
[pid=16147] vsize: 258764
Current children cumulated CPU time (s) 387.67
Current children cumulated vsize (Kb) 260888

[startup+400.035 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61988 0 0 0 39513 253 0 0 25 0 1 0 1854862196 264986624 55248 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64694 55248 145 145 0 64549 0
[pid=16147] vsize: 258776
Current children cumulated CPU time (s) 397.67
Current children cumulated vsize (Kb) 260900

[startup+410.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 61998 0 0 0 40513 253 0 0 25 0 1 0 1854862196 265023488 55258 4294967295 134512640 135094434 3221224432 3221223092 134553457 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64703 55258 145 145 0 64558 0
[pid=16147] vsize: 258812
Current children cumulated CPU time (s) 407.67
Current children cumulated vsize (Kb) 260936

[startup+420.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62003 0 0 0 41513 253 0 0 25 0 1 0 1854862196 265043968 55263 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64708 55263 145 145 0 64563 0
[pid=16147] vsize: 258832
Current children cumulated CPU time (s) 417.67
Current children cumulated vsize (Kb) 260956

[startup+430.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62014 0 0 0 42513 253 0 0 25 0 1 0 1854862196 265084928 55274 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64718 55274 145 145 0 64573 0
[pid=16147] vsize: 258872
Current children cumulated CPU time (s) 427.67
Current children cumulated vsize (Kb) 260996

[startup+440.039 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62035 0 0 0 43513 253 0 0 25 0 1 0 1854862196 265166848 55295 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64738 55295 145 145 0 64593 0
[pid=16147] vsize: 258952
Current children cumulated CPU time (s) 437.67
Current children cumulated vsize (Kb) 261076

[startup+450.039 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62043 0 0 0 44513 254 0 0 25 0 1 0 1854862196 265199616 55303 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64746 55303 145 145 0 64601 0
[pid=16147] vsize: 258984
Current children cumulated CPU time (s) 447.68
Current children cumulated vsize (Kb) 261108

[startup+460.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62117 0 0 0 45513 254 0 0 25 0 1 0 1854862196 265494528 55377 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64818 55377 145 145 0 64673 0
[pid=16147] vsize: 259272
Current children cumulated CPU time (s) 457.68
Current children cumulated vsize (Kb) 261396

[startup+470.041 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62117 0 0 0 46513 254 0 0 25 0 1 0 1854862196 265494528 55377 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64818 55377 145 145 0 64673 0
[pid=16147] vsize: 259272
Current children cumulated CPU time (s) 467.68
Current children cumulated vsize (Kb) 261396

[startup+480.041 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62118 0 0 0 47513 254 0 0 25 0 1 0 1854862196 265494528 55378 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64818 55378 145 145 0 64673 0
[pid=16147] vsize: 259272
Current children cumulated CPU time (s) 477.68
Current children cumulated vsize (Kb) 261396

[startup+490.042 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62137 0 0 0 48514 254 0 0 25 0 1 0 1854862196 265555968 55397 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64833 55397 145 145 0 64688 0
[pid=16147] vsize: 259332
Current children cumulated CPU time (s) 487.69
Current children cumulated vsize (Kb) 261456

[startup+500.043 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62153 0 0 0 49513 254 0 0 25 0 1 0 1854862196 265617408 55413 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64848 55413 145 145 0 64703 0
[pid=16147] vsize: 259392
Current children cumulated CPU time (s) 497.68
Current children cumulated vsize (Kb) 261516

[startup+510.044 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62157 0 0 0 50513 254 0 0 25 0 1 0 1854862196 265633792 55417 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64852 55417 145 145 0 64707 0
[pid=16147] vsize: 259408
Current children cumulated CPU time (s) 507.68
Current children cumulated vsize (Kb) 261532

[startup+520.044 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62174 0 0 0 51513 254 0 0 25 0 1 0 1854862196 265674752 55434 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64862 55434 145 145 0 64717 0
[pid=16147] vsize: 259448
Current children cumulated CPU time (s) 517.68
Current children cumulated vsize (Kb) 261572

[startup+530.045 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62176 0 0 0 52514 254 0 0 25 0 1 0 1854862196 265682944 55436 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64864 55436 145 145 0 64719 0
[pid=16147] vsize: 259456
Current children cumulated CPU time (s) 527.69
Current children cumulated vsize (Kb) 261580

[startup+540.046 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62180 0 0 0 53514 255 0 0 25 0 1 0 1854862196 265695232 55440 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64867 55440 145 145 0 64722 0
[pid=16147] vsize: 259468
Current children cumulated CPU time (s) 537.7
Current children cumulated vsize (Kb) 261592

[startup+550.046 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62186 0 0 0 54512 255 0 0 25 0 1 0 1854862196 265719808 55446 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16147/statm): 64873 55446 145 145 0 64728 0
[pid=16147] vsize: 259492
Current children cumulated CPU time (s) 547.68
Current children cumulated vsize (Kb) 261616

[startup+560.047 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62195 0 0 0 55511 255 0 0 25 0 1 0 1854862196 265752576 55455 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64881 55455 145 145 0 64736 0
[pid=16147] vsize: 259524
Current children cumulated CPU time (s) 557.67
Current children cumulated vsize (Kb) 261648

[startup+570.048 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62209 0 0 0 56512 255 0 0 25 0 1 0 1854862196 265805824 55469 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64894 55469 145 145 0 64749 0
[pid=16147] vsize: 259576
Current children cumulated CPU time (s) 567.68
Current children cumulated vsize (Kb) 261700

[startup+580.048 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62222 0 0 0 57512 255 0 0 25 0 1 0 1854862196 265854976 55482 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64906 55482 145 145 0 64761 0
[pid=16147] vsize: 259624
Current children cumulated CPU time (s) 577.68
Current children cumulated vsize (Kb) 261748

[startup+590.049 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62227 0 0 0 58512 255 0 0 25 0 1 0 1854862196 265875456 55487 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64911 55487 145 145 0 64766 0
[pid=16147] vsize: 259644
Current children cumulated CPU time (s) 587.68
Current children cumulated vsize (Kb) 261768

[startup+600.049 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62236 0 0 0 59512 255 0 0 25 0 1 0 1854862196 265912320 55496 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64920 55496 145 145 0 64775 0
[pid=16147] vsize: 259680
Current children cumulated CPU time (s) 597.68
Current children cumulated vsize (Kb) 261804

[startup+610.049 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62249 0 0 0 60511 256 0 0 25 0 1 0 1854862196 265961472 55509 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64932 55509 145 145 0 64787 0
[pid=16147] vsize: 259728
Current children cumulated CPU time (s) 607.68
Current children cumulated vsize (Kb) 261852

[startup+620.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62263 0 0 0 61511 256 0 0 25 0 1 0 1854862196 266014720 55523 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64945 55523 145 145 0 64800 0
[pid=16147] vsize: 259780
Current children cumulated CPU time (s) 617.68
Current children cumulated vsize (Kb) 261904

[startup+630.052 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62269 0 0 0 62512 256 0 0 25 0 1 0 1854862196 266039296 55529 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64951 55529 145 145 0 64806 0
[pid=16147] vsize: 259804
Current children cumulated CPU time (s) 627.69
Current children cumulated vsize (Kb) 261928

[startup+640.053 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62274 0 0 0 63512 256 0 0 25 0 1 0 1854862196 266059776 55534 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64956 55534 145 145 0 64811 0
[pid=16147] vsize: 259824
Current children cumulated CPU time (s) 637.69
Current children cumulated vsize (Kb) 261948

[startup+650.052 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62283 0 0 0 64512 256 0 0 25 0 1 0 1854862196 266092544 55543 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64964 55543 145 145 0 64819 0
[pid=16147] vsize: 259856
Current children cumulated CPU time (s) 647.69
Current children cumulated vsize (Kb) 261980

[startup+660.054 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62292 0 0 0 65512 256 0 0 25 0 1 0 1854862196 266129408 55552 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64973 55552 145 145 0 64828 0
[pid=16147] vsize: 259892
Current children cumulated CPU time (s) 657.69
Current children cumulated vsize (Kb) 262016

[startup+670.054 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62301 0 0 0 66512 256 0 0 25 0 1 0 1854862196 266162176 55561 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64981 55561 145 145 0 64836 0
[pid=16147] vsize: 259924
Current children cumulated CPU time (s) 667.69
Current children cumulated vsize (Kb) 262048

[startup+680.055 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62311 0 0 0 67512 257 0 0 25 0 1 0 1854862196 266203136 55571 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 64991 55571 145 145 0 64846 0
[pid=16147] vsize: 259964
Current children cumulated CPU time (s) 677.7
Current children cumulated vsize (Kb) 262088

[startup+690.056 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62326 0 0 0 68511 257 0 0 25 0 1 0 1854862196 266260480 55586 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65005 55586 145 145 0 64860 0
[pid=16147] vsize: 260020
Current children cumulated CPU time (s) 687.69
Current children cumulated vsize (Kb) 262144

[startup+700.057 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62338 0 0 0 69511 257 0 0 25 0 1 0 1854862196 266305536 55598 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65016 55598 145 145 0 64871 0
[pid=16147] vsize: 260064
Current children cumulated CPU time (s) 697.69
Current children cumulated vsize (Kb) 262188

[startup+710.057 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62345 0 0 0 70512 257 0 0 25 0 1 0 1854862196 266334208 55605 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65023 55605 145 145 0 64878 0
[pid=16147] vsize: 260092
Current children cumulated CPU time (s) 707.7
Current children cumulated vsize (Kb) 262216

[startup+720.058 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62358 0 0 0 71512 257 0 0 25 0 1 0 1854862196 266383360 55618 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65035 55618 145 145 0 64890 0
[pid=16147] vsize: 260140
Current children cumulated CPU time (s) 717.7
Current children cumulated vsize (Kb) 262264

[startup+730.059 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62370 0 0 0 72512 257 0 0 25 0 1 0 1854862196 266428416 55630 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65046 55630 145 145 0 64901 0
[pid=16147] vsize: 260184
Current children cumulated CPU time (s) 727.7
Current children cumulated vsize (Kb) 262308

[startup+740.059 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62385 0 0 0 73512 257 0 0 25 0 1 0 1854862196 266489856 55645 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65061 55645 145 145 0 64916 0
[pid=16147] vsize: 260244
Current children cumulated CPU time (s) 737.7
Current children cumulated vsize (Kb) 262368

[startup+750.06 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62392 0 0 0 74511 258 0 0 25 0 1 0 1854862196 266514432 55652 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65067 55652 145 145 0 64922 0
[pid=16147] vsize: 260268
Current children cumulated CPU time (s) 747.7
Current children cumulated vsize (Kb) 262392

[startup+760.061 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62399 0 0 0 75511 258 0 0 25 0 1 0 1854862196 266543104 55659 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65074 55659 145 145 0 64929 0
[pid=16147] vsize: 260296
Current children cumulated CPU time (s) 757.7
Current children cumulated vsize (Kb) 262420

[startup+770.06 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62406 0 0 0 76511 258 0 0 25 0 1 0 1854862196 266571776 55666 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65081 55666 145 145 0 64936 0
[pid=16147] vsize: 260324
Current children cumulated CPU time (s) 767.7
Current children cumulated vsize (Kb) 262448

[startup+780.061 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62410 0 0 0 77512 258 0 0 25 0 1 0 1854862196 266584064 55670 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65084 55670 145 145 0 64939 0
[pid=16147] vsize: 260336
Current children cumulated CPU time (s) 777.71
Current children cumulated vsize (Kb) 262460

[startup+790.062 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62423 0 0 0 78512 258 0 0 25 0 1 0 1854862196 266608640 55683 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65090 55683 145 145 0 64945 0
[pid=16147] vsize: 260360
Current children cumulated CPU time (s) 787.71
Current children cumulated vsize (Kb) 262484

[startup+800.061 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62431 0 0 0 79512 258 0 0 25 0 1 0 1854862196 266641408 55691 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65098 55691 145 145 0 64953 0
[pid=16147] vsize: 260392
Current children cumulated CPU time (s) 797.71
Current children cumulated vsize (Kb) 262516

[startup+810.062 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62438 0 0 0 80512 258 0 0 25 0 1 0 1854862196 266665984 55698 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65104 55698 145 145 0 64959 0
[pid=16147] vsize: 260416
Current children cumulated CPU time (s) 807.71
Current children cumulated vsize (Kb) 262540

[startup+820.063 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62471 0 0 0 81512 258 0 0 25 0 1 0 1854862196 266690560 55731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65110 55731 145 145 0 64965 0
[pid=16147] vsize: 260440
Current children cumulated CPU time (s) 817.71
Current children cumulated vsize (Kb) 262564

[startup+830.063 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62486 0 0 0 82512 258 0 0 25 0 1 0 1854862196 266747904 55746 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65124 55746 145 145 0 64979 0
[pid=16147] vsize: 260496
Current children cumulated CPU time (s) 827.71
Current children cumulated vsize (Kb) 262620

[startup+840.064 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62496 0 0 0 83511 259 0 0 25 0 1 0 1854862196 266788864 55756 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65134 55756 145 145 0 64989 0
[pid=16147] vsize: 260536
Current children cumulated CPU time (s) 837.71
Current children cumulated vsize (Kb) 262660

[startup+850.065 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62507 0 0 0 84512 259 0 0 25 0 1 0 1854862196 266829824 55767 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65144 55767 145 145 0 64999 0
[pid=16147] vsize: 260576
Current children cumulated CPU time (s) 847.72
Current children cumulated vsize (Kb) 262700

[startup+860.066 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62517 0 0 0 85512 259 0 0 25 0 1 0 1854862196 266858496 55777 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65151 55777 145 145 0 65006 0
[pid=16147] vsize: 260604
Current children cumulated CPU time (s) 857.72
Current children cumulated vsize (Kb) 262728

[startup+870.066 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62524 0 0 0 86510 261 0 0 25 0 1 0 1854862196 266883072 55784 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65157 55784 145 145 0 65012 0
[pid=16147] vsize: 260628
Current children cumulated CPU time (s) 867.72
Current children cumulated vsize (Kb) 262752

[startup+880.067 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62531 0 0 0 87510 261 0 0 25 0 1 0 1854862196 266911744 55791 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65164 55791 145 145 0 65019 0
[pid=16147] vsize: 260656
Current children cumulated CPU time (s) 877.72
Current children cumulated vsize (Kb) 262780

[startup+890.068 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62542 0 0 0 88510 262 0 0 25 0 1 0 1854862196 266936320 55802 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65170 55802 145 145 0 65025 0
[pid=16147] vsize: 260680
Current children cumulated CPU time (s) 887.73
Current children cumulated vsize (Kb) 262804

[startup+900.068 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62554 0 0 0 89509 262 0 0 25 0 1 0 1854862196 266981376 55814 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65181 55814 145 145 0 65036 0
[pid=16147] vsize: 260724
Current children cumulated CPU time (s) 897.72
Current children cumulated vsize (Kb) 262848

[startup+910.069 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62559 0 0 0 90508 263 0 0 25 0 1 0 1854862196 267001856 55819 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16147/statm): 65186 55819 145 145 0 65041 0
[pid=16147] vsize: 260744
Current children cumulated CPU time (s) 907.72
Current children cumulated vsize (Kb) 262868

[startup+920.07 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62573 0 0 0 91507 263 0 0 25 0 1 0 1854862196 267055104 55833 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65199 55833 145 145 0 65054 0
[pid=16147] vsize: 260796
Current children cumulated CPU time (s) 917.71
Current children cumulated vsize (Kb) 262920

[startup+930.071 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62582 0 0 0 92507 264 0 0 25 0 1 0 1854862196 267091968 55842 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65208 55842 145 145 0 65063 0
[pid=16147] vsize: 260832
Current children cumulated CPU time (s) 927.72
Current children cumulated vsize (Kb) 262956

[startup+940.072 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62593 0 0 0 93507 264 0 0 25 0 1 0 1854862196 267132928 55853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65218 55853 145 145 0 65073 0
[pid=16147] vsize: 260872
Current children cumulated CPU time (s) 937.72
Current children cumulated vsize (Kb) 262996

[startup+950.072 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62605 0 0 0 94506 265 0 0 25 0 1 0 1854862196 267177984 55865 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65229 55865 145 145 0 65084 0
[pid=16147] vsize: 260916
Current children cumulated CPU time (s) 947.72
Current children cumulated vsize (Kb) 263040

[startup+960.072 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62627 0 0 0 95506 265 0 0 25 0 1 0 1854862196 267247616 55887 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65246 55887 145 145 0 65101 0
[pid=16147] vsize: 260984
Current children cumulated CPU time (s) 957.72
Current children cumulated vsize (Kb) 263108

[startup+970.073 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62645 0 0 0 96506 265 0 0 25 0 1 0 1854862196 267317248 55905 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65263 55905 145 145 0 65118 0
[pid=16147] vsize: 261052
Current children cumulated CPU time (s) 967.72
Current children cumulated vsize (Kb) 263176

[startup+980.074 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62655 0 0 0 97506 265 0 0 25 0 1 0 1854862196 267354112 55915 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65272 55915 145 145 0 65127 0
[pid=16147] vsize: 261088
Current children cumulated CPU time (s) 977.72
Current children cumulated vsize (Kb) 263212

[startup+990.074 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62678 0 0 0 98506 266 0 0 25 0 1 0 1854862196 267390976 55938 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65281 55938 145 145 0 65136 0
[pid=16147] vsize: 261124
Current children cumulated CPU time (s) 987.73
Current children cumulated vsize (Kb) 263248

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62687 0 0 0 99505 266 0 0 25 0 1 0 1854862196 267423744 55947 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65289 55947 145 145 0 65144 0
[pid=16147] vsize: 261156
Current children cumulated CPU time (s) 997.72
Current children cumulated vsize (Kb) 263280

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62701 0 0 0 100505 266 0 0 25 0 1 0 1854862196 267476992 55961 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65302 55961 145 145 0 65157 0
[pid=16147] vsize: 261208
Current children cumulated CPU time (s) 1007.72
Current children cumulated vsize (Kb) 263332

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62713 0 0 0 101505 266 0 0 25 0 1 0 1854862196 267526144 55973 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65314 55973 145 145 0 65169 0
[pid=16147] vsize: 261256
Current children cumulated CPU time (s) 1017.72
Current children cumulated vsize (Kb) 263380

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62726 0 0 0 102506 266 0 0 25 0 1 0 1854862196 267575296 55986 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65326 55986 145 145 0 65181 0
[pid=16147] vsize: 261304
Current children cumulated CPU time (s) 1027.73
Current children cumulated vsize (Kb) 263428

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62732 0 0 0 103506 266 0 0 25 0 1 0 1854862196 267599872 55992 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65332 55992 145 145 0 65187 0
[pid=16147] vsize: 261328
Current children cumulated CPU time (s) 1037.73
Current children cumulated vsize (Kb) 263452

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62735 0 0 0 104506 266 0 0 25 0 1 0 1854862196 267612160 55995 4294967295 134512640 135094434 3221224432 3221223088 134561748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65335 55995 145 145 0 65190 0
[pid=16147] vsize: 261340
Current children cumulated CPU time (s) 1047.73
Current children cumulated vsize (Kb) 263464

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62743 0 0 0 105506 267 0 0 25 0 1 0 1854862196 267640832 56003 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65342 56003 145 145 0 65197 0
[pid=16147] vsize: 261368
Current children cumulated CPU time (s) 1057.74
Current children cumulated vsize (Kb) 263492

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62755 0 0 0 106506 267 0 0 25 0 1 0 1854862196 267948032 56015 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65417 56015 145 145 0 65272 0
[pid=16147] vsize: 261668
Current children cumulated CPU time (s) 1067.74
Current children cumulated vsize (Kb) 263792

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62762 0 0 0 107506 267 0 0 25 0 1 0 1854862196 267976704 56022 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65424 56022 145 145 0 65279 0
[pid=16147] vsize: 261696
Current children cumulated CPU time (s) 1077.74
Current children cumulated vsize (Kb) 263820

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62775 0 0 0 108506 267 0 0 25 0 1 0 1854862196 268025856 56035 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65436 56035 145 145 0 65291 0
[pid=16147] vsize: 261744
Current children cumulated CPU time (s) 1087.74
Current children cumulated vsize (Kb) 263868

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62786 0 0 0 109505 268 0 0 25 0 1 0 1854862196 268070912 56046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65447 56046 145 145 0 65302 0
[pid=16147] vsize: 261788
Current children cumulated CPU time (s) 1097.74
Current children cumulated vsize (Kb) 263912

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62798 0 0 0 110505 268 0 0 25 0 1 0 1854862196 268115968 56058 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65458 56058 145 145 0 65313 0
[pid=16147] vsize: 261832
Current children cumulated CPU time (s) 1107.74
Current children cumulated vsize (Kb) 263956

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62836 0 0 0 111505 268 0 0 25 0 1 0 1854862196 268263424 56096 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65494 56096 145 145 0 65349 0
[pid=16147] vsize: 261976
Current children cumulated CPU time (s) 1117.74
Current children cumulated vsize (Kb) 264100

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62860 0 0 0 112504 268 0 0 25 0 1 0 1854862196 268357632 56120 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65517 56120 145 145 0 65372 0
[pid=16147] vsize: 262068
Current children cumulated CPU time (s) 1127.73
Current children cumulated vsize (Kb) 264192

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62879 0 0 0 113504 268 0 0 25 0 1 0 1854862196 268431360 56139 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65535 56139 145 145 0 65390 0
[pid=16147] vsize: 262140
Current children cumulated CPU time (s) 1137.73
Current children cumulated vsize (Kb) 264264

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62891 0 0 0 114504 269 0 0 25 0 1 0 1854862196 268480512 56151 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65547 56151 145 145 0 65402 0
[pid=16147] vsize: 262188
Current children cumulated CPU time (s) 1147.74
Current children cumulated vsize (Kb) 264312

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62916 0 0 0 115503 269 0 0 25 0 1 0 1854862196 268574720 56176 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65570 56176 145 145 0 65425 0
[pid=16147] vsize: 262280
Current children cumulated CPU time (s) 1157.73
Current children cumulated vsize (Kb) 264404

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62931 0 0 0 116504 269 0 0 25 0 1 0 1854862196 268636160 56191 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65585 56191 145 145 0 65440 0
[pid=16147] vsize: 262340
Current children cumulated CPU time (s) 1167.74
Current children cumulated vsize (Kb) 264464

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62951 0 0 0 117503 269 0 0 25 0 1 0 1854862196 268713984 56211 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65604 56211 145 145 0 65459 0
[pid=16147] vsize: 262416
Current children cumulated CPU time (s) 1177.73
Current children cumulated vsize (Kb) 264540

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62974 0 0 0 118503 270 0 0 25 0 1 0 1854862196 268804096 56234 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65626 56234 145 145 0 65481 0
[pid=16147] vsize: 262504
Current children cumulated CPU time (s) 1187.74
Current children cumulated vsize (Kb) 264628

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62984 0 0 0 119503 270 0 0 25 0 1 0 1854862196 268840960 56244 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65635 56244 145 145 0 65490 0
[pid=16147] vsize: 262540
Current children cumulated CPU time (s) 1197.74
Current children cumulated vsize (Kb) 264664

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62990 0 0 0 120503 270 0 0 25 0 1 0 1854862196 268857344 56250 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65639 56250 145 145 0 65494 0
[pid=16147] vsize: 262556
Current children cumulated CPU time (s) 1207.74
Current children cumulated vsize (Kb) 264680



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 16147
Raw data (/proc/16143/stat): 16143 (minisat+_script) S 16142 16143 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1854862191 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16143/statm): 531 226 485 147 0 384 0
[pid=16143] vsize: 2124
Raw data (/proc/16147/stat): 16147 (minisat+_64-bit) R 16143 16143 16528 0 -1 0 62990 0 0 0 120503 270 0 0 25 0 1 0 1854862196 268857344 56250 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16147/statm): 65639 56250 145 145 0 65494 0
[pid=16147] vsize: 262556
Current children cumulated CPU time (s) 1207.74
Current children cumulated vsize (Kb) 264680

Sending SIGTERM to -16143
Sleeping 2 seconds
One traced child (pid=16143) ended because it received signal 15 (SIGTERM)
One traced child (pid=16147) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.2
CPU time (s): 1207.85
CPU user time (s): 1205.04
CPU system time (s): 2.81757
CPU usage (%): 99.8057
Max. virtual memory (cumulated for all children) (Kb): 264680

Verifier Data

ERROR: no interpretation found !