Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-fit1p.opb
MD5SUM0417a8bac185d4a033d4915882b274ef
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 30780
Biggest coefficient in the objective function 1610612736
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 1591285381686
Number of bits of the sum of numbers in the objective function 41
Biggest number in a constraint 59431609958400
Number of bits of the biggest number in a constraint 46
Biggest sum of numbers in a constraint 209844586667159
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables45485
Total number of constraints1026
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1026
Minimum length of a constraint17
Maximum length of a constraint619

Trace number 2630

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        908568 kB
Buffers:         30708 kB
Cached:          68684 kB
SwapCached:       1044 kB
Active:          59540 kB
Inactive:        42552 kB
HighTotal:      131008 kB
HighFree:        58744 kB
LowTotal:       903652 kB
LowFree:        849824 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            18048 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:35:54 (client local time) WITH STATUS 0 IN 1208.49 SECONDS
stats: 2773 7 1208.49 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 2187] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1653 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1714]---> BDD-cost:   18
c ---[1713]---> BDD-cost:   17
c ---[1712]---> BDD-cost:   17
c ---[1710]---> BDD-cost:   17
c ---[1709]---> BDD-cost:   18
c ---[1708]---> BDD-cost:   16
c ---[1707]---> BDD-cost:   16
c ---[1706]---> BDD-cost:   17
c ---[1705]---> BDD-cost:   17
c ---[1703]---> BDD-cost:   16
c ---[1702]---> BDD-cost:   17
c ---[1701]---> BDD-cost:   17
c ---[1700]---> BDD-cost:   16
c ---[1699]---> BDD-cost:   16
c ---[1698]---> BDD-cost:   17
c ---[1697]---> BDD-cost:   17
c ---[1695]---> BDD-cost:   16
c ---[1694]---> BDD-cost:   16
c ---[1693]---> BDD-cost:   18
c ---[1691]---> BDD-cost:   16
c ---[1690]---> BDD-cost:   18
c ---[1689]---> BDD-cost:   18
c ---[1688]---> BDD-cost:   17
c ---[1687]---> BDD-cost:   17
c ---[1686]---> BDD-cost:   16
c ---[1685]---> BDD-cost:   18
c ---[1683]---> BDD-cost:   17
c ---[1681]---> BDD-cost:   18
c ---[1680]---> BDD-cost:   17
c ---[1679]---> BDD-cost:   17
c ---[1678]---> BDD-cost:   18
c ---[1677]---> BDD-cost:   16
c ---[1676]---> BDD-cost:   16
c ---[1674]---> BDD-cost:   18
c ---[1673]---> BDD-cost:   16
c ---[1672]---> BDD-cost:   17
c ---[1671]---> BDD-cost:   17
c ---[1670]---> BDD-cost:   16
c ---[1669]---> BDD-cost:   18
c ---[1667]---> BDD-cost:   18
c ---[1666]---> BDD-cost:   17
c ---[1665]---> BDD-cost:   16
c ---[1664]---> BDD-cost:   19
c ---[1663]---> BDD-cost:   19
c ---[1662]---> BDD-cost:   16
c ---[1661]---> BDD-cost:   16
c ---[1660]---> BDD-cost:   18
c ---[1659]---> BDD-cost:   17
c ---[1658]---> BDD-cost:   17
c ---[1657]---> BDD-cost:   16
c ---[1656]---> BDD-cost:   17
c ---[1655]---> BDD-cost:   18
c ---[1652]---> BDD-cost:   16
c ---[1651]---> BDD-cost:   16
c ---[1650]---> BDD-cost:   18
c ---[1649]---> BDD-cost:   16
c ---[1648]---> BDD-cost:   16
c ---[1647]---> BDD-cost:   16
c ---[1646]---> BDD-cost:   18
c ---[1645]---> BDD-cost:   18
c ---[1644]---> BDD-cost:   18
c ---[1641]---> BDD-cost:   16
c ---[1639]---> BDD-cost:   16
c ---[1638]---> BDD-cost:   16
c ---[1636]---> BDD-cost:   17
c ---[1633]---> BDD-cost:   18
c ---[1632]---> BDD-cost:   16
c ---[1631]---> BDD-cost:   16
c ---[1630]---> BDD-cost:   17
c ---[1629]---> BDD-cost:   18
c ---[1628]---> BDD-cost:   17
c ---[1627]---> BDD-cost:   16
c ---[1626]---> BDD-cost:   16
c ---[1625]---> BDD-cost:   18
c ---[1624]---> BDD-cost:   17
c ---[1623]---> BDD-cost:   17
c ---[1622]---> BDD-cost:   18
c ---[1621]---> BDD-cost:   18
c ---[1620]---> BDD-cost:   18
c ---[1619]---> BDD-cost:   16
c ---[1617]---> BDD-cost:   16
c ---[1616]---> BDD-cost:   18
c ---[1615]---> BDD-cost:   16
c ---[1614]---> BDD-cost:   16
c ---[1613]---> BDD-cost:   17
c ---[1612]---> BDD-cost:   17
c ---[1611]---> BDD-cost:   18
c ---[1610]---> BDD-cost:   16
c ---[1609]---> BDD-cost:   18
c ---[1608]---> BDD-cost:   18
c ---[1606]---> BDD-cost:   17
c ---[1605]---> BDD-cost:   18
c ---[1604]---> BDD-cost:   16
c ---[1602]---> BDD-cost:   17
c ---[1601]---> BDD-cost:   18
c ---[1600]---> BDD-cost:   18
c ---[1599]---> BDD-cost:   17
c ---[1597]---> BDD-cost:   18
c ---[1596]---> BDD-cost:   17
c ---[1595]---> BDD-cost:   18
c ---[1594]---> BDD-cost:   17
c ---[1593]---> BDD-cost:   17
c ---[1592]---> BDD-cost:   17
c ---[1590]---> BDD-cost:   16
c ---[1589]---> BDD-cost:   16
c ---[1588]---> BDD-cost:   16
c ---[1587]---> BDD-cost:   16
c ---[1586]---> BDD-cost:   16
c ---[1585]---> BDD-cost:   17
c ---[1584]---> BDD-cost:   18
c ---[1583]---> BDD-cost:   16
c ---[1582]---> BDD-cost:   16
c ---[1581]---> BDD-cost:   16
c ---[1580]---> BDD-cost:   16
c ---[1579]---> BDD-cost:   17
c ---[1577]---> BDD-cost:   16
c ---[1575]---> BDD-cost:   18
c ---[1572]---> BDD-cost:   18
c ---[1571]---> BDD-cost:   18
c ---[1570]---> BDD-cost:   16
c ---[1569]---> BDD-cost:   17
c ---[1568]---> BDD-cost:   17
c ---[1567]---> BDD-cost:   18
c ---[1566]---> BDD-cost:   16
c ---[1564]---> BDD-cost:   16
c ---[1563]---> BDD-cost:   16
c ---[1562]---> BDD-cost:   17
c ---[1559]---> BDD-cost:   17
c ---[1558]---> BDD-cost:   17
c ---[1557]---> BDD-cost:   17
c ---[1555]---> BDD-cost:   17
c ---[1554]---> BDD-cost:   16
c ---[1553]---> BDD-cost:   19
c ---[1552]---> BDD-cost:   16
c ---[1551]---> BDD-cost:   16
c ---[1550]---> BDD-cost:   16
c ---[1549]---> BDD-cost:   18
c ---[1548]---> BDD-cost:   17
c ---[1546]---> BDD-cost:   17
c ---[1545]---> BDD-cost:   18
c ---[1544]---> BDD-cost:   16
c ---[1543]---> BDD-cost:   17
c ---[1542]---> BDD-cost:   17
c ---[1541]---> BDD-cost:   17
c ---[1539]---> BDD-cost:   16
c ---[1538]---> BDD-cost:   16
c ---[1537]---> BDD-cost:   16
c ---[1536]---> BDD-cost:   17
c ---[1534]---> BDD-cost:   17
c ---[1533]---> BDD-cost:   16
c ---[1532]---> BDD-cost:   17
c ---[1531]---> BDD-cost:   17
c ---[1530]---> BDD-cost:   16
c ---[1529]---> BDD-cost:   16
c ---[1528]---> BDD-cost:   16
c ---[1527]---> BDD-cost:   18
c ---[1526]---> BDD-cost:   18
c ---[1525]---> BDD-cost:   17
c ---[1524]---> BDD-cost:   17
c ---[1523]---> BDD-cost:   17
c ---[1522]---> BDD-cost:   16
c ---[1521]---> BDD-cost:   16
c ---[1520]---> BDD-cost:   18
c ---[1519]---> BDD-cost:   17
c ---[1518]---> BDD-cost:   16
c ---[1517]---> BDD-cost:   16
c ---[1514]---> BDD-cost:   17
c ---[1513]---> BDD-cost:   18
c ---[1511]---> BDD-cost:   16
c ---[1510]---> BDD-cost:   18
c ---[1509]---> BDD-cost:   16
c ---[1508]---> BDD-cost:   16
c ---[1507]---> BDD-cost:   16
c ---[1506]---> BDD-cost:   16
c ---[1505]---> BDD-cost:   16
c ---[1504]---> BDD-cost:   17
c ---[1503]---> BDD-cost:   17
c ---[1502]---> BDD-cost:   18
c ---[1501]---> BDD-cost:   18
c ---[1500]---> BDD-cost:   17
c ---[1498]---> BDD-cost:   18
c ---[1497]---> BDD-cost:   16
c ---[1493]---> BDD-cost:   17
c ---[1492]---> BDD-cost:   17
c ---[1491]---> BDD-cost:   17
c ---[1490]---> BDD-cost:   18
c ---[1489]---> BDD-cost:   18
c ---[1488]---> BDD-cost:   16
c ---[1487]---> BDD-cost:   16
c ---[1485]---> BDD-cost:   17
c ---[1484]---> BDD-cost:   16
c ---[1483]---> BDD-cost:   17
c ---[1482]---> BDD-cost:   16
c ---[1481]---> BDD-cost:   18
c ---[1480]---> BDD-cost:   17
c ---[1479]---> BDD-cost:   17
c ---[1478]---> BDD-cost:   17
c ---[1476]---> BDD-cost:   16
c ---[1475]---> BDD-cost:   18
c ---[1473]---> BDD-cost:   18
c ---[1472]---> BDD-cost:   18
c ---[1471]---> BDD-cost:   16
c ---[1470]---> BDD-cost:   17
c ---[1469]---> BDD-cost:   17
c ---[1468]---> BDD-cost:   17
c ---[1466]---> BDD-cost:   16
c ---[1465]---> BDD-cost:   17
c ---[1464]---> BDD-cost:   18
c ---[1463]---> BDD-cost:   16
c ---[1462]---> BDD-cost:   17
c ---[1461]---> BDD-cost:   18
c ---[1460]---> BDD-cost:   16
c ---[1459]---> BDD-cost:   17
c ---[1458]---> BDD-cost:   18
c ---[1456]---> BDD-cost:   19
c ---[1455]---> BDD-cost:   17
c ---[1454]---> BDD-cost:   16
c ---[1453]---> BDD-cost:   16
c ---[1451]---> BDD-cost:   18
c ---[1450]---> BDD-cost:   17
c ---[1448]---> BDD-cost:   16
c ---[1446]---> BDD-cost:   17
c ---[1444]---> BDD-cost:   17
c ---[1443]---> BDD-cost:   17
c ---[1442]---> BDD-cost:   18
c ---[1441]---> BDD-cost:   17
c ---[1440]---> BDD-cost:   16
c ---[1439]---> BDD-cost:   16
c ---[1438]---> BDD-cost:   16
c ---[1437]---> BDD-cost:   17
c ---[1436]---> BDD-cost:   16
c ---[1435]---> BDD-cost:   18
c ---[1434]---> BDD-cost:   16
c ---[1433]---> BDD-cost:   16
c ---[1432]---> BDD-cost:   16
c ---[1431]---> BDD-cost:   17

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/9392/stat): 9392 (minisat+_script) R 9391 9392 30740 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785832734 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/9392/statm): 174 3 169 147 0 27 0
[pid=9392] 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=9393
New process pid=9394
New process pid=9395
execve syscall for /bin/sed executable
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
One traced child (pid=9394) exited with status: 0
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=9395) exited with status: 0
One traced child (pid=9393) exited with status: 0
New process pid=9396
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-fit1p.opb
One traced child (pid=9396) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=9397
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-fit1p.opb

[startup+10.0039 s]
Raw data (loadavg): 0.86 0.92 0.90 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 3724 0 0 0 853 20 0 0 25 0 1 0 1785832838 17055744 3668 4294967295 134512640 135167914 3221224448 3221223016 134846961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 4164 3668 162 162 0 4002 0
[pid=9397] vsize: 16656
Current children cumulated CPU time (s) 9.61
Current children cumulated vsize (Kb) 18784

[startup+20.0057 s]
Raw data (loadavg): 0.88 0.92 0.90 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 6265 0 0 0 1818 36 0 0 25 0 1 0 1785832838 27467776 6209 4294967295 134512640 135167914 3221224448 3221222284 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 6706 6209 162 162 0 6544 0
[pid=9397] vsize: 26824
Current children cumulated CPU time (s) 19.42
Current children cumulated vsize (Kb) 28952

[startup+30.0065 s]
Raw data (loadavg): 0.90 0.92 0.90 1/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) T 9392 9392 30740 0 -1 0 9009 0 0 0 2780 54 0 0 25 0 1 0 1785832838 38154240 8870 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9397/statm): 9315 8870 162 162 0 9153 0
[pid=9397] vsize: 37260
Current children cumulated CPU time (s) 29.22
Current children cumulated vsize (Kb) 39388

[startup+40.0073 s]
Raw data (loadavg): 0.91 0.92 0.90 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 3749 69 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221218748 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 39.06
Current children cumulated vsize (Kb) 48612

[startup+50.009 s]
Raw data (loadavg): 0.93 0.92 0.90 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 4748 69 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221218620 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 49.05
Current children cumulated vsize (Kb) 48612

[startup+60.0088 s]
Raw data (loadavg): 0.94 0.93 0.90 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 5748 70 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221219476 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 59.06
Current children cumulated vsize (Kb) 48612

[startup+70.0106 s]
Raw data (loadavg): 0.95 0.93 0.90 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 6746 71 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221219248 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 69.05
Current children cumulated vsize (Kb) 48612

[startup+80.0114 s]
Raw data (loadavg): 0.95 0.93 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 7746 72 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221219164 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 79.06
Current children cumulated vsize (Kb) 48612

[startup+90.0111 s]
Raw data (loadavg): 0.96 0.93 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 8745 73 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221221416 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 89.06
Current children cumulated vsize (Kb) 48612

[startup+100.012 s]
Raw data (loadavg): 0.97 0.93 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 9745 73 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221220484 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 99.06
Current children cumulated vsize (Kb) 48612

[startup+110.013 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11631 0 0 0 10744 74 0 0 25 0 1 0 1785832838 47599616 11225 4294967295 134512640 135167914 3221224448 3221218736 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9397/statm): 11621 11225 162 162 0 11459 0
[pid=9397] vsize: 46484
Current children cumulated CPU time (s) 109.06
Current children cumulated vsize (Kb) 48612

[startup+120.014 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 11744 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221217580 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 119.06
Current children cumulated vsize (Kb) 48844

[startup+130.015 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 12744 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221219964 134718176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 129.06
Current children cumulated vsize (Kb) 48844

[startup+140.015 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 13744 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221220144 134844720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 139.06
Current children cumulated vsize (Kb) 48844

[startup+150.016 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 14745 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221220112 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 149.07
Current children cumulated vsize (Kb) 48844

[startup+160.017 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 15745 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221219512 134849087 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 159.07
Current children cumulated vsize (Kb) 48844

[startup+170.017 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 16745 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221221408 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 169.07
Current children cumulated vsize (Kb) 48844

[startup+180.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 17745 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221219904 134628744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 179.07
Current children cumulated vsize (Kb) 48844

[startup+190.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 18746 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221221616 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 189.08
Current children cumulated vsize (Kb) 48844

[startup+200.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 19746 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221221236 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 199.08
Current children cumulated vsize (Kb) 48844

[startup+210.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 20746 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221220032 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 209.08
Current children cumulated vsize (Kb) 48844

[startup+220.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 21746 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221219888 134628768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 219.08
Current children cumulated vsize (Kb) 48844

[startup+230.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 11773 0 0 0 22747 74 0 0 25 0 1 0 1785832838 47837184 11284 4294967295 134512640 135167914 3221224448 3221220524 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 11679 11284 162 162 0 11517 0
[pid=9397] vsize: 46716
Current children cumulated CPU time (s) 229.09
Current children cumulated vsize (Kb) 48844

[startup+240.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 23746 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221218736 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 239.09
Current children cumulated vsize (Kb) 51040

[startup+250.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 24747 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221218544 134718501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 249.1
Current children cumulated vsize (Kb) 51040

[startup+260.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 25747 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221219264 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 259.1
Current children cumulated vsize (Kb) 51040

[startup+270.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 26747 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220144 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 269.1
Current children cumulated vsize (Kb) 51040

[startup+280.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 27747 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220584 134693553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 279.1
Current children cumulated vsize (Kb) 51040

[startup+290.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 28747 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220352 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 289.1
Current children cumulated vsize (Kb) 51040

[startup+300.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 29748 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221219344 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 299.11
Current children cumulated vsize (Kb) 51040

[startup+310.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 30748 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220304 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 309.11
Current children cumulated vsize (Kb) 51040

[startup+320.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 31748 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221221472 134630940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 319.11
Current children cumulated vsize (Kb) 51040

[startup+330.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 32749 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221219792 134845890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 329.12
Current children cumulated vsize (Kb) 51040

[startup+340.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 33749 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220752 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 339.12
Current children cumulated vsize (Kb) 51040

[startup+350.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 34749 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220912 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 349.12
Current children cumulated vsize (Kb) 51040

[startup+360.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 35749 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221221912 134693640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 359.12
Current children cumulated vsize (Kb) 51040

[startup+370.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 36750 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221221456 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 369.13
Current children cumulated vsize (Kb) 51040

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 37750 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221222720 134629426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 379.13
Current children cumulated vsize (Kb) 51040

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 38750 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220256 134844731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 389.13
Current children cumulated vsize (Kb) 51040

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12152 0 0 0 39750 75 0 0 25 0 1 0 1785832838 50085888 11663 4294967295 134512640 135167914 3221224448 3221220672 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11663 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 399.13
Current children cumulated vsize (Kb) 51040

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12172 0 0 0 40750 75 0 0 25 0 1 0 1785832838 50085888 11683 4294967295 134512640 135167914 3221224448 3221220224 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11683 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 409.13
Current children cumulated vsize (Kb) 51040

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12172 0 0 0 41751 75 0 0 25 0 1 0 1785832838 50085888 11683 4294967295 134512640 135167914 3221224448 3221221792 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11683 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 419.14
Current children cumulated vsize (Kb) 51040

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12172 0 0 0 42751 75 0 0 25 0 1 0 1785832838 50085888 11683 4294967295 134512640 135167914 3221224448 3221220656 134718181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12228 11683 162 162 0 12066 0
[pid=9397] vsize: 48912
Current children cumulated CPU time (s) 429.14
Current children cumulated vsize (Kb) 51040

[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 43750 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221218720 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 439.14
Current children cumulated vsize (Kb) 51704

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 44750 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221219888 134628817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 449.14
Current children cumulated vsize (Kb) 51704

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 45750 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221218944 134722527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 459.14
Current children cumulated vsize (Kb) 51704

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 46751 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221220556 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 469.15
Current children cumulated vsize (Kb) 51704

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 47751 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221220908 134695248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 479.15
Current children cumulated vsize (Kb) 51704

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 48751 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221219336 134849087 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 489.15
Current children cumulated vsize (Kb) 51704

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 49751 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221219680 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 499.15
Current children cumulated vsize (Kb) 51704

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 50752 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221219184 134629228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 509.16
Current children cumulated vsize (Kb) 51704

[startup+520.043 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 51752 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221221580 134723291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 519.16
Current children cumulated vsize (Kb) 51704

[startup+530.044 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 52752 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221221200 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 529.16
Current children cumulated vsize (Kb) 51704

[startup+540.045 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 53752 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221220320 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 539.16
Current children cumulated vsize (Kb) 51704

[startup+550.046 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 54753 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221220496 134696316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 549.17
Current children cumulated vsize (Kb) 51704

[startup+560.046 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12557 0 0 0 55753 76 0 0 25 0 1 0 1785832838 50765824 11903 4294967295 134512640 135167914 3221224448 3221221856 134844697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11903 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 559.17
Current children cumulated vsize (Kb) 51704

[startup+570.047 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 56753 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221218612 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 569.17
Current children cumulated vsize (Kb) 51704

[startup+580.048 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 57753 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221218428 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 579.17
Current children cumulated vsize (Kb) 51704

[startup+590.049 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 58753 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221218640 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 589.17
Current children cumulated vsize (Kb) 51704

[startup+600.05 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 59754 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219772 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 599.18
Current children cumulated vsize (Kb) 51704

[startup+610.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 60754 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219500 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 609.18
Current children cumulated vsize (Kb) 51704

[startup+620.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 61754 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220496 134696298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 619.18
Current children cumulated vsize (Kb) 51704

[startup+630.052 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 62754 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220176 134849108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 629.18
Current children cumulated vsize (Kb) 51704

[startup+640.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 63755 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219472 134718203 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 639.19
Current children cumulated vsize (Kb) 51704

[startup+650.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 64755 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220864 134696613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 649.19
Current children cumulated vsize (Kb) 51704

[startup+660.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 65755 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219872 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 659.19
Current children cumulated vsize (Kb) 51704

[startup+670.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 66755 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219680 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 669.19
Current children cumulated vsize (Kb) 51704

[startup+680.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 67756 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220908 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 679.2
Current children cumulated vsize (Kb) 51704

[startup+690.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 68756 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219948 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 689.2
Current children cumulated vsize (Kb) 51704

[startup+700.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 69756 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220032 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 699.2
Current children cumulated vsize (Kb) 51704

[startup+710.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 70756 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221221604 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 709.2
Current children cumulated vsize (Kb) 51704

[startup+720.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 71757 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220504 134693654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 719.21
Current children cumulated vsize (Kb) 51704

[startup+730.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 72757 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221221060 134845938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 729.21
Current children cumulated vsize (Kb) 51704

[startup+740.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 73757 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220904 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 739.21
Current children cumulated vsize (Kb) 51704

[startup+750.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 74758 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221221200 134844697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 749.22
Current children cumulated vsize (Kb) 51704

[startup+760.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 75758 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221218864 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 759.22
Current children cumulated vsize (Kb) 51704

[startup+770.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 76758 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219440 134696316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 769.22
Current children cumulated vsize (Kb) 51704

[startup+780.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 77758 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220608 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 779.22
Current children cumulated vsize (Kb) 51704

[startup+790.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 78759 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220976 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 789.23
Current children cumulated vsize (Kb) 51704

[startup+800.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 79759 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220784 134844682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 799.23
Current children cumulated vsize (Kb) 51704

[startup+810.068 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 80759 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220760 134693740 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 809.23
Current children cumulated vsize (Kb) 51704

[startup+820.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 81759 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221221632 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 819.23
Current children cumulated vsize (Kb) 51704

[startup+830.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 82760 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221221344 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 829.24
Current children cumulated vsize (Kb) 51704

[startup+840.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 83760 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219792 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 839.24
Current children cumulated vsize (Kb) 51704

[startup+850.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 84760 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220764 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 849.24
Current children cumulated vsize (Kb) 51704

[startup+860.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 85760 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220684 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 859.24
Current children cumulated vsize (Kb) 51704

[startup+870.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 86761 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219008 134630898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 869.25
Current children cumulated vsize (Kb) 51704

[startup+880.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 87761 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219324 134695248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 879.25
Current children cumulated vsize (Kb) 51704

[startup+890.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 88761 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221217776 134629145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 889.25
Current children cumulated vsize (Kb) 51704

[startup+900.076 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 89761 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220496 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 899.25
Current children cumulated vsize (Kb) 51704

[startup+910.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 90762 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221221068 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 909.26
Current children cumulated vsize (Kb) 51704

[startup+920.078 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 91762 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220336 134696578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 919.26
Current children cumulated vsize (Kb) 51704

[startup+930.079 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 92762 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220344 134846924 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 929.26
Current children cumulated vsize (Kb) 51704

[startup+940.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 93762 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219824 134720470 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 939.26
Current children cumulated vsize (Kb) 51704

[startup+950.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 94763 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221219668 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 949.27
Current children cumulated vsize (Kb) 51704

[startup+960.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 95763 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221221616 134522315 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 959.27
Current children cumulated vsize (Kb) 51704

[startup+970.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12612 0 0 0 96763 76 0 0 25 0 1 0 1785832838 50765824 11958 4294967295 134512640 135167914 3221224448 3221220080 134629024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11958 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 969.27
Current children cumulated vsize (Kb) 51704

[startup+980.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 97764 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221218320 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 979.28
Current children cumulated vsize (Kb) 51704

[startup+990.085 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 98764 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221219312 134522462 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 989.28
Current children cumulated vsize (Kb) 51704

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 99764 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221220236 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 999.28
Current children cumulated vsize (Kb) 51704

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 100764 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221219088 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1009.28
Current children cumulated vsize (Kb) 51704

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 101765 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221219648 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1019.29
Current children cumulated vsize (Kb) 51704

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 102765 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221219852 134845940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1029.29
Current children cumulated vsize (Kb) 51704

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 103765 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221220256 134844723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1039.29
Current children cumulated vsize (Kb) 51704

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 104765 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221221712 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1049.29
Current children cumulated vsize (Kb) 51704

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 105765 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221218648 134693744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1059.29
Current children cumulated vsize (Kb) 51704

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 106766 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221219168 134522199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1069.3
Current children cumulated vsize (Kb) 51704

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 107766 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221219008 134630935 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1079.3
Current children cumulated vsize (Kb) 51704

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 108766 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221221008 134845909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1089.3
Current children cumulated vsize (Kb) 51704

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 109766 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221220240 134630738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1099.3
Current children cumulated vsize (Kb) 51704

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 110767 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221221388 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1109.31
Current children cumulated vsize (Kb) 51704

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12630 0 0 0 111767 76 0 0 25 0 1 0 1785832838 50765824 11976 4294967295 134512640 135167914 3221224448 3221220864 134696587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11976 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1119.31
Current children cumulated vsize (Kb) 51704

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 112767 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221217772 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1129.31
Current children cumulated vsize (Kb) 51704

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 113767 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221219348 134843031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1139.31
Current children cumulated vsize (Kb) 51704

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 114767 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221221104 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1149.31
Current children cumulated vsize (Kb) 51704

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 115768 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221219904 134844697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1159.32
Current children cumulated vsize (Kb) 51704

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 116768 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221220384 134694489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1169.32
Current children cumulated vsize (Kb) 51704

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 117768 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221219892 134630745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1179.32
Current children cumulated vsize (Kb) 51704

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 118768 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221221200 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1189.32
Current children cumulated vsize (Kb) 51704

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 119769 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1199.33
Current children cumulated vsize (Kb) 51704

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 120769 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221220496 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1209.33
Current children cumulated vsize (Kb) 51704



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 9397
Raw data (/proc/9392/stat): 9392 (minisat+_script) S 9391 9392 30740 0 -1 0 314 2893 0 0 0 1 75 12 18 0 1 0 1785832734 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9392/statm): 532 234 485 147 0 385 0
[pid=9392] vsize: 2128
Raw data (/proc/9397/stat): 9397 (minisat+_bignum) R 9392 9392 30740 0 -1 0 12681 0 0 0 120769 76 0 0 25 0 1 0 1785832838 50765824 11985 4294967295 134512640 135167914 3221224448 3221220552 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9397/statm): 12394 11985 162 162 0 12232 0
[pid=9397] vsize: 49576
Current children cumulated CPU time (s) 1209.33
Current children cumulated vsize (Kb) 51704

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.49
CPU user time (s): 1207.7
CPU system time (s): 0.790879
CPU usage (%): 99.8643
Max. virtual memory (cumulated for all children) (Kb): 51704

Verifier Data

ERROR: no interpretation found !