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-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-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 benchmark1207.19
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 6339

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        894700 kB
Buffers:         33444 kB
Cached:          75680 kB
SwapCached:        492 kB
Active:          58836 kB
Inactive:        52824 kB
HighTotal:      131008 kB
HighFree:        53088 kB
LowTotal:       903652 kB
LowFree:        841612 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5892 kB
Slab:            22432 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 06:03:20 (client local time) WITH STATUS 0 IN 1207.87 SECONDS
stats: 3501 7 1207.87 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/12422/stat): 12422 (minisat+_script) R 12421 12422 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797866829 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12422/statm): 174 3 169 147 0 27 0
[pid=12422] 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=12423
New process pid=12424
New process pid=12425
execve syscall for /bin/sed executable
One traced child (pid=12424) 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=12425) exited with status: 0
One traced child (pid=12423) exited with status: 0
New process pid=12426
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-sp98ar.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.96 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 13394 0 0 0 894 56 0 0 25 0 1 0 1797866834 49704960 9553 4294967295 134512640 135094434 3221224432 3221222288 134784962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12426/statm): 12135 9553 145 145 0 11990 0
[pid=12426] vsize: 48540
Current children cumulated CPU time (s) 9.5
Current children cumulated vsize (Kb) 50664

[startup+20.0061 s]
Raw data (loadavg): 0.94 0.96 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 31816 0 0 0 1792 117 0 0 21 0 1 0 1797866834 113508352 25076 4294967295 134512640 135094434 3221224432 3220841168 134521800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12426/statm): 27712 25076 145 145 0 27567 0
[pid=12426] vsize: 110848
Current children cumulated CPU time (s) 19.09
Current children cumulated vsize (Kb) 112972

[startup+30.007 s]
Raw data (loadavg): 0.95 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 58082 0 0 0 2566 222 0 0 25 0 1 0 1797866834 249638912 51342 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12426/statm): 60947 51342 145 145 0 60802 0
[pid=12426] vsize: 243788
Current children cumulated CPU time (s) 27.88
Current children cumulated vsize (Kb) 245912

[startup+40.0088 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 59374 0 0 0 3550 228 0 0 25 0 1 0 1797866834 254930944 52634 4294967295 134512640 135094434 3221224432 3221223044 134563157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 62239 52634 145 145 0 62094 0
[pid=12426] vsize: 248956
Current children cumulated CPU time (s) 37.78
Current children cumulated vsize (Kb) 251080

[startup+50.0097 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 59777 0 0 0 4545 231 0 0 25 0 1 0 1797866834 256581632 53037 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 62642 53037 145 145 0 62497 0
[pid=12426] vsize: 250568
Current children cumulated CPU time (s) 47.76
Current children cumulated vsize (Kb) 252692

[startup+60.0105 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60040 0 0 0 5542 232 0 0 25 0 1 0 1797866834 257658880 53300 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 62905 53300 145 145 0 62760 0
[pid=12426] vsize: 251620
Current children cumulated CPU time (s) 57.74
Current children cumulated vsize (Kb) 253744

[startup+70.0114 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60128 0 0 0 6541 233 0 0 25 0 1 0 1797866834 258019328 53388 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 62993 53388 145 145 0 62848 0
[pid=12426] vsize: 251972
Current children cumulated CPU time (s) 67.74
Current children cumulated vsize (Kb) 254096

[startup+80.0123 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60307 0 0 0 7539 234 0 0 25 0 1 0 1797866834 258867200 53567 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63200 53567 145 145 0 63055 0
[pid=12426] vsize: 252800
Current children cumulated CPU time (s) 77.73
Current children cumulated vsize (Kb) 254924

[startup+90.0131 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60450 0 0 0 8536 235 0 0 25 0 1 0 1797866834 259448832 53710 4294967295 134512640 135094434 3221224432 3221223108 134553436 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63342 53710 145 145 0 63197 0
[pid=12426] vsize: 253368
Current children cumulated CPU time (s) 87.71
Current children cumulated vsize (Kb) 255492

[startup+100.014 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60517 0 0 0 9535 236 0 0 25 0 1 0 1797866834 259719168 53777 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63408 53777 145 145 0 63263 0
[pid=12426] vsize: 253632
Current children cumulated CPU time (s) 97.71
Current children cumulated vsize (Kb) 255756

[startup+110.016 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60691 0 0 0 10532 237 0 0 25 0 1 0 1797866834 260444160 53951 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63585 53951 145 145 0 63440 0
[pid=12426] vsize: 254340
Current children cumulated CPU time (s) 107.69
Current children cumulated vsize (Kb) 256464

[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60727 0 0 0 11532 237 0 0 25 0 1 0 1797866834 260587520 53987 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63620 53987 145 145 0 63475 0
[pid=12426] vsize: 254480
Current children cumulated CPU time (s) 117.69
Current children cumulated vsize (Kb) 256604

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60782 0 0 0 12531 237 0 0 25 0 1 0 1797866834 260812800 54042 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63675 54042 145 145 0 63530 0
[pid=12426] vsize: 254700
Current children cumulated CPU time (s) 127.68
Current children cumulated vsize (Kb) 256824

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 60944 0 0 0 13530 238 0 0 25 0 1 0 1797866834 261423104 54204 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63824 54204 145 145 0 63679 0
[pid=12426] vsize: 255296
Current children cumulated CPU time (s) 137.68
Current children cumulated vsize (Kb) 257420

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61086 0 0 0 14529 239 0 0 25 0 1 0 1797866834 261939200 54346 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 63950 54346 145 145 0 63805 0
[pid=12426] vsize: 255800
Current children cumulated CPU time (s) 147.68
Current children cumulated vsize (Kb) 257924

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61234 0 0 0 15528 239 0 0 25 0 1 0 1797866834 262250496 54494 4294967295 134512640 135094434 3221224432 3221223136 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64026 54494 145 145 0 63881 0
[pid=12426] vsize: 256104
Current children cumulated CPU time (s) 157.67
Current children cumulated vsize (Kb) 258228

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61389 0 0 0 16527 240 0 0 25 0 1 0 1797866834 263057408 54649 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64223 54649 145 145 0 64078 0
[pid=12426] vsize: 256892
Current children cumulated CPU time (s) 167.67
Current children cumulated vsize (Kb) 259016

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61502 0 0 0 17524 241 0 0 25 0 1 0 1797866834 263467008 54762 4294967295 134512640 135094434 3221224432 3221223088 134561500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12426/statm): 64323 54762 145 145 0 64178 0
[pid=12426] vsize: 257292
Current children cumulated CPU time (s) 177.65
Current children cumulated vsize (Kb) 259416

[startup+190.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61515 0 0 0 18524 241 0 0 25 0 1 0 1797866834 263507968 54775 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64333 54775 145 145 0 64188 0
[pid=12426] vsize: 257332
Current children cumulated CPU time (s) 187.65
Current children cumulated vsize (Kb) 259456

[startup+200.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61532 0 0 0 19524 241 0 0 25 0 1 0 1797866834 263573504 54792 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64349 54792 145 145 0 64204 0
[pid=12426] vsize: 257396
Current children cumulated CPU time (s) 197.65
Current children cumulated vsize (Kb) 259520

[startup+210.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61554 0 0 0 20523 241 0 0 25 0 1 0 1797866834 263663616 54814 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64371 54814 145 145 0 64226 0
[pid=12426] vsize: 257484
Current children cumulated CPU time (s) 207.64
Current children cumulated vsize (Kb) 259608

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61572 0 0 0 21523 241 0 0 25 0 1 0 1797866834 263733248 54832 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64388 54832 145 145 0 64243 0
[pid=12426] vsize: 257552
Current children cumulated CPU time (s) 217.64
Current children cumulated vsize (Kb) 259676

[startup+230.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61602 0 0 0 22523 241 0 0 25 0 1 0 1797866834 263852032 54862 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64417 54862 145 145 0 64272 0
[pid=12426] vsize: 257668
Current children cumulated CPU time (s) 227.64
Current children cumulated vsize (Kb) 259792

[startup+240.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61645 0 0 0 23523 241 0 0 25 0 1 0 1797866834 263974912 54905 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64447 54905 145 145 0 64302 0
[pid=12426] vsize: 257788
Current children cumulated CPU time (s) 237.64
Current children cumulated vsize (Kb) 259912

[startup+250.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61673 0 0 0 24522 242 0 0 25 0 1 0 1797866834 264060928 54933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64468 54933 145 145 0 64323 0
[pid=12426] vsize: 257872
Current children cumulated CPU time (s) 247.64
Current children cumulated vsize (Kb) 259996

[startup+260.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) T 12422 12422 8263 0 -1 0 61687 0 0 0 25522 242 0 0 25 0 1 0 1797866834 264118272 54947 4294967295 134512640 135094434 3221224432 3221222844 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64482 54947 145 145 0 64337 0
[pid=12426] vsize: 257928
Current children cumulated CPU time (s) 257.64
Current children cumulated vsize (Kb) 260052

[startup+270.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61739 0 0 0 26522 242 0 0 25 0 1 0 1797866834 264327168 54999 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64533 54999 145 145 0 64388 0
[pid=12426] vsize: 258132
Current children cumulated CPU time (s) 267.64
Current children cumulated vsize (Kb) 260256

[startup+280.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61765 0 0 0 27522 242 0 0 25 0 1 0 1797866834 264429568 55025 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64558 55025 145 145 0 64413 0
[pid=12426] vsize: 258232
Current children cumulated CPU time (s) 277.64
Current children cumulated vsize (Kb) 260356

[startup+290.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61774 0 0 0 28522 242 0 0 25 0 1 0 1797866834 264466432 55034 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64567 55034 145 145 0 64422 0
[pid=12426] vsize: 258268
Current children cumulated CPU time (s) 287.64
Current children cumulated vsize (Kb) 260392

[startup+300.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61831 0 0 0 29521 243 0 0 25 0 1 0 1797866834 264564736 55091 4294967295 134512640 135094434 3221224432 3221223092 134553512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64591 55091 145 145 0 64446 0
[pid=12426] vsize: 258364
Current children cumulated CPU time (s) 297.64
Current children cumulated vsize (Kb) 260488

[startup+310.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61845 0 0 0 30522 243 0 0 25 0 1 0 1797866834 264617984 55105 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64604 55105 145 145 0 64459 0
[pid=12426] vsize: 258416
Current children cumulated CPU time (s) 307.65
Current children cumulated vsize (Kb) 260540

[startup+320.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61866 0 0 0 31522 243 0 0 25 0 1 0 1797866834 264699904 55126 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64624 55126 145 145 0 64479 0
[pid=12426] vsize: 258496
Current children cumulated CPU time (s) 317.65
Current children cumulated vsize (Kb) 260620

[startup+330.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61878 0 0 0 32520 243 0 0 25 0 1 0 1797866834 264749056 55138 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12426/statm): 64636 55138 145 145 0 64491 0
[pid=12426] vsize: 258544
Current children cumulated CPU time (s) 327.63
Current children cumulated vsize (Kb) 260668

[startup+340.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61890 0 0 0 33520 244 0 0 25 0 1 0 1797866834 264794112 55150 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64647 55150 145 145 0 64502 0
[pid=12426] vsize: 258588
Current children cumulated CPU time (s) 337.64
Current children cumulated vsize (Kb) 260712

[startup+350.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61903 0 0 0 34519 244 0 0 25 0 1 0 1797866834 264847360 55163 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64660 55163 145 145 0 64515 0
[pid=12426] vsize: 258640
Current children cumulated CPU time (s) 347.63
Current children cumulated vsize (Kb) 260764

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61912 0 0 0 35520 244 0 0 25 0 1 0 1797866834 264880128 55172 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64668 55172 145 145 0 64523 0
[pid=12426] vsize: 258672
Current children cumulated CPU time (s) 357.64
Current children cumulated vsize (Kb) 260796

[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61914 0 0 0 36520 244 0 0 25 0 1 0 1797866834 264888320 55174 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64670 55174 145 145 0 64525 0
[pid=12426] vsize: 258680
Current children cumulated CPU time (s) 367.64
Current children cumulated vsize (Kb) 260804

[startup+380.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61920 0 0 0 37520 244 0 0 25 0 1 0 1797866834 264912896 55180 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64676 55180 145 145 0 64531 0
[pid=12426] vsize: 258704
Current children cumulated CPU time (s) 377.64
Current children cumulated vsize (Kb) 260828

[startup+390.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61985 0 0 0 38520 245 0 0 25 0 1 0 1797866834 264974336 55245 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64691 55245 145 145 0 64546 0
[pid=12426] vsize: 258764
Current children cumulated CPU time (s) 387.65
Current children cumulated vsize (Kb) 260888

[startup+400.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61988 0 0 0 39520 245 0 0 25 0 1 0 1797866834 264986624 55248 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64694 55248 145 145 0 64549 0
[pid=12426] vsize: 258776
Current children cumulated CPU time (s) 397.65
Current children cumulated vsize (Kb) 260900

[startup+410.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 61998 0 0 0 40520 245 0 0 25 0 1 0 1797866834 265023488 55258 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64703 55258 145 145 0 64558 0
[pid=12426] vsize: 258812
Current children cumulated CPU time (s) 407.65
Current children cumulated vsize (Kb) 260936

[startup+420.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62003 0 0 0 41520 245 0 0 25 0 1 0 1797866834 265043968 55263 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64708 55263 145 145 0 64563 0
[pid=12426] vsize: 258832
Current children cumulated CPU time (s) 417.65
Current children cumulated vsize (Kb) 260956

[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62015 0 0 0 42520 245 0 0 25 0 1 0 1797866834 265089024 55275 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64719 55275 145 145 0 64574 0
[pid=12426] vsize: 258876
Current children cumulated CPU time (s) 427.65
Current children cumulated vsize (Kb) 261000

[startup+440.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62036 0 0 0 43520 245 0 0 25 0 1 0 1797866834 265170944 55296 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64739 55296 145 145 0 64594 0
[pid=12426] vsize: 258956
Current children cumulated CPU time (s) 437.65
Current children cumulated vsize (Kb) 261080

[startup+450.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62043 0 0 0 44520 245 0 0 25 0 1 0 1797866834 265199616 55303 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64746 55303 145 145 0 64601 0
[pid=12426] vsize: 258984
Current children cumulated CPU time (s) 447.65
Current children cumulated vsize (Kb) 261108

[startup+460.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62117 0 0 0 45520 245 0 0 25 0 1 0 1797866834 265494528 55377 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64818 55377 145 145 0 64673 0
[pid=12426] vsize: 259272
Current children cumulated CPU time (s) 457.65
Current children cumulated vsize (Kb) 261396

[startup+470.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62117 0 0 0 46520 245 0 0 25 0 1 0 1797866834 265494528 55377 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64818 55377 145 145 0 64673 0
[pid=12426] vsize: 259272
Current children cumulated CPU time (s) 467.65
Current children cumulated vsize (Kb) 261396

[startup+480.056 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62118 0 0 0 47520 245 0 0 25 0 1 0 1797866834 265494528 55378 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64818 55378 145 145 0 64673 0
[pid=12426] vsize: 259272
Current children cumulated CPU time (s) 477.65
Current children cumulated vsize (Kb) 261396

[startup+490.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62137 0 0 0 48521 245 0 0 25 0 1 0 1797866834 265555968 55397 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64833 55397 145 145 0 64688 0
[pid=12426] vsize: 259332
Current children cumulated CPU time (s) 487.66
Current children cumulated vsize (Kb) 261456

[startup+500.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62153 0 0 0 49520 246 0 0 25 0 1 0 1797866834 265617408 55413 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64848 55413 145 145 0 64703 0
[pid=12426] vsize: 259392
Current children cumulated CPU time (s) 497.66
Current children cumulated vsize (Kb) 261516

[startup+510.059 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62157 0 0 0 50521 246 0 0 25 0 1 0 1797866834 265633792 55417 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64852 55417 145 145 0 64707 0
[pid=12426] vsize: 259408
Current children cumulated CPU time (s) 507.67
Current children cumulated vsize (Kb) 261532

[startup+520.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62174 0 0 0 51520 246 0 0 25 0 1 0 1797866834 265674752 55434 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64862 55434 145 145 0 64717 0
[pid=12426] vsize: 259448
Current children cumulated CPU time (s) 517.66
Current children cumulated vsize (Kb) 261572

[startup+530.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62177 0 0 0 52521 246 0 0 25 0 1 0 1797866834 265687040 55437 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64865 55437 145 145 0 64720 0
[pid=12426] vsize: 259460
Current children cumulated CPU time (s) 527.67
Current children cumulated vsize (Kb) 261584

[startup+540.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62180 0 0 0 53521 246 0 0 25 0 1 0 1797866834 265695232 55440 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64867 55440 145 145 0 64722 0
[pid=12426] vsize: 259468
Current children cumulated CPU time (s) 537.67
Current children cumulated vsize (Kb) 261592

[startup+550.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62186 0 0 0 54520 246 0 0 25 0 1 0 1797866834 265719808 55446 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12426/statm): 64873 55446 145 145 0 64728 0
[pid=12426] vsize: 259492
Current children cumulated CPU time (s) 547.66
Current children cumulated vsize (Kb) 261616

[startup+560.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62195 0 0 0 55520 246 0 0 25 0 1 0 1797866834 265752576 55455 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64881 55455 145 145 0 64736 0
[pid=12426] vsize: 259524
Current children cumulated CPU time (s) 557.66
Current children cumulated vsize (Kb) 261648

[startup+570.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62209 0 0 0 56520 246 0 0 25 0 1 0 1797866834 265805824 55469 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64894 55469 145 145 0 64749 0
[pid=12426] vsize: 259576
Current children cumulated CPU time (s) 567.66
Current children cumulated vsize (Kb) 261700

[startup+580.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62222 0 0 0 57520 246 0 0 25 0 1 0 1797866834 265854976 55482 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64906 55482 145 145 0 64761 0
[pid=12426] vsize: 259624
Current children cumulated CPU time (s) 577.66
Current children cumulated vsize (Kb) 261748

[startup+590.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62228 0 0 0 58520 246 0 0 25 0 1 0 1797866834 265879552 55488 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64912 55488 145 145 0 64767 0
[pid=12426] vsize: 259648
Current children cumulated CPU time (s) 587.66
Current children cumulated vsize (Kb) 261772

[startup+600.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62237 0 0 0 59520 246 0 0 25 0 1 0 1797866834 265916416 55497 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64921 55497 145 145 0 64776 0
[pid=12426] vsize: 259684
Current children cumulated CPU time (s) 597.66
Current children cumulated vsize (Kb) 261808

[startup+610.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62249 0 0 0 60520 246 0 0 25 0 1 0 1797866834 265961472 55509 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64932 55509 145 145 0 64787 0
[pid=12426] vsize: 259728
Current children cumulated CPU time (s) 607.66
Current children cumulated vsize (Kb) 261852

[startup+620.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62263 0 0 0 61520 247 0 0 25 0 1 0 1797866834 266014720 55523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64945 55523 145 145 0 64800 0
[pid=12426] vsize: 259780
Current children cumulated CPU time (s) 617.67
Current children cumulated vsize (Kb) 261904

[startup+630.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62269 0 0 0 62520 247 0 0 25 0 1 0 1797866834 266039296 55529 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64951 55529 145 145 0 64806 0
[pid=12426] vsize: 259804
Current children cumulated CPU time (s) 627.67
Current children cumulated vsize (Kb) 261928

[startup+640.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62274 0 0 0 63521 247 0 0 25 0 1 0 1797866834 266059776 55534 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64956 55534 145 145 0 64811 0
[pid=12426] vsize: 259824
Current children cumulated CPU time (s) 637.68
Current children cumulated vsize (Kb) 261948

[startup+650.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62283 0 0 0 64521 247 0 0 25 0 1 0 1797866834 266092544 55543 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64964 55543 145 145 0 64819 0
[pid=12426] vsize: 259856
Current children cumulated CPU time (s) 647.68
Current children cumulated vsize (Kb) 261980

[startup+660.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62292 0 0 0 65521 247 0 0 25 0 1 0 1797866834 266129408 55552 4294967295 134512640 135094434 3221224432 3221223088 134557829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64973 55552 145 145 0 64828 0
[pid=12426] vsize: 259892
Current children cumulated CPU time (s) 657.68
Current children cumulated vsize (Kb) 262016

[startup+670.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62303 0 0 0 66521 247 0 0 25 0 1 0 1797866834 266170368 55563 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64983 55563 145 145 0 64838 0
[pid=12426] vsize: 259932
Current children cumulated CPU time (s) 667.68
Current children cumulated vsize (Kb) 262056

[startup+680.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62312 0 0 0 67521 247 0 0 25 0 1 0 1797866834 266207232 55572 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 64992 55572 145 145 0 64847 0
[pid=12426] vsize: 259968
Current children cumulated CPU time (s) 677.68
Current children cumulated vsize (Kb) 262092

[startup+690.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62326 0 0 0 68521 247 0 0 25 0 1 0 1797866834 266260480 55586 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65005 55586 145 145 0 64860 0
[pid=12426] vsize: 260020
Current children cumulated CPU time (s) 687.68
Current children cumulated vsize (Kb) 262144

[startup+700.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62339 0 0 0 69521 247 0 0 25 0 1 0 1797866834 266309632 55599 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65017 55599 145 145 0 64872 0
[pid=12426] vsize: 260068
Current children cumulated CPU time (s) 697.68
Current children cumulated vsize (Kb) 262192

[startup+710.081 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62346 0 0 0 70521 247 0 0 25 0 1 0 1797866834 266338304 55606 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65024 55606 145 145 0 64879 0
[pid=12426] vsize: 260096
Current children cumulated CPU time (s) 707.68
Current children cumulated vsize (Kb) 262220

[startup+720.082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62358 0 0 0 71521 247 0 0 25 0 1 0 1797866834 266383360 55618 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65035 55618 145 145 0 64890 0
[pid=12426] vsize: 260140
Current children cumulated CPU time (s) 717.68
Current children cumulated vsize (Kb) 262264

[startup+730.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62370 0 0 0 72521 247 0 0 25 0 1 0 1797866834 266428416 55630 4294967295 134512640 135094434 3221224432 3221223092 134553512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65046 55630 145 145 0 64901 0
[pid=12426] vsize: 260184
Current children cumulated CPU time (s) 727.68
Current children cumulated vsize (Kb) 262308

[startup+740.085 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62385 0 0 0 73521 248 0 0 25 0 1 0 1797866834 266489856 55645 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65061 55645 145 145 0 64916 0
[pid=12426] vsize: 260244
Current children cumulated CPU time (s) 737.69
Current children cumulated vsize (Kb) 262368

[startup+750.086 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62392 0 0 0 74521 248 0 0 25 0 1 0 1797866834 266514432 55652 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65067 55652 145 145 0 64922 0
[pid=12426] vsize: 260268
Current children cumulated CPU time (s) 747.69
Current children cumulated vsize (Kb) 262392

[startup+760.087 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62399 0 0 0 75522 248 0 0 25 0 1 0 1797866834 266543104 55659 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65074 55659 145 145 0 64929 0
[pid=12426] vsize: 260296
Current children cumulated CPU time (s) 757.7
Current children cumulated vsize (Kb) 262420

[startup+770.087 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62406 0 0 0 76522 248 0 0 25 0 1 0 1797866834 266571776 55666 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65081 55666 145 145 0 64936 0
[pid=12426] vsize: 260324
Current children cumulated CPU time (s) 767.7
Current children cumulated vsize (Kb) 262448

[startup+780.088 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62410 0 0 0 77522 248 0 0 25 0 1 0 1797866834 266584064 55670 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65084 55670 145 145 0 64939 0
[pid=12426] vsize: 260336
Current children cumulated CPU time (s) 777.7
Current children cumulated vsize (Kb) 262460

[startup+790.089 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62423 0 0 0 78522 248 0 0 25 0 1 0 1797866834 266608640 55683 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65090 55683 145 145 0 64945 0
[pid=12426] vsize: 260360
Current children cumulated CPU time (s) 787.7
Current children cumulated vsize (Kb) 262484

[startup+800.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62431 0 0 0 79522 248 0 0 25 0 1 0 1797866834 266641408 55691 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65098 55691 145 145 0 64953 0
[pid=12426] vsize: 260392
Current children cumulated CPU time (s) 797.7
Current children cumulated vsize (Kb) 262516

[startup+810.092 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62438 0 0 0 80522 248 0 0 25 0 1 0 1797866834 266665984 55698 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65104 55698 145 145 0 64959 0
[pid=12426] vsize: 260416
Current children cumulated CPU time (s) 807.7
Current children cumulated vsize (Kb) 262540

[startup+820.093 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62471 0 0 0 81522 248 0 0 25 0 1 0 1797866834 266690560 55731 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65110 55731 145 145 0 64965 0
[pid=12426] vsize: 260440
Current children cumulated CPU time (s) 817.7
Current children cumulated vsize (Kb) 262564

[startup+830.093 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62489 0 0 0 82522 248 0 0 25 0 1 0 1797866834 266760192 55749 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65127 55749 145 145 0 64982 0
[pid=12426] vsize: 260508
Current children cumulated CPU time (s) 827.7
Current children cumulated vsize (Kb) 262632

[startup+840.094 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62496 0 0 0 83523 248 0 0 25 0 1 0 1797866834 266788864 55756 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65134 55756 145 145 0 64989 0
[pid=12426] vsize: 260536
Current children cumulated CPU time (s) 837.71
Current children cumulated vsize (Kb) 262660

[startup+850.095 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62507 0 0 0 84523 248 0 0 25 0 1 0 1797866834 266829824 55767 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65144 55767 145 145 0 64999 0
[pid=12426] vsize: 260576
Current children cumulated CPU time (s) 847.71
Current children cumulated vsize (Kb) 262700

[startup+860.096 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62517 0 0 0 85523 248 0 0 25 0 1 0 1797866834 266858496 55777 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65151 55777 145 145 0 65006 0
[pid=12426] vsize: 260604
Current children cumulated CPU time (s) 857.71
Current children cumulated vsize (Kb) 262728

[startup+870.097 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62524 0 0 0 86523 248 0 0 25 0 1 0 1797866834 266883072 55784 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65157 55784 145 145 0 65012 0
[pid=12426] vsize: 260628
Current children cumulated CPU time (s) 867.71
Current children cumulated vsize (Kb) 262752

[startup+880.098 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62532 0 0 0 87523 249 0 0 25 0 1 0 1797866834 266915840 55792 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65165 55792 145 145 0 65020 0
[pid=12426] vsize: 260660
Current children cumulated CPU time (s) 877.72
Current children cumulated vsize (Kb) 262784

[startup+890.098 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62542 0 0 0 88523 249 0 0 25 0 1 0 1797866834 266936320 55802 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65170 55802 145 145 0 65025 0
[pid=12426] vsize: 260680
Current children cumulated CPU time (s) 887.72
Current children cumulated vsize (Kb) 262804

[startup+900.099 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62554 0 0 0 89523 249 0 0 25 0 1 0 1797866834 266981376 55814 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65181 55814 145 145 0 65036 0
[pid=12426] vsize: 260724
Current children cumulated CPU time (s) 897.72
Current children cumulated vsize (Kb) 262848

[startup+910.101 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62559 0 0 0 90522 249 0 0 25 0 1 0 1797866834 267001856 55819 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65186 55819 145 145 0 65041 0
[pid=12426] vsize: 260744
Current children cumulated CPU time (s) 907.71
Current children cumulated vsize (Kb) 262868

[startup+920.102 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62573 0 0 0 91522 250 0 0 25 0 1 0 1797866834 267055104 55833 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65199 55833 145 145 0 65054 0
[pid=12426] vsize: 260796
Current children cumulated CPU time (s) 917.72
Current children cumulated vsize (Kb) 262920

[startup+930.103 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62582 0 0 0 92522 250 0 0 25 0 1 0 1797866834 267091968 55842 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65208 55842 145 145 0 65063 0
[pid=12426] vsize: 260832
Current children cumulated CPU time (s) 927.72
Current children cumulated vsize (Kb) 262956

[startup+940.104 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62593 0 0 0 93522 250 0 0 25 0 1 0 1797866834 267132928 55853 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65218 55853 145 145 0 65073 0
[pid=12426] vsize: 260872
Current children cumulated CPU time (s) 937.72
Current children cumulated vsize (Kb) 262996

[startup+950.105 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62606 0 0 0 94522 250 0 0 25 0 1 0 1797866834 267182080 55866 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65230 55866 145 145 0 65085 0
[pid=12426] vsize: 260920
Current children cumulated CPU time (s) 947.72
Current children cumulated vsize (Kb) 263044

[startup+960.106 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62627 0 0 0 95522 250 0 0 25 0 1 0 1797866834 267247616 55887 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65246 55887 145 145 0 65101 0
[pid=12426] vsize: 260984
Current children cumulated CPU time (s) 957.72
Current children cumulated vsize (Kb) 263108

[startup+970.107 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62646 0 0 0 96522 250 0 0 25 0 1 0 1797866834 267321344 55906 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65264 55906 145 145 0 65119 0
[pid=12426] vsize: 261056
Current children cumulated CPU time (s) 967.72
Current children cumulated vsize (Kb) 263180

[startup+980.108 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62655 0 0 0 97522 250 0 0 25 0 1 0 1797866834 267354112 55915 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65272 55915 145 145 0 65127 0
[pid=12426] vsize: 261088
Current children cumulated CPU time (s) 977.72
Current children cumulated vsize (Kb) 263212

[startup+990.109 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62678 0 0 0 98522 250 0 0 25 0 1 0 1797866834 267390976 55938 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65281 55938 145 145 0 65136 0
[pid=12426] vsize: 261124
Current children cumulated CPU time (s) 987.72
Current children cumulated vsize (Kb) 263248

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62688 0 0 0 99522 250 0 0 25 0 1 0 1797866834 267427840 55948 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65290 55948 145 145 0 65145 0
[pid=12426] vsize: 261160
Current children cumulated CPU time (s) 997.72
Current children cumulated vsize (Kb) 263284

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62702 0 0 0 100522 251 0 0 25 0 1 0 1797866834 267481088 55962 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65303 55962 145 145 0 65158 0
[pid=12426] vsize: 261212
Current children cumulated CPU time (s) 1007.73
Current children cumulated vsize (Kb) 263336

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62713 0 0 0 101522 251 0 0 25 0 1 0 1797866834 267526144 55973 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65314 55973 145 145 0 65169 0
[pid=12426] vsize: 261256
Current children cumulated CPU time (s) 1017.73
Current children cumulated vsize (Kb) 263380

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62726 0 0 0 102522 251 0 0 25 0 1 0 1797866834 267575296 55986 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65326 55986 145 145 0 65181 0
[pid=12426] vsize: 261304
Current children cumulated CPU time (s) 1027.73
Current children cumulated vsize (Kb) 263428

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62732 0 0 0 103522 251 0 0 25 0 1 0 1797866834 267599872 55992 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65332 55992 145 145 0 65187 0
[pid=12426] vsize: 261328
Current children cumulated CPU time (s) 1037.73
Current children cumulated vsize (Kb) 263452

[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62735 0 0 0 104522 251 0 0 25 0 1 0 1797866834 267612160 55995 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65335 55995 145 145 0 65190 0
[pid=12426] vsize: 261340
Current children cumulated CPU time (s) 1047.73
Current children cumulated vsize (Kb) 263464

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62744 0 0 0 105523 251 0 0 25 0 1 0 1797866834 267644928 56004 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65343 56004 145 145 0 65198 0
[pid=12426] vsize: 261372
Current children cumulated CPU time (s) 1057.74
Current children cumulated vsize (Kb) 263496

[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62755 0 0 0 106523 251 0 0 25 0 1 0 1797866834 267948032 56015 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65417 56015 145 145 0 65272 0
[pid=12426] vsize: 261668
Current children cumulated CPU time (s) 1067.74
Current children cumulated vsize (Kb) 263792

[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62763 0 0 0 107523 251 0 0 25 0 1 0 1797866834 267980800 56023 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65425 56023 145 145 0 65280 0
[pid=12426] vsize: 261700
Current children cumulated CPU time (s) 1077.74
Current children cumulated vsize (Kb) 263824

[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62775 0 0 0 108523 251 0 0 25 0 1 0 1797866834 268025856 56035 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65436 56035 145 145 0 65291 0
[pid=12426] vsize: 261744
Current children cumulated CPU time (s) 1087.74
Current children cumulated vsize (Kb) 263868

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62786 0 0 0 109523 251 0 0 25 0 1 0 1797866834 268070912 56046 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65447 56046 145 145 0 65302 0
[pid=12426] vsize: 261788
Current children cumulated CPU time (s) 1097.74
Current children cumulated vsize (Kb) 263912

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62799 0 0 0 110523 251 0 0 25 0 1 0 1797866834 268120064 56059 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65459 56059 145 145 0 65314 0
[pid=12426] vsize: 261836
Current children cumulated CPU time (s) 1107.74
Current children cumulated vsize (Kb) 263960

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62838 0 0 0 111523 251 0 0 25 0 1 0 1797866834 268271616 56098 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65496 56098 145 145 0 65351 0
[pid=12426] vsize: 261984
Current children cumulated CPU time (s) 1117.74
Current children cumulated vsize (Kb) 264108

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62861 0 0 0 112523 252 0 0 25 0 1 0 1797866834 268361728 56121 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65518 56121 145 145 0 65373 0
[pid=12426] vsize: 262072
Current children cumulated CPU time (s) 1127.75
Current children cumulated vsize (Kb) 264196

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62879 0 0 0 113522 252 0 0 25 0 1 0 1797866834 268431360 56139 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65535 56139 145 145 0 65390 0
[pid=12426] vsize: 262140
Current children cumulated CPU time (s) 1137.74
Current children cumulated vsize (Kb) 264264

[startup+1150.13 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62892 0 0 0 114523 252 0 0 25 0 1 0 1797866834 268484608 56152 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65548 56152 145 145 0 65403 0
[pid=12426] vsize: 262192
Current children cumulated CPU time (s) 1147.75
Current children cumulated vsize (Kb) 264316

[startup+1160.13 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62917 0 0 0 115522 252 0 0 25 0 1 0 1797866834 268578816 56177 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65571 56177 145 145 0 65426 0
[pid=12426] vsize: 262284
Current children cumulated CPU time (s) 1157.74
Current children cumulated vsize (Kb) 264408

[startup+1170.13 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62932 0 0 0 116522 252 0 0 25 0 1 0 1797866834 268640256 56192 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65586 56192 145 145 0 65441 0
[pid=12426] vsize: 262344
Current children cumulated CPU time (s) 1167.74
Current children cumulated vsize (Kb) 264468

[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62951 0 0 0 117522 252 0 0 25 0 1 0 1797866834 268713984 56211 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65604 56211 145 145 0 65459 0
[pid=12426] vsize: 262416
Current children cumulated CPU time (s) 1177.74
Current children cumulated vsize (Kb) 264540

[startup+1190.13 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62974 0 0 0 118522 252 0 0 25 0 1 0 1797866834 268804096 56234 4294967295 134512640 135094434 3221224432 3221223088 134558435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65626 56234 145 145 0 65481 0
[pid=12426] vsize: 262504
Current children cumulated CPU time (s) 1187.74
Current children cumulated vsize (Kb) 264628

[startup+1200.13 s]
Raw data (loadavg): 1.15 1.00 0.95 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62984 0 0 0 119523 252 0 0 25 0 1 0 1797866834 268840960 56244 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65635 56244 145 145 0 65490 0
[pid=12426] vsize: 262540
Current children cumulated CPU time (s) 1197.75
Current children cumulated vsize (Kb) 264664

[startup+1210.13 s]
Raw data (loadavg): 1.12 1.00 0.95 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62990 0 0 0 120523 252 0 0 25 0 1 0 1797866834 268857344 56250 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65639 56250 145 145 0 65494 0
[pid=12426] vsize: 262556
Current children cumulated CPU time (s) 1207.75
Current children cumulated vsize (Kb) 264680



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 1.12 1.00 0.95 2/57 12426
Raw data (/proc/12422/stat): 12422 (minisat+_script) S 12421 12422 8263 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797866829 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12422/statm): 531 226 485 147 0 384 0
[pid=12422] vsize: 2124
Raw data (/proc/12426/stat): 12426 (minisat+_64-bit) R 12422 12422 8263 0 -1 0 62990 0 0 0 120523 252 0 0 25 0 1 0 1797866834 268857344 56250 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12426/statm): 65639 56250 145 145 0 65494 0
[pid=12426] vsize: 262556
Current children cumulated CPU time (s) 1207.75
Current children cumulated vsize (Kb) 264680

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

Child status: 0
Real time (s): 1210.25
CPU time (s): 1207.87
CPU user time (s): 1205.24
CPU system time (s): 2.6376
CPU usage (%): 99.804
Max. virtual memory (cumulated for all children) (Kb): 264680

Verifier Data

ERROR: no interpretation found !