Some explanations

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

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-czprob.opb
MD5SUMcfa1bf2f1dd2df0f424e37a2971f8ba1
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 65500
Biggest coefficient in the objective function 16110321664000
Number of bits for the biggest coefficient in the objective function 44
Sum of the numbers in the objective function 32674140101032650
Number of bits of the sum of numbers in the objective function 55
Biggest number in a constraint 16110321664000
Number of bits of the biggest number in a constraint 44
Biggest sum of numbers in a constraint 32674140101032650
Number of bits of the biggest sum of numbers55
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables65880
Total number of constraints927
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 constraints927
Minimum length of a constraint20
Maximum length of a constraint7460

Trace number 5994

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        890084 kB
Buffers:          9448 kB
Cached:         109820 kB
SwapCached:        752 kB
Active:          35792 kB
Inactive:        86084 kB
HighTotal:      131008 kB
HighFree:        23464 kB
LowTotal:       903652 kB
LowFree:        866620 kB
SwapTotal:     2097136 kB
SwapFree:      2095876 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            17016 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:52:56 (client local time) WITH STATUS 0 IN 1207.26 SECONDS
stats: 3147 7 1207.26 0

Solver Data

c Parsing PB file...
c Converting 1726 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1725]---> Adder-cost: 12872   maxlim: 94111061   bits: 28/27
c ---[1724]---> Adder-cost: 11886   maxlim: 495322795   bits: 30/29
c ---[1723]---> Adder-cost: 10540   maxlim: 715075261   bits: 30/30
c ---[1722]---> Adder-cost: 8455   maxlim: 256417039   bits: 29/28
c ---[1721]---> Adder-cost: 1022   maxlim: 318643   bits: 19/19
c ---[1720]---> BDD-cost:    7
c ---[1719]---> Adder-cost: 13778   maxlim: 1123951266   bits: 31/31
c ---[1718]---> Adder-cost: 11216   maxlim: 419287690   bits: 30/29
c ---[1717]---> Adder-cost: 17290   maxlim: 792028228   bits: 31/30
c ---[1716]---> BDD-cost: 1855
c ---[1715]---> Adder-cost: 13702   maxlim: 2102946219   bits: 32/31
c ---[1714]---> Adder-cost: 8398   maxlim: 230843009   bits: 29/28
c ---[1712]---> Adder-cost: 13556   maxlim: 447438745   bits: 30/29
c ---[1711]---> Adder-cost: 654   maxlim: 161776   bits: 18/18
c ---[1710]---> Adder-cost: 8922   maxlim: 418111312   bits: 30/29
c ---[1709]---> Adder-cost: 16508   maxlim: 281807139   bits: 30/29
c ---[1707]---> Adder-cost: 4604   maxlim: 3688502   bits: 22/22
c ---[1705]---> Adder-cost: 4426   maxlim: 3472196   bits: 23/22
c ---[1703]---> Adder-cost: 5128   maxlim: 3206051   bits: 23/22
c ---[1701]---> Adder-cost: 5918   maxlim: 3568906   bits: 23/22
c ---[1699]---> Adder-cost: 484   maxlim: 135137   bits: 19/18
c ---[1697]---> BDD-cost:   23
c ---[1695]---> Adder-cost: 6638   maxlim: 4018401   bits: 23/22
c ---[1693]---> Adder-cost: 4066   maxlim: 2519108   bits: 22/22
c ---[1691]---> Adder-cost: 6072   maxlim: 3831272   bits: 23/22
c ---[1689]---> Adder-cost: 612   maxlim: 104684   bits: 18/17
c ---[1687]---> Adder-cost: 4436   maxlim: 1839673   bits: 22/21
c ---[1685]---> Adder-cost: 2380   maxlim: 2058120   bits: 22/21
c ---[1683]---> Adder-cost: 3052   maxlim: 1357823   bits: 22/21
c ---[1681]---> Adder-cost: 2612   maxlim: 2505213   bits: 22/22
c ---[1679]---> Adder-cost: 366   maxlim: 177098   bits: 19/18
c ---[1677]---> Adder-cost: 4574   maxlim: 3558211   bits: 23/22
c ---[1675]---> Adder-cost: 6010   maxlim: 4073335   bits: 23/22
c ---[1673]---> Adder-cost: 4412   maxlim: 80342991   bits: 27/27
c ---[1671]---> BDD-cost:   65
c ---[1669]---> Sorter-cost:  960     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1667]---> Sorter-cost: 1026     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1665]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1663]---> Sorter-cost: 1026     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1659]---> Sorter-cost: 1189     Base: 2 2 2 2 2 2 2 2
c ---[1657]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2
c ---[1655]---> Sorter-cost: 1432     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1653]---> Sorter-cost: 1673     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1651]---> Sorter-cost: 1549     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1649]---> Sorter-cost: 1190     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1647]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2
c ---[1645]---> Sorter-cost: 1189     Base: 2 2 2 2 2 2 2 2
c ---[1643]---> Sorter-cost: 1792     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1641]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1639]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[1637]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1635]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1633]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1631]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1629]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1627]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1625]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[1623]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1621]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1619]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1617]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1615]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1613]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1611]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1609]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1607]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1605]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1603]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1601]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1599]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1597]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1595]---> Sorter-cost: 1306     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1593]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1591]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1589]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1587]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1585]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1583]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1581]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1579]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1577]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1575]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2
c ---[1573]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2
c ---[1571]---> Sorter-cost: 1410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1569]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1567]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1565]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[1563]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[1561]---> Sorter-cost: 1410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1559]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1557]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1555]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1553]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1551]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1549]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1547]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1545]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1543]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1541]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1539]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1537]---> Sorter-cost:  498     Base: 2 2 2 2 2 2 2 2
c ---[1535]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1533]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1521]---> BDD-cost:   50
c ---[1515]---> BDD-cost:   60
c ---[1495]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1493]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1491]---> Sorter-cost: 1939     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1489]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1487]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1485]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1483]---> BDD-cost:   55
c ---[1481]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1479]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1477]---> Sorter-cost: 1190     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1475]---> Sorter-cost: 1410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1473]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1471]---> Sorter-cost: 1989     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1469]---> Sorter-cost: 1626     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1467]---> Sorter-cost: 1626     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1465]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1463]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1461]---> Sorter-cost: 1410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1459]---> Sorter-cost: 1898     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1457]---> Sorter-cost: 2031     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1455]---> Sorter-cost: 1629     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1453]---> Sorter-cost: 1764     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1451]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1449]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1447]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1445]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1443]---> Adder-cost: 252   maxlim: 131638   bits: 18/18
c ---[1441]---> Adder-cost: 270   maxlim: 274998   bits: 19/19
c ---[1439]---> Adder-cost: 180   maxlim: 8630   bits: 14/14
c ---[1437]---> Adder-cost: 324   maxlim: 2163382   bits: 22/22
c ---[1435]---> Sorter-cost: 1751     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1433]---> Sorter-cost: 1939     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1431]---> Sorter-cost: 1939     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1429]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1427]---> Sorter-cost: 2617     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1425]---> Sorter-cost: 1759     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1423]---> Sorter-cost: 1902     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1421]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1419]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1417]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[1415]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1413]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1411]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1409]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1407]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1405]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1403]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1401]---> Sorter-cost: 2125     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1399]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[1397]---> Sorter-cost: 1455     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1395]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1393]---> Sorter-cost: 1991     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1391]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1389]---> Sorter-cost: 1991     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1387]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1385]---> Sorter-cost: 1991     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1383]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[1381]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1379]---> Sorter-cost: 1991     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1377]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1375]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1373]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1369]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1367]---> Sorter-cost:  189     Base: 2 2 2 2 2 2 2 2
c ---[1365]---> BDD-cost:   50
c ---[1359]---> BDD-cost:   65
c ---[1355]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1349]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1347]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1343]---> BDD-cost:   55
c ---[1341]---> BDD-cost:   88
c ---[1339]---> Sorter-cost:  189     Base: 2 2 2 2 2 2 2 2
c ---[1337]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1331]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1329]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1327]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1311]---> BDD-cost:   70
c ---[1309]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1307]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1305]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1303]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1301]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1299]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1297]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1295]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1293]---> BDD-cost:   55
c ---[1291]---> BDD-cost:   60
c ---[1289]---> BDD-cost:   29
c ---[1287]---> BDD-cost:   50
c ---[1285]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1283]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1281]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1279]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2
c ---[1277]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1275]---> BDD-cost:   27
c ---[1273]---> BDD-cost:   23
c ---[1271]---> BDD-cost:   21
c ---[1269]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[1267]---> BDD-cost:   50
c ---[1265]---> BDD-cost:   50
c ---[1263]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1261]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1259]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1257]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[1255]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[1253]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1251]---> BDD-cost:   60
c ---[1249]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1247]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1245]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1229]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1227]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1225]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1221]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1217]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1215]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1213]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1211]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1205]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1203]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1201]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1199]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1197]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1195]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1193]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1191]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1189]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1187]---> Sorter-cost: 1306     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1185]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1183]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1181]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1179]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1177]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1175]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1173]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1171]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1169]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1167]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1165]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1163]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1161]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1157]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1155]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1153]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1151]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1149]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1147]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1145]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1143]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1141]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1139]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1137]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1133]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1129]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1125]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1123]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1119]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1117]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1115]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1113]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1111]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[1109]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[1107]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1105]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1103]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1101]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1099]---> Sorter-cost:  498     Base: 2 2 2 2 2 2 2 2
c ---[1097]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1095]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2
c ---[1093]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1091]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1089]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1087]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1085]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1083]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1081]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1079]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1077]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1075]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1073]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1071]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1069]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1067]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1065]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1063]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1061]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1059]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1057]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1055]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1053]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1051]---> BDD-cost:   60
c ---[1049]---> BDD-cost:   65
c ---[1047]---> BDD-cost:   55
c ---[1009]---> BDD-cost:   60
c ---[1007]---> BDD-cost:   70
c ---[1005]---> BDD-cost:   55
c ---[1003]---> BDD-cost:   65
c ---[1001]---> BDD-cost:   70
c ---[ 999]---> BDD-cost:   60
c ---[ 997]---> BDD-cost:   65
c ---[ 995]---> BDD-cost:   60
c ---[ 993]---> BDD-cost:   50
c ---[ 991]---> BDD-cost:   60
c ---[ 989]---> BDD-cost:   60
c ---[ 987]---> BDD-cost:   55
c ---[ 985]---> BDD-cost:   60
c ---[ 983]---> BDD-cost:   55
c ---[ 981]---> BDD-cost:   60
c ---[ 979]---> BDD-cost:   45
c ---[ 977]---> BDD-cost:   60
c ---[ 975]---> BDD-cost:   40
c ---[ 973]---> BDD-cost:   50
c ---[ 971]---> BDD-cost:   50
c ---[ 969]---> BDD-cost:   60
c ---[ 965]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 963]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 961]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 959]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 957]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 955]---> Sorter-cost:  498     Base: 2 2 2 2 2 2 2 2
c ---[ 953]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 951]---> Sorter-cost:  564     Base: 2 2 2 2 2 2 2 2 2
c ---[ 949]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 947]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 945]---> Sorter-cost:  564     Base: 2 2 2 2 2 2 2 2 2
c ---[ 943]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 941]---> Sorter-cost: 1238     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 939]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 937]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 935]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 933]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 931]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 929]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 927]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 925]---> Sorter-cost:  189     Base: 2 2 2 2 2 2 2 2
c ---[ 923]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 883]---> BDD-cost:   75
c ---[ 881]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 879]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 877]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 875]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 873]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 871]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 869]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 833]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 831]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 829]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 827]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 825]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 823]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 821]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 819]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 817]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 815]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 813]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 811]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 809]---> Sorter-cost:  659     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 807]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> Sorter-cost:  800     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 803]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Sorter-cost:  800     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 797]---> Sorter-cost:  800     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 795]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 793]---> Sorter-cost:  477     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 791]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 789]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 787]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 785]---> Sorter-cost:  659     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost:  659     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> BDD-cost:   33
c ---[ 777]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> BDD-cost:   37
c ---[ 773]---> BDD-cost:   39
c ---[ 769]---> BDD-cost:   75
c ---[ 767]---> BDD-cost:   70
c ---[ 765]---> BDD-cost:   60
c ---[ 763]---> BDD-cost:   65
c ---[ 761]---> BDD-cost:   34
c ---[ 755]---> BDD-cost:   33
c ---[ 753]---> BDD-cost:   33
c ---[ 751]---> BDD-cost:   37
c ---[ 743]---> BDD-cost:   60
c ---[ 741]---> BDD-cost:   50
c ---[ 737]---> BDD-cost:   60
c ---[ 735]---> BDD-cost:   55
c ---[ 733]---> BDD-cost:   60
c ---[ 731]---> BDD-cost:   70
c ---[ 729]---> BDD-cost:   50
c ---[ 689]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 685]---> BDD-cost:   60
c ---[ 683]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 681]---> Sorter-cost:  189     Base: 2 2 2 2 2 2 2 2
c ---[ 679]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 677]---> BDD-cost:   88
c ---[ 675]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 673]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 671]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 669]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 667]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 665]---> BDD-cost:   88
c ---[ 663]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 657]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 637]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost:  189     Base: 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 623]---> BDD-cost:   88
c ---[ 621]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 619]---> BDD-cost:   88
c ---[ 617]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 607]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 605]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> BDD-cost:   45
c ---[ 601]---> BDD-cost:   55
c ---[ 599]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 597]---> BDD-cost:   35
c ---[ 595]---> BDD-cost:   45
c ---[ 593]---> BDD-cost:   40
c ---[ 591]---> BDD-cost:   45
c ---[ 589]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 583]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 581]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> BDD-cost:   75
c ---[ 573]---> BDD-cost:   70
c ---[ 571]---> BDD-cost:   55
c ---[ 569]---> BDD-cost:   60
c ---[ 567]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> BDD-cost:   50
c ---[ 563]---> BDD-cost:   50
c ---[ 561]---> BDD-cost:   50
c ---[ 559]---> BDD-cost:   55
c ---[ 557]---> BDD-cost:   70
c ---[ 555]---> BDD-cost:   45
c ---[ 553]---> BDD-cost:   50
c ---[ 551]---> BDD-cost:   50
c ---[ 549]---> BDD-cost:   50
c ---[ 547]---> BDD-cost:   45
c ---[ 545]---> BDD-cost:   40
c ---[ 543]---> BDD-cost:   40
c ---[ 541]---> BDD-cost:   55
c ---[ 539]---> BDD-cost:   45
c ---[ 537]---> BDD-cost:   45
c ---[ 535]---> BDD-cost:   40
c ---[ 519]---> BDD-cost:   70
c ---[ 517]---> BDD-cost:   50
c ---[ 515]---> BDD-cost:   50
c ---[ 513]---> BDD-cost:   75
c ---[ 511]---> BDD-cost:   60
c ---[ 509]---> BDD-cost:   60
c ---[ 507]---> BDD-cost:   55
c ---[ 505]---> BDD-cost:   35
c ---[ 503]---> BDD-cost:   55
c ---[ 501]---> BDD-cost:   35
c ---[ 495]---> BDD-cost:   70
c ---[ 493]---> BDD-cost:   45
c ---[ 491]---> BDD-cost:   55
c ---[ 489]---> BDD-cost:   65
c ---[ 487]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> BDD-cost:   50
c ---[ 477]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> BDD-cost:   60
c ---[ 463]---> BDD-cost:   55
c ---[ 461]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> BDD-cost:   50
c ---[ 449]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 443]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost:  189     Base: 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> BDD-cost:   50
c ---[ 431]---> BDD-cost:   55
c ---[ 429]---> BDD-cost:   55
c ---[ 427]---> BDD-cost:   60
c ---[ 425]---> BDD-cost:   55
c ---[ 423]---> BDD-cost:   60
c ---[ 421]---> BDD-cost:   60
c ---[ 419]---> BDD-cost:   60
c ---[ 417]---> BDD-cost:   60
c ---[ 415]---> BDD-cost:   50
c ---[ 413]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 399]---> BDD-cost:   88
c ---[ 397]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> Sorter-cost:  213     Base: 2 2 2 2 2 2 2 2 2
c ---[ 389]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 387]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 381]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 375]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 369]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 361]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 357]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 355]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost:  357     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 345]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 337]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 329]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 327]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 325]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 323]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost:  357     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost:  357     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Sorter-cost:  357     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 315]---> BDD-cost:   70
c ---[ 313]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 307]---> BDD-cost:   55
c ---[ 305]---> BDD-cost:   55
c ---[ 303]---> BDD-cost:   65
c ---[ 301]---> BDD-cost:   55
c ---[ 299]---> BDD-cost:   65
c ---[ 297]---> BDD-cost:   55
c ---[ 295]---> BDD-cost:   55
c ---[ 293]---> BDD-cost:   55
c ---[ 291]---> BDD-cost:   65
c ---[ 289]---> BDD-cost:   35
c ---[ 287]---> BDD-cost:   40
c ---[ 285]---> BDD-cost:   55
c ---[ 283]---> BDD-cost:   40
c ---[ 281]---> BDD-cost:   40
c ---[ 279]---> BDD-cost:   45
c ---[ 277]---> BDD-cost:   75
c ---[ 275]---> BDD-cost:   60
c ---[ 269]---> BDD-cost:   50
c ---[ 267]---> BDD-cost:   60
c ---[ 265]---> BDD-cost:   35
c ---[ 263]---> BDD-cost:   60
c ---[ 261]---> BDD-cost:   55
c ---[ 259]---> BDD-cost:   60
c ---[ 257]---> BDD-cost:   55
c ---[ 255]---> BDD-cost:   40
c ---[ 253]---> BDD-cost:   55
c ---[ 251]---> BDD-cost:   55
c ---[ 249]---> BDD-cost:   60
c ---[ 247]---> BDD-cost:   60
c ---[ 245]---> BDD-cost:   60
c ---[ 243]---> BDD-cost:   55
c ---[ 241]---> BDD-cost:   45
c ---[ 239]---> BDD-cost:   55
c ---[ 233]---> BDD-cost:   55
c ---[ 231]---> BDD-cost:   35
c ---[ 229]---> BDD-cost:   35
c ---[ 227]---> BDD-cost:   45
c ---[ 225]---> BDD-cost:   45
c ---[ 223]---> BDD-cost:   40
c ---[ 221]---> BDD-cost:   45
c ---[ 219]---> BDD-cost:   40
c ---[ 217]---> BDD-cost:   75
c ---[ 215]---> BDD-cost:   60
c ---[ 209]---> BDD-cost:   50
c ---[ 207]---> BDD-cost:   45
c ---[ 205]---> BDD-cost:   50
c ---[ 203]---> BDD-cost:   40
c ---[ 201]---> BDD-cost:   40
c ---[ 199]---> BDD-cost:   75
c ---[ 197]---> BDD-cost:   35
c ---[ 195]---> BDD-cost:   55
c ---[ 193]---> BDD-cost:   50
c ---[ 167]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 155]---> BDD-cost:   65
c ---[ 153]---> BDD-cost:   55
c ---[ 151]---> BDD-cost:   60
c ---[ 149]---> BDD-cost:   55
c ---[ 147]---> BDD-cost:   65
c ---[ 145]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> BDD-cost:   84
c ---[ 137]---> BDD-cost:   76
c ---[ 135]---> BDD-cost:   45
c ---[ 133]---> BDD-cost:   55
c ---[ 131]---> BDD-cost:   45
c ---[ 129]---> BDD-cost:   60
c ---[ 127]---> BDD-cost:   45
c ---[ 123]---> BDD-cost:   55
c ---[ 121]---> BDD-cost:   55
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   55
c ---[ 115]---> BDD-cost:   55
c ---[ 113]---> BDD-cost:   55
c ---[  53]---> BDD-cost:   55
c ---[  51]---> BDD-cost:   70
c ---[  49]---> BDD-cost:   50
c ---[  43]---> BDD-cost:   60
c ---[  39]---> BDD-cost:   21
c ---[  37]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   55
c ---[  33]---> BDD-cost:   50
c ---[  31]---> BDD-cost:   21
c ---[  29]---> BDD-cost:   25
c ---[  27]---> BDD-cost:   23
c ---[  25]---> BDD-cost:   21
c ---[  22]---> Sorter-cost:  941     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Adder-cost: 230   maxlim: 70709   bits: 18/17
c ---[  16]---> Sorter-cost: 1708     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost: 1708     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  272     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost: 1410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost: 1520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost: 2691     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost: 1857     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost: 1723     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2401325  7504911 |  800441       0        0     nan |  0.000 % |
c |       100 | 2401305  7504867 |  880485      99      345     3.5 |  8.866 % |
c |       250 | 2401216  7504668 |  968533     246      853     3.5 |  8.870 % |
c |       475 | 2401120  7504452 | 1065386     462     1584     3.4 |  8.875 % |
c |       813 | 2400898  7503955 | 1171925     796     2881     3.6 |  8.885 % |
c |      1321 | 2400807  7503748 | 1289118    1301     4473     3.4 |  8.890 % |
c |      2082 | 2400736  7503589 | 1418030    2058     7179     3.5 |  8.894 % |
c |      3221 | 2400477  7502918 | 1559833    3177    11279     3.6 |  8.905 % |
c |      4929 | 2399380  7500374 | 1715816    4828    17289     3.6 |  8.960 % |
c |      7492 | 2399005  7499525 | 1887398    7367    29905     4.1 |  8.980 % |
c |     11337 | 2398032  7497324 | 2076137   11160    51644     4.6 |  9.029 % |
c |     17103 | 2396081  7492908 | 2283751   16841    81686     4.9 |  9.129 % |
c |     25752 | 2395362  7491283 | 2512126   25449   194056     7.6 |  9.167 % |
c |     38726 | 2393190  7486337 | 2763339   38284   334680     8.7 |  9.277 % |

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/9370/stat): 9370 (minisat+_script) R 9369 9370 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796760338 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9370/statm): 174 3 169 147 0 27 0
[pid=9370] 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=9371
New process pid=9372
New process pid=9373
execve syscall for /bin/sed executable
One traced child (pid=9372) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=9373) exited with status: 0
One traced child (pid=9371) exited with status: 0
New process pid=9374
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-czprob.opb

[startup+10.0034 s]
Raw data (loadavg): 0.93 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 6874 0 0 0 936 34 0 0 25 0 1 0 1796760343 30339072 4900 4294967295 134512640 135094434 3221224432 3221223248 134580074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 7407 4900 145 145 0 7262 0
[pid=9374] vsize: 29628
Current children cumulated CPU time (s) 9.71
Current children cumulated vsize (Kb) 31752

[startup+20.004 s]
Raw data (loadavg): 0.94 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 6874 0 0 0 1936 34 0 0 25 0 1 0 1796760343 30339072 4900 4294967295 134512640 135094434 3221224432 3221223248 134580059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 7407 4900 145 145 0 7262 0
[pid=9374] vsize: 29628
Current children cumulated CPU time (s) 19.71
Current children cumulated vsize (Kb) 31752

[startup+30.0047 s]
Raw data (loadavg): 0.95 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 7634 0 0 0 2934 36 0 0 25 0 1 0 1796760343 29945856 4778 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 7311 4778 145 145 0 7166 0
[pid=9374] vsize: 29244
Current children cumulated CPU time (s) 29.71
Current children cumulated vsize (Kb) 31368

[startup+40.0053 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 7634 0 0 0 3934 36 0 0 25 0 1 0 1796760343 29945856 4778 4294967295 134512640 135094434 3221224432 3221221456 134600307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 7311 4778 145 145 0 7166 0
[pid=9374] vsize: 29244
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 31368

[startup+50.0059 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 4921 44 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221219968 134676349 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 49.66
Current children cumulated vsize (Kb) 36436

[startup+60.0066 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 5921 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 59.67
Current children cumulated vsize (Kb) 36436

[startup+70.0062 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 6922 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221221808 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 69.68
Current children cumulated vsize (Kb) 36436

[startup+80.0078 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 7922 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221221552 134676999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 79.68
Current children cumulated vsize (Kb) 36436

[startup+90.0085 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 8922 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221221164 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 36436

[startup+100.008 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 9922 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221221200 134676376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 99.68
Current children cumulated vsize (Kb) 36436

[startup+110.009 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 10923 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221220752 134676586 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 36436

[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 11922 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 36436

[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 12923 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 129.69
Current children cumulated vsize (Kb) 36436

[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 10105 0 0 0 13923 45 0 0 25 0 1 0 1796760343 35135488 5774 4294967295 134512640 135094434 3221224432 3221220864 134518564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 8578 5774 145 145 0 8433 0
[pid=9374] vsize: 34312
Current children cumulated CPU time (s) 139.69
Current children cumulated vsize (Kb) 36436

[startup+150.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 13206 0 0 0 14906 55 0 0 25 0 1 0 1796760343 37167104 6370 4294967295 134512640 135094434 3221224432 3221221552 134677065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9074 6370 145 145 0 8929 0
[pid=9374] vsize: 36296
Current children cumulated CPU time (s) 149.62
Current children cumulated vsize (Kb) 38420

[startup+160.012 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 13206 0 0 0 15906 55 0 0 25 0 1 0 1796760343 37167104 6370 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9074 6370 145 145 0 8929 0
[pid=9374] vsize: 36296
Current children cumulated CPU time (s) 159.62
Current children cumulated vsize (Kb) 38420

[startup+170.013 s]
Raw data (loadavg): 1.13 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 15246 0 0 0 16896 61 0 0 25 0 1 0 1796760343 37138432 6363 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9067 6363 145 145 0 8922 0
[pid=9374] vsize: 36268
Current children cumulated CPU time (s) 169.58
Current children cumulated vsize (Kb) 38392

[startup+180.013 s]
Raw data (loadavg): 1.11 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 15246 0 0 0 17897 61 0 0 25 0 1 0 1796760343 37138432 6363 4294967295 134512640 135094434 3221224432 3221221632 134677354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9067 6363 145 145 0 8922 0
[pid=9374] vsize: 36268
Current children cumulated CPU time (s) 179.59
Current children cumulated vsize (Kb) 38392

[startup+190.014 s]
Raw data (loadavg): 1.10 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 17307 0 0 0 18885 68 0 0 25 0 1 0 1796760343 37195776 6377 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9081 6377 145 145 0 8936 0
[pid=9374] vsize: 36324
Current children cumulated CPU time (s) 189.54
Current children cumulated vsize (Kb) 38448

[startup+200.014 s]
Raw data (loadavg): 1.08 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 17307 0 0 0 19884 69 0 0 25 0 1 0 1796760343 37195776 6377 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9081 6377 145 145 0 8936 0
[pid=9374] vsize: 36324
Current children cumulated CPU time (s) 199.54
Current children cumulated vsize (Kb) 38448

[startup+210.015 s]
Raw data (loadavg): 1.07 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 17307 0 0 0 20885 69 0 0 25 0 1 0 1796760343 37195776 6377 4294967295 134512640 135094434 3221224432 3221221424 134676993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9081 6377 145 145 0 8936 0
[pid=9374] vsize: 36324
Current children cumulated CPU time (s) 209.55
Current children cumulated vsize (Kb) 38448

[startup+220.016 s]
Raw data (loadavg): 1.06 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 17307 0 0 0 21885 69 0 0 25 0 1 0 1796760343 37195776 6377 4294967295 134512640 135094434 3221224432 3221222080 134676376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9081 6377 145 145 0 8936 0
[pid=9374] vsize: 36324
Current children cumulated CPU time (s) 219.55
Current children cumulated vsize (Kb) 38448

[startup+230.016 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 17307 0 0 0 22885 69 0 0 25 0 1 0 1796760343 37195776 6377 4294967295 134512640 135094434 3221224432 3221221904 134677042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9081 6377 145 145 0 8936 0
[pid=9374] vsize: 36324
Current children cumulated CPU time (s) 229.55
Current children cumulated vsize (Kb) 38448

[startup+240.017 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 17307 0 0 0 23885 69 0 0 25 0 1 0 1796760343 37195776 6377 4294967295 134512640 135094434 3221224432 3221222036 134676464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9081 6377 145 145 0 8936 0
[pid=9374] vsize: 36324
Current children cumulated CPU time (s) 239.55
Current children cumulated vsize (Kb) 38448

[startup+250.017 s]
Raw data (loadavg): 1.11 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 24870 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220576 134600144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 249.48
Current children cumulated vsize (Kb) 39460

[startup+260.017 s]
Raw data (loadavg): 1.10 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 25870 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220804 134677232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 259.48
Current children cumulated vsize (Kb) 39460

[startup+270.017 s]
Raw data (loadavg): 1.08 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 26871 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 269.49
Current children cumulated vsize (Kb) 39460

[startup+280.017 s]
Raw data (loadavg): 1.07 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 27871 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 279.49
Current children cumulated vsize (Kb) 39460

[startup+290.018 s]
Raw data (loadavg): 1.06 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 28871 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 289.49
Current children cumulated vsize (Kb) 39460

[startup+300.018 s]
Raw data (loadavg): 1.05 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 29871 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220464 134677091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 299.49
Current children cumulated vsize (Kb) 39460

[startup+310.018 s]
Raw data (loadavg): 1.04 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 30871 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220928 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 309.49
Current children cumulated vsize (Kb) 39460

[startup+320.019 s]
Raw data (loadavg): 1.03 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 31872 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221424 134677147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 319.5
Current children cumulated vsize (Kb) 39460

[startup+330.02 s]
Raw data (loadavg): 1.03 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 32872 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221152 134676465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 329.5
Current children cumulated vsize (Kb) 39460

[startup+340.02 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 33872 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220672 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 339.5
Current children cumulated vsize (Kb) 39460

[startup+350.02 s]
Raw data (loadavg): 1.02 1.02 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 34872 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221728 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 349.5
Current children cumulated vsize (Kb) 39460

[startup+360.021 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 35873 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221376 134677069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 359.51
Current children cumulated vsize (Kb) 39460

[startup+370.021 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 36873 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220624 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 369.51
Current children cumulated vsize (Kb) 39460

[startup+380.022 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 37873 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220928 134676586 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 379.51
Current children cumulated vsize (Kb) 39460

[startup+390.022 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 38873 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221008 134677078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 389.51
Current children cumulated vsize (Kb) 39460

[startup+400.023 s]
Raw data (loadavg): 1.01 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 39873 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221632 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 399.51
Current children cumulated vsize (Kb) 39460

[startup+410.024 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 40873 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220848 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 409.51
Current children cumulated vsize (Kb) 39460

[startup+420.023 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 41874 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 419.52
Current children cumulated vsize (Kb) 39460

[startup+430.025 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 42874 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221456 134677239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 429.52
Current children cumulated vsize (Kb) 39460

[startup+440.026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 43874 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221552 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 439.52
Current children cumulated vsize (Kb) 39460

[startup+450.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 44874 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221176 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 449.52
Current children cumulated vsize (Kb) 39460

[startup+460.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 45875 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221452 134600233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 459.53
Current children cumulated vsize (Kb) 39460

[startup+470.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 46875 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 469.53
Current children cumulated vsize (Kb) 39460

[startup+480.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 47875 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 479.53
Current children cumulated vsize (Kb) 39460

[startup+490.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 19752 0 0 0 48875 77 0 0 25 0 1 0 1796760343 38232064 6776 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9334 6776 145 145 0 9189 0
[pid=9374] vsize: 37336
Current children cumulated CPU time (s) 489.53
Current children cumulated vsize (Kb) 39460

[startup+500.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22281 0 0 0 49859 86 0 0 25 0 1 0 1796760343 38440960 6812 4294967295 134512640 135094434 3221224432 3221220648 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9374/statm): 9385 6812 145 145 0 9240 0
[pid=9374] vsize: 37540
Current children cumulated CPU time (s) 499.46
Current children cumulated vsize (Kb) 39664

[startup+510.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22281 0 0 0 50859 86 0 0 25 0 1 0 1796760343 38440960 6812 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9385 6812 145 145 0 9240 0
[pid=9374] vsize: 37540
Current children cumulated CPU time (s) 509.46
Current children cumulated vsize (Kb) 39664

[startup+520.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22281 0 0 0 51859 86 0 0 25 0 1 0 1796760343 38440960 6812 4294967295 134512640 135094434 3221224432 3221221376 134676999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9385 6812 145 145 0 9240 0
[pid=9374] vsize: 37540
Current children cumulated CPU time (s) 519.46
Current children cumulated vsize (Kb) 39664

[startup+530.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22301 0 0 0 52859 86 0 0 25 0 1 0 1796760343 38440960 6812 4294967295 134512640 135094434 3221224432 3221221456 134677366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9385 6812 145 145 0 9240 0
[pid=9374] vsize: 37540
Current children cumulated CPU time (s) 529.46
Current children cumulated vsize (Kb) 39664

[startup+540.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22341 0 0 0 53859 86 0 0 25 0 1 0 1796760343 38440960 6812 4294967295 134512640 135094434 3221224432 3221221176 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9385 6812 145 145 0 9240 0
[pid=9374] vsize: 37540
Current children cumulated CPU time (s) 539.46
Current children cumulated vsize (Kb) 39664

[startup+550.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22421 0 0 0 54859 86 0 0 25 0 1 0 1796760343 38440960 6809 4294967295 134512640 135094434 3221224432 3221221796 134600159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9385 6809 145 145 0 9240 0
[pid=9374] vsize: 37540
Current children cumulated CPU time (s) 549.46
Current children cumulated vsize (Kb) 39664

[startup+560.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22621 0 0 0 55859 87 0 0 25 0 1 0 1796760343 38440960 6806 4294967295 134512640 135094434 3221224432 3221221632 134676542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9385 6806 145 145 0 9240 0
[pid=9374] vsize: 37540
Current children cumulated CPU time (s) 559.47
Current children cumulated vsize (Kb) 39664

[startup+570.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 22911 0 0 0 56857 88 0 0 25 0 1 0 1796760343 38375424 6796 4294967295 134512640 135094434 3221224432 3221222256 134676251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 9369 6796 145 145 0 9224 0
[pid=9374] vsize: 37476
Current children cumulated CPU time (s) 569.46
Current children cumulated vsize (Kb) 39600

[startup+580.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 57826 104 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221219696 134676595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 579.31
Current children cumulated vsize (Kb) 47816

[startup+590.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 58826 104 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 589.31
Current children cumulated vsize (Kb) 47816

[startup+600.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 59826 104 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221220672 134676280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 599.31
Current children cumulated vsize (Kb) 47816

[startup+610.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 60826 104 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221024 134676259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 609.31
Current children cumulated vsize (Kb) 47816

[startup+620.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 61826 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221072 134677147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 619.32
Current children cumulated vsize (Kb) 47816

[startup+630.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 62826 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 629.32
Current children cumulated vsize (Kb) 47816

[startup+640.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 63826 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 639.32
Current children cumulated vsize (Kb) 47816

[startup+650.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 64826 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221272 134600155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 649.32
Current children cumulated vsize (Kb) 47816

[startup+660.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 65827 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221280 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 659.33
Current children cumulated vsize (Kb) 47816

[startup+670.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 66827 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221280 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 669.33
Current children cumulated vsize (Kb) 47816

[startup+680.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 67827 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221808 134600215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 679.33
Current children cumulated vsize (Kb) 47816

[startup+690.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 68827 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221796 134600159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 689.33
Current children cumulated vsize (Kb) 47816

[startup+700.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 69827 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221632 134600307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 699.33
Current children cumulated vsize (Kb) 47816

[startup+710.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 70828 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 709.34
Current children cumulated vsize (Kb) 47816

[startup+720.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 71828 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 719.34
Current children cumulated vsize (Kb) 47816

[startup+730.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 28046 0 0 0 72828 105 0 0 25 0 1 0 1796760343 46788608 8456 4294967295 134512640 135094434 3221224432 3221221880 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11423 8456 145 145 0 11278 0
[pid=9374] vsize: 45692
Current children cumulated CPU time (s) 729.34
Current children cumulated vsize (Kb) 47816

[startup+740.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 30075 0 0 0 73816 113 0 0 25 0 1 0 1796760343 46891008 8481 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11448 8481 145 145 0 11303 0
[pid=9374] vsize: 45792
Current children cumulated CPU time (s) 739.3
Current children cumulated vsize (Kb) 47916

[startup+750.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 30075 0 0 0 74817 113 0 0 25 0 1 0 1796760343 46891008 8481 4294967295 134512640 135094434 3221224432 3221221612 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11448 8481 145 145 0 11303 0
[pid=9374] vsize: 45792
Current children cumulated CPU time (s) 749.31
Current children cumulated vsize (Kb) 47916

[startup+760.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 30075 0 0 0 75817 113 0 0 25 0 1 0 1796760343 46891008 8481 4294967295 134512640 135094434 3221224432 3221221808 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11448 8481 145 145 0 11303 0
[pid=9374] vsize: 45792
Current children cumulated CPU time (s) 759.31
Current children cumulated vsize (Kb) 47916

[startup+770.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 32046 0 0 0 76806 119 0 0 25 0 1 0 1796760343 46882816 8479 4294967295 134512640 135094434 3221224432 3221221104 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11446 8479 145 145 0 11301 0
[pid=9374] vsize: 45784
Current children cumulated CPU time (s) 769.26
Current children cumulated vsize (Kb) 47908

[startup+780.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 32046 0 0 0 77806 119 0 0 25 0 1 0 1796760343 46882816 8479 4294967295 134512640 135094434 3221224432 3221220496 134676311 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11446 8479 145 145 0 11301 0
[pid=9374] vsize: 45784
Current children cumulated CPU time (s) 779.26
Current children cumulated vsize (Kb) 47908

[startup+790.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 32485 0 0 0 78803 121 0 0 25 0 1 0 1796760343 46882816 8479 4294967295 134512640 135094434 3221224432 3221221280 134676522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11446 8479 145 145 0 11301 0
[pid=9374] vsize: 45784
Current children cumulated CPU time (s) 789.25
Current children cumulated vsize (Kb) 47908

[startup+800.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 32485 0 0 0 79803 121 0 0 25 0 1 0 1796760343 46882816 8479 4294967295 134512640 135094434 3221224432 3221221552 134677028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11446 8479 145 145 0 11301 0
[pid=9374] vsize: 45784
Current children cumulated CPU time (s) 799.25
Current children cumulated vsize (Kb) 47908

[startup+810.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 33458 0 0 0 80797 124 0 0 25 0 1 0 1796760343 46796800 8458 4294967295 134512640 135094434 3221224432 3221220752 134677287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9374/statm): 11425 8458 145 145 0 11280 0
[pid=9374] vsize: 45700
Current children cumulated CPU time (s) 809.22
Current children cumulated vsize (Kb) 47824

[startup+820.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 33458 0 0 0 81797 124 0 0 25 0 1 0 1796760343 46796800 8458 4294967295 134512640 135094434 3221224432 3221221280 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11425 8458 145 145 0 11280 0
[pid=9374] vsize: 45700
Current children cumulated CPU time (s) 819.22
Current children cumulated vsize (Kb) 47824

[startup+830.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 33458 0 0 0 82797 124 0 0 25 0 1 0 1796760343 46796800 8458 4294967295 134512640 135094434 3221224432 3221221632 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11425 8458 145 145 0 11280 0
[pid=9374] vsize: 45700
Current children cumulated CPU time (s) 829.22
Current children cumulated vsize (Kb) 47824

[startup+840.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 33458 0 0 0 83798 124 0 0 25 0 1 0 1796760343 46796800 8458 4294967295 134512640 135094434 3221224432 3221221512 134676461 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11425 8458 145 145 0 11280 0
[pid=9374] vsize: 45700
Current children cumulated CPU time (s) 839.23
Current children cumulated vsize (Kb) 47824

[startup+850.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 33650 0 0 0 84797 125 0 0 25 0 1 0 1796760343 47104000 8566 4294967295 134512640 135094434 3221224432 3220942272 134596815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 11500 8566 145 145 0 11355 0
[pid=9374] vsize: 46000
Current children cumulated CPU time (s) 849.23
Current children cumulated vsize (Kb) 48124

[startup+860.048 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) T 9370 9370 15400 0 -1 0 44846 0 0 0 85706 169 0 0 17 0 1 0 1796760343 93933568 19361 4294967295 134512640 135094434 3221224432 3221214044 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9374/statm): 22933 19361 145 145 0 22788 0
[pid=9374] vsize: 91732
Current children cumulated CPU time (s) 858.76
Current children cumulated vsize (Kb) 93856

[startup+870.049 s]
Raw data (loadavg): 1.00 1.00 0.93 1/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) T 9370 9370 15400 0 -1 0 74359 0 0 0 86438 299 0 0 22 0 1 0 1796760343 250011648 48874 4294967295 134512640 135094434 3221224432 3221207772 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9374/statm): 61038 48874 145 145 0 60893 0
[pid=9374] vsize: 244152
Current children cumulated CPU time (s) 867.38
Current children cumulated vsize (Kb) 246276

[startup+880.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 76879 0 0 0 87415 309 0 0 25 0 1 0 1796760343 257646592 51394 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 62902 51394 145 145 0 62757 0
[pid=9374] vsize: 251608
Current children cumulated CPU time (s) 877.25
Current children cumulated vsize (Kb) 253732

[startup+890.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77266 0 0 0 88411 310 0 0 25 0 1 0 1796760343 259047424 51781 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63244 51781 145 145 0 63099 0
[pid=9374] vsize: 252976
Current children cumulated CPU time (s) 887.22
Current children cumulated vsize (Kb) 255100

[startup+900.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77444 0 0 0 89408 312 0 0 25 0 1 0 1796760343 259715072 51959 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63407 51959 145 145 0 63262 0
[pid=9374] vsize: 253628
Current children cumulated CPU time (s) 897.21
Current children cumulated vsize (Kb) 255752

[startup+910.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77501 0 0 0 90407 313 0 0 25 0 1 0 1796760343 259940352 52016 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63462 52016 145 145 0 63317 0
[pid=9374] vsize: 253848
Current children cumulated CPU time (s) 907.21
Current children cumulated vsize (Kb) 255972

[startup+920.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77529 0 0 0 91407 313 0 0 25 0 1 0 1796760343 260063232 52044 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63492 52044 145 145 0 63347 0
[pid=9374] vsize: 253968
Current children cumulated CPU time (s) 917.21
Current children cumulated vsize (Kb) 256092

[startup+930.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77569 0 0 0 92407 313 0 0 25 0 1 0 1796760343 260222976 52084 4294967295 134512640 135094434 3221224432 3221223184 134559213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63531 52084 145 145 0 63386 0
[pid=9374] vsize: 254124
Current children cumulated CPU time (s) 927.21
Current children cumulated vsize (Kb) 256248

[startup+940.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77592 0 0 0 93406 313 0 0 25 0 1 0 1796760343 260317184 52107 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63554 52107 145 145 0 63409 0
[pid=9374] vsize: 254216
Current children cumulated CPU time (s) 937.2
Current children cumulated vsize (Kb) 256340

[startup+950.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77831 0 0 0 94403 314 0 0 25 0 1 0 1796760343 261173248 52346 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63763 52346 145 145 0 63618 0
[pid=9374] vsize: 255052
Current children cumulated CPU time (s) 947.18
Current children cumulated vsize (Kb) 257176

[startup+960.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77896 0 0 0 95403 314 0 0 25 0 1 0 1796760343 261464064 52411 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63834 52411 145 145 0 63689 0
[pid=9374] vsize: 255336
Current children cumulated CPU time (s) 957.18
Current children cumulated vsize (Kb) 257460

[startup+970.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77928 0 0 0 96402 315 0 0 25 0 1 0 1796760343 261591040 52443 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63865 52443 145 145 0 63720 0
[pid=9374] vsize: 255460
Current children cumulated CPU time (s) 967.18
Current children cumulated vsize (Kb) 257584

[startup+980.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77964 0 0 0 97402 315 0 0 25 0 1 0 1796760343 261730304 52479 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63899 52479 145 145 0 63754 0
[pid=9374] vsize: 255596
Current children cumulated CPU time (s) 977.18
Current children cumulated vsize (Kb) 257720

[startup+990.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 77997 0 0 0 98401 316 0 0 25 0 1 0 1796760343 261861376 52512 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63931 52512 145 145 0 63786 0
[pid=9374] vsize: 255724
Current children cumulated CPU time (s) 987.18
Current children cumulated vsize (Kb) 257848

[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78035 0 0 0 99400 316 0 0 25 0 1 0 1796760343 262012928 52550 4294967295 134512640 135094434 3221224432 3221223056 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 63968 52550 145 145 0 63823 0
[pid=9374] vsize: 255872
Current children cumulated CPU time (s) 997.17
Current children cumulated vsize (Kb) 257996

[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78082 0 0 0 100400 317 0 0 25 0 1 0 1796760343 262205440 52597 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64015 52597 145 145 0 63870 0
[pid=9374] vsize: 256060
Current children cumulated CPU time (s) 1007.18
Current children cumulated vsize (Kb) 258184

[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78113 0 0 0 101399 317 0 0 25 0 1 0 1796760343 262328320 52628 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64045 52628 145 145 0 63900 0
[pid=9374] vsize: 256180
Current children cumulated CPU time (s) 1017.17
Current children cumulated vsize (Kb) 258304

[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78135 0 0 0 102399 317 0 0 25 0 1 0 1796760343 262418432 52650 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64067 52650 145 145 0 63922 0
[pid=9374] vsize: 256268
Current children cumulated CPU time (s) 1027.17
Current children cumulated vsize (Kb) 258392

[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78153 0 0 0 103399 317 0 0 25 0 1 0 1796760343 262492160 52668 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64085 52668 145 145 0 63940 0
[pid=9374] vsize: 256340
Current children cumulated CPU time (s) 1037.17
Current children cumulated vsize (Kb) 258464

[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78179 0 0 0 104399 318 0 0 25 0 1 0 1796760343 262594560 52694 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64110 52694 145 145 0 63965 0
[pid=9374] vsize: 256440
Current children cumulated CPU time (s) 1047.18
Current children cumulated vsize (Kb) 258564

[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78212 0 0 0 105398 318 0 0 25 0 1 0 1796760343 262791168 52727 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64158 52727 145 145 0 64013 0
[pid=9374] vsize: 256632
Current children cumulated CPU time (s) 1057.17
Current children cumulated vsize (Kb) 258756

[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78250 0 0 0 106397 318 0 0 25 0 1 0 1796760343 262938624 52765 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64194 52765 145 145 0 64049 0
[pid=9374] vsize: 256776
Current children cumulated CPU time (s) 1067.16
Current children cumulated vsize (Kb) 258900

[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78298 0 0 0 107397 319 0 0 25 0 1 0 1796760343 263131136 52813 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64241 52813 145 145 0 64096 0
[pid=9374] vsize: 256964
Current children cumulated CPU time (s) 1077.17
Current children cumulated vsize (Kb) 259088

[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78349 0 0 0 108396 319 0 0 25 0 1 0 1796760343 263331840 52864 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64290 52864 145 145 0 64145 0
[pid=9374] vsize: 257160
Current children cumulated CPU time (s) 1087.16
Current children cumulated vsize (Kb) 259284

[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78407 0 0 0 109395 320 0 0 25 0 1 0 1796760343 263561216 52922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64346 52922 145 145 0 64201 0
[pid=9374] vsize: 257384
Current children cumulated CPU time (s) 1097.16
Current children cumulated vsize (Kb) 259508

[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78471 0 0 0 110395 320 0 0 25 0 1 0 1796760343 263815168 52986 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64408 52986 145 145 0 64263 0
[pid=9374] vsize: 257632
Current children cumulated CPU time (s) 1107.16
Current children cumulated vsize (Kb) 259756

[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78506 0 0 0 111394 321 0 0 25 0 1 0 1796760343 263954432 53021 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64442 53021 145 145 0 64297 0
[pid=9374] vsize: 257768
Current children cumulated CPU time (s) 1117.16
Current children cumulated vsize (Kb) 259892

[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78540 0 0 0 112394 321 0 0 25 0 1 0 1796760343 264089600 53055 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64475 53055 145 145 0 64330 0
[pid=9374] vsize: 257900
Current children cumulated CPU time (s) 1127.16
Current children cumulated vsize (Kb) 260024

[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78563 0 0 0 113393 322 0 0 25 0 1 0 1796760343 264179712 53078 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64497 53078 145 145 0 64352 0
[pid=9374] vsize: 257988
Current children cumulated CPU time (s) 1137.16
Current children cumulated vsize (Kb) 260112

[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78577 0 0 0 114393 322 0 0 25 0 1 0 1796760343 264232960 53092 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64510 53092 145 145 0 64365 0
[pid=9374] vsize: 258040
Current children cumulated CPU time (s) 1147.16
Current children cumulated vsize (Kb) 260164

[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78690 0 0 0 115392 322 0 0 25 0 1 0 1796760343 264814592 53205 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64652 53205 145 145 0 64507 0
[pid=9374] vsize: 258608
Current children cumulated CPU time (s) 1157.15
Current children cumulated vsize (Kb) 260732

[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78712 0 0 0 116391 323 0 0 25 0 1 0 1796760343 264896512 53227 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64672 53227 145 145 0 64527 0
[pid=9374] vsize: 258688
Current children cumulated CPU time (s) 1167.15
Current children cumulated vsize (Kb) 260812

[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78745 0 0 0 117390 324 0 0 25 0 1 0 1796760343 265027584 53260 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64704 53260 145 145 0 64559 0
[pid=9374] vsize: 258816
Current children cumulated CPU time (s) 1177.15
Current children cumulated vsize (Kb) 260940

[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78810 0 0 0 118389 325 0 0 25 0 1 0 1796760343 265285632 53325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64767 53325 145 145 0 64622 0
[pid=9374] vsize: 259068
Current children cumulated CPU time (s) 1187.15
Current children cumulated vsize (Kb) 261192

[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78842 0 0 0 119389 325 0 0 25 0 1 0 1796760343 265412608 53357 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64798 53357 145 145 0 64653 0
[pid=9374] vsize: 259192
Current children cumulated CPU time (s) 1197.15
Current children cumulated vsize (Kb) 261316

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78854 0 0 0 120389 325 0 0 25 0 1 0 1796760343 265457664 53369 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64809 53369 145 145 0 64664 0
[pid=9374] vsize: 259236
Current children cumulated CPU time (s) 1207.15
Current children cumulated vsize (Kb) 261360



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 9374
Raw data (/proc/9370/stat): 9370 (minisat+_script) S 9369 9370 15400 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796760338 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9370/statm): 531 226 485 147 0 384 0
[pid=9370] vsize: 2124
Raw data (/proc/9374/stat): 9374 (minisat+_64-bit) R 9370 9370 15400 0 -1 0 78854 0 0 0 120389 325 0 0 25 0 1 0 1796760343 265457664 53369 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9374/statm): 64809 53369 145 145 0 64664 0
[pid=9374] vsize: 259236
Current children cumulated CPU time (s) 1207.15
Current children cumulated vsize (Kb) 261360

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

Child status: 0
Real time (s): 1210.18
CPU time (s): 1207.26
CPU user time (s): 1203.89
CPU system time (s): 3.36249
CPU usage (%): 99.7583
Max. virtual memory (cumulated for all children) (Kb): 261360

Verifier Data

ERROR: no interpretation found !