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/MIPLIB/miplib3/normalized-mps-v2-13-7-mitre.opb
MD5SUMcb52c3dd346b4d656b5e715b686fba39
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 8562
Optimality of the best value was proved NO
Number of terms in the objective function 9324
Biggest coefficient in the objective function 213
Number of bits for the biggest coefficient in the objective function 8
Sum of the numbers in the objective function 909647
Number of bits of the sum of numbers in the objective function 20
Biggest number in a constraint 1069
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 909647
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.55
Number of variables10724
Total number of constraints12778
Number of constraints which are clauses140
Number of constraints which are cardinality constraints (but not clauses)12255
Number of constraints which are nor clauses,nor cardinality constraints383
Minimum length of a constraint1
Maximum length of a constraint98

Trace number 6217

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        908956 kB
Buffers:         17104 kB
Cached:          80716 kB
SwapCached:        848 kB
Active:          24244 kB
Inactive:        76180 kB
HighTotal:      131008 kB
HighFree:        49224 kB
LowTotal:       903652 kB
LowFree:        859732 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5508 kB
Slab:            19720 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:50:06 (client local time) WITH STATUS 0 IN 1208.74 SECONDS
stats: 3373 7 1208.74 0

Solver Data

c Parsing PB file...
c Converting 2045 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .................................................................sssssssssssssssssssssss.ss.sss.s.sssssssssssssssssssssssssssssssssssssssssss.ssssss.sss.sssss.sssssssssss.ssss.ss...........................................................................
c ---[2147]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2146]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2145]---> BDD-cost:   41
c ---[2134]---> BDD-cost:   41
c ---[2123]---> BDD-cost:   41
c ---[2112]---> BDD-cost:   41
c ---[2104]---> BDD-cost:   41
c ---[2103]---> BDD-cost:   41
c ---[2102]---> BDD-cost:   41
c ---[2101]---> BDD-cost:   67
c ---[2100]---> BDD-cost:   67
c ---[2099]---> BDD-cost:   67
c ---[2098]---> BDD-cost:   67
c ---[2097]---> BDD-cost:   67
c ---[2096]---> BDD-cost:   41
c ---[2095]---> BDD-cost:   67
c ---[2094]---> BDD-cost:   67
c ---[2093]---> BDD-cost:   67
c ---[2092]---> BDD-cost:   67
c ---[2091]---> BDD-cost:   67
c ---[2090]---> BDD-cost:   67
c ---[2089]---> BDD-cost:   67
c ---[2088]---> BDD-cost:   67
c ---[2087]---> BDD-cost:   67
c ---[2086]---> BDD-cost:   67
c ---[2085]---> BDD-cost:   41
c ---[2084]---> BDD-cost:   67
c ---[2083]---> BDD-cost:   67
c ---[2082]---> BDD-cost:   67
c ---[2081]---> BDD-cost:   67
c ---[2080]---> BDD-cost:   67
c ---[2079]---> BDD-cost:   67
c ---[2078]---> BDD-cost:   67
c ---[2077]---> BDD-cost:   67
c ---[2076]---> BDD-cost:   67
c ---[2075]---> BDD-cost:   67
c ---[2074]---> BDD-cost:   41
c ---[2073]---> BDD-cost:   67
c ---[2072]---> BDD-cost:   67
c ---[2071]---> BDD-cost:   67
c ---[2070]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2069]---> BDD-cost:   41
c ---[2068]---> BDD-cost:   41
c ---[2067]---> BDD-cost:   41
c ---[2066]---> BDD-cost:   26
c ---[2065]---> BDD-cost:   26
c ---[2064]---> BDD-cost:   26
c ---[2063]---> BDD-cost:   26
c ---[2062]---> BDD-cost:   26
c ---[2061]---> BDD-cost:   26
c ---[2060]---> BDD-cost:   26
c ---[2059]---> BDD-cost:   26
c ---[2058]---> BDD-cost:   26
c ---[2057]---> BDD-cost:   26
c ---[2056]---> BDD-cost:   26
c ---[2055]---> BDD-cost:   26
c ---[2054]---> BDD-cost:   26
c ---[2053]---> BDD-cost:   26
c ---[2052]---> BDD-cost:   26
c ---[2051]---> BDD-cost:   26
c ---[2050]---> BDD-cost:   26
c ---[2049]---> BDD-cost:   26
c ---[2048]---> BDD-cost:   26
c ---[2047]---> BDD-cost:   26
c ---[2046]---> BDD-cost:   26
c ---[2045]---> BDD-cost:   26
c ---[2044]---> BDD-cost:   26
c ---[2043]---> BDD-cost:   26
c ---[2042]---> BDD-cost:   26
c ---[2041]---> BDD-cost:   26
c ---[2040]---> BDD-cost:   26
c ---[2039]---> BDD-cost:   26
c ---[2038]---> BDD-cost:    7
c ---[2037]---> BDD-cost:    7
c ---[2036]---> BDD-cost:    7
c ---[2035]---> BDD-cost:    7
c ---[2034]---> BDD-cost:    7
c ---[2033]---> BDD-cost:    7
c ---[2032]---> BDD-cost:    7
c ---[2031]---> BDD-cost:    7
c ---[2030]---> BDD-cost:    7
c ---[2029]---> BDD-cost:    7
c ---[2028]---> BDD-cost:    7
c ---[2027]---> BDD-cost:    7
c ---[2026]---> BDD-cost:    7
c ---[2025]---> BDD-cost:    7
c ---[2024]---> BDD-cost:    7
c ---[2023]---> BDD-cost:    7
c ---[2022]---> BDD-cost:    7
c ---[2021]---> BDD-cost:    7
c ---[2020]---> BDD-cost:    7
c ---[2019]---> BDD-cost:    7
c ---[2018]---> BDD-cost:    7
c ---[2017]---> BDD-cost:    7
c ---[2016]---> BDD-cost:    7
c ---[2015]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2014]---> BDD-cost:    7
c ---[2013]---> BDD-cost:    7
c ---[2012]---> BDD-cost:    7
c ---[2011]---> BDD-cost:    7
c ---[2010]---> BDD-cost:    7
c ---[1981]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1980]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1979]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1978]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1977]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1976]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1975]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1974]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1973]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1972]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1971]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1970]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1969]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1968]---> Sorter-cost: 6025     Base: 3 5 3 3 5
c ---[1967]---> Sorter-cost: 6024     Base: 3 5 3 3 5
c ---[1966]---> Sorter-cost: 6026     Base: 5 3 3 3 5
c ---[1965]---> Sorter-cost: 6027     Base: 5 3 3 3 5
c ---[1964]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1963]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1962]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1961]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1960]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1959]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1958]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1957]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1956]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[1955]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1954]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1953]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1952]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1951]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1950]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1949]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1948]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1947]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1946]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1945]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1944]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1943]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1942]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1941]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[1940]---> Adder-cost: 448   maxlim: 8073   bits: 14/13
c ---[1939]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1938]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1937]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1936]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1935]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1934]---> Sorter-cost: 6024     Base: 3 5 3 3 5
c ---[1933]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1932]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1931]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1930]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1929]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1928]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1927]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1926]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1925]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1924]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1923]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1922]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1921]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1920]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1919]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1918]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1917]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1916]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1915]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1914]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1913]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1912]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1911]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1910]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1909]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1908]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1907]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1906]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1905]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1904]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1903]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1902]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1901]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1900]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1899]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1898]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1897]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1896]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1895]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1894]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1893]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1892]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1891]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1890]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1889]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1888]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1887]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1886]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1885]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1884]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1883]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1882]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1881]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1880]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1879]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1878]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1877]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1876]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1875]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1874]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1873]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1872]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1871]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1870]---> Adder-cost: 462   maxlim: 8078   bits: 14/13
c ---[1869]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1868]---> Adder-cost: 462   maxlim: 8083   bits: 14/13
c ---[1867]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1866]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1865]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1864]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1863]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1862]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1861]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1860]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1859]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1858]---> BDD-cost:   20
c ---[1857]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1856]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1855]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1854]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1853]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1852]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1851]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1850]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1849]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1848]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1847]---> BDD-cost:   20
c ---[1846]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1845]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1844]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1843]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1842]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1841]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1840]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1839]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1838]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1837]---> Sorter-cost: 4826     Base: 3 5 2 2 2 2 3
c ---[1836]---> BDD-cost:   20
c ---[1835]---> Sorter-cost: 4825     Base: 3 5 2 2 2 2 3
c ---[1834]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1833]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1832]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1831]---> Adder-cost: 424   maxlim: 4849   bits: 14/13
c ---[1830]---> Adder-cost: 424   maxlim: 4852   bits: 14/13
c ---[1829]---> Sorter-cost: 6056     Base: 5 3 3 3 5
c ---[1828]---> Sorter-cost: 6055     Base: 5 3 3 3 5
c ---[1827]---> Sorter-cost: 6056     Base: 5 3 3 3 5
c ---[1826]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1825]---> BDD-cost:   20
c ---[1824]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1823]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1822]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1821]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1820]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1819]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1818]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1817]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1816]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1815]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1814]---> BDD-cost:   20
c ---[1813]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1812]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1811]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1810]---> Adder-cost: 448   maxlim: 8063   bits: 14/13
c ---[1809]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[1808]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1807]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1806]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1805]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1804]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1803]---> BDD-cost:   20
c ---[1802]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1801]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1800]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1799]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1798]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1797]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1796]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1795]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1794]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1793]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1792]---> BDD-cost:   20
c ---[1791]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1790]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1789]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1788]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1787]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1786]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1785]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1784]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1783]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1782]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1781]---> BDD-cost:   20
c ---[1780]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1779]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1778]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1777]---> Sorter-cost: 6056     Base: 5 3 3 3 5
c ---[1776]---> Sorter-cost: 6055     Base: 5 3 3 3 5
c ---[1775]---> Sorter-cost: 6056     Base: 5 3 3 3 5
c ---[1774]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1773]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1772]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1771]---> Sorter-cost: 6056     Base: 5 3 3 3 5
c ---[1770]---> BDD-cost:   20
c ---[1769]---> Sorter-cost: 6055     Base: 5 3 3 3 5
c ---[1768]---> Sorter-cost: 6056     Base: 5 3 3 3 5
c ---[1767]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1766]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1765]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1764]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1763]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1762]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1761]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1760]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1759]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1758]---> BDD-cost:   20
c ---[1757]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1756]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1755]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1754]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1753]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1752]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1751]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1750]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1749]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[1748]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1747]---> BDD-cost:   20
c ---[1746]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1745]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1744]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1743]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1742]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1741]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1740]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1739]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1738]---> Sorter-cost: 6027     Base: 5 3 3 3 5
c ---[1737]---> Sorter-cost: 6026     Base: 5 3 3 3 5
c ---[1736]---> BDD-cost:   20
c ---[1735]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1734]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1733]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1732]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1731]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1730]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1729]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1728]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1727]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1726]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1725]---> BDD-cost:   20
c ---[1724]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1723]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1722]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1721]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1720]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1719]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1718]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1717]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1716]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1715]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1714]---> BDD-cost:   20
c ---[1713]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1712]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1711]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1710]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1709]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1708]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1707]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1706]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1705]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1704]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1703]---> BDD-cost:   20
c ---[1702]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1701]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1700]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1699]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1698]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1697]---> Sorter-cost: 6024     Base: 3 5 3 3 5
c ---[1696]---> Sorter-cost: 6024     Base: 3 5 3 3 5
c ---[1695]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1694]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1692]---> BDD-cost:   53
c ---[1691]---> BDD-cost:   20
c ---[1689]---> BDD-cost:   53
c ---[1687]---> BDD-cost:   53
c ---[1685]---> BDD-cost:   53
c ---[1683]---> BDD-cost:   53
c ---[1681]---> BDD-cost:   53
c ---[1679]---> BDD-cost:   53
c ---[1677]---> BDD-cost:   53
c ---[1675]---> BDD-cost:   53
c ---[1673]---> BDD-cost:   53
c ---[1671]---> BDD-cost:   53
c ---[1670]---> BDD-cost:   20
c ---[1668]---> BDD-cost:   53
c ---[1666]---> BDD-cost:   53
c ---[1664]---> BDD-cost:   53
c ---[1662]---> BDD-cost:   53
c ---[1660]---> BDD-cost:   53
c ---[1658]---> BDD-cost:   53
c ---[1656]---> BDD-cost:   53
c ---[1654]---> BDD-cost:   53
c ---[1652]---> BDD-cost:   53
c ---[1650]---> BDD-cost:   53
c ---[1649]---> BDD-cost:   20
c ---[1647]---> BDD-cost:   53
c ---[1645]---> BDD-cost:   53
c ---[1643]---> BDD-cost:   53
c ---[1641]---> BDD-cost:   53
c ---[1639]---> BDD-cost:   53
c ---[1637]---> BDD-cost:   53
c ---[1635]---> BDD-cost:   53
c ---[1633]---> BDD-cost:   53
c ---[1631]---> BDD-cost:   53
c ---[1629]---> BDD-cost:   53
c ---[1628]---> BDD-cost:   20
c ---[1626]---> BDD-cost:   53
c ---[1624]---> BDD-cost:   53
c ---[1622]---> BDD-cost:   53
c ---[1620]---> BDD-cost:   53
c ---[1618]---> BDD-cost:   53
c ---[1616]---> BDD-cost:   53
c ---[1614]---> BDD-cost:   53
c ---[1612]---> BDD-cost:   53
c ---[1610]---> BDD-cost:   53
c ---[1608]---> BDD-cost:   53
c ---[1607]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1606]---> BDD-cost:   20
c ---[1604]---> BDD-cost:   53
c ---[1602]---> BDD-cost:   53
c ---[1600]---> BDD-cost:   53
c ---[1598]---> BDD-cost:   53
c ---[1596]---> BDD-cost:   53
c ---[1594]---> BDD-cost:   53
c ---[1592]---> BDD-cost:   53
c ---[1590]---> BDD-cost:   53
c ---[1588]---> BDD-cost:   53
c ---[1586]---> BDD-cost:   53
c ---[1585]---> BDD-cost:   20
c ---[1583]---> BDD-cost:   53
c ---[1581]---> BDD-cost:   53
c ---[1579]---> BDD-cost:   53
c ---[1577]---> BDD-cost:   53
c ---[1575]---> BDD-cost:   53
c ---[1573]---> BDD-cost:   53
c ---[1571]---> BDD-cost:   53
c ---[1569]---> BDD-cost:   53
c ---[1567]---> BDD-cost:   53
c ---[1565]---> BDD-cost:   53
c ---[1564]---> BDD-cost:   20
c ---[1562]---> BDD-cost:   53
c ---[1560]---> BDD-cost:   53
c ---[1558]---> BDD-cost:   53
c ---[1556]---> BDD-cost:   53
c ---[1554]---> BDD-cost:   53
c ---[1552]---> BDD-cost:   53
c ---[1550]---> BDD-cost:   53
c ---[1548]---> BDD-cost:   53
c ---[1546]---> BDD-cost:   53
c ---[1544]---> BDD-cost:   53
c ---[1543]---> BDD-cost:   20
c ---[1541]---> BDD-cost:   53
c ---[1539]---> BDD-cost:   53
c ---[1537]---> BDD-cost:   53
c ---[1535]---> BDD-cost:   53
c ---[1533]---> BDD-cost:   53
c ---[1531]---> BDD-cost:   53
c ---[1529]---> BDD-cost:   53
c ---[1527]---> BDD-cost:   53
c ---[1525]---> BDD-cost:   53
c ---[1523]---> BDD-cost:   53
c ---[1522]---> BDD-cost:   20
c ---[1520]---> BDD-cost:   53
c ---[1518]---> BDD-cost:   53
c ---[1516]---> BDD-cost:   53
c ---[1514]---> BDD-cost:   53
c ---[1512]---> BDD-cost:   53
c ---[1510]---> BDD-cost:   53
c ---[1508]---> BDD-cost:   53
c ---[1506]---> BDD-cost:   53
c ---[1504]---> BDD-cost:   53
c ---[1502]---> BDD-cost:   53
c ---[1501]---> BDD-cost:   20
c ---[1499]---> BDD-cost:   53
c ---[1497]---> BDD-cost:   53
c ---[1495]---> BDD-cost:   53
c ---[1493]---> BDD-cost:   53
c ---[1491]---> BDD-cost:   53
c ---[1489]---> BDD-cost:   53
c ---[1487]---> BDD-cost:   53
c ---[1485]---> BDD-cost:   53
c ---[1483]---> BDD-cost:   53
c ---[1481]---> BDD-cost:   53
c ---[1480]---> BDD-cost:   20
c ---[1478]---> BDD-cost:   53
c ---[1476]---> BDD-cost:   53
c ---[1474]---> BDD-cost:   53
c ---[1472]---> BDD-cost:   53
c ---[1470]---> BDD-cost:   53
c ---[1468]---> BDD-cost:   53
c ---[1466]---> BDD-cost:   53
c ---[1464]---> BDD-cost:   53
c ---[1462]---> BDD-cost:   53
c ---[1460]---> BDD-cost:   53
c ---[1459]---> BDD-cost:   20
c ---[1457]---> BDD-cost:   53
c ---[1455]---> BDD-cost:   53
c ---[1453]---> BDD-cost:   53
c ---[1451]---> BDD-cost:   53
c ---[1449]---> BDD-cost:   53
c ---[1447]---> BDD-cost:   53
c ---[1445]---> BDD-cost:   53
c ---[1443]---> BDD-cost:   53
c ---[1441]---> BDD-cost:   53
c ---[1439]---> BDD-cost:   53
c ---[1438]---> BDD-cost:   20
c ---[1436]---> BDD-cost:   53
c ---[1434]---> BDD-cost:   53
c ---[1432]---> BDD-cost:   53
c ---[1430]---> BDD-cost:   53
c ---[1428]---> BDD-cost:   53
c ---[1426]---> BDD-cost:   53
c ---[1424]---> BDD-cost:   53
c ---[1422]---> BDD-cost:   53
c ---[1420]---> BDD-cost:   53
c ---[1418]---> BDD-cost:   53
c ---[1417]---> BDD-cost:   23
c ---[1415]---> BDD-cost:   53
c ---[1413]---> BDD-cost:   53
c ---[1411]---> BDD-cost:   53
c ---[1409]---> BDD-cost:   53
c ---[1407]---> BDD-cost:   53
c ---[1405]---> BDD-cost:   53
c ---[1403]---> BDD-cost:   53
c ---[1401]---> BDD-cost:   53
c ---[1399]---> BDD-cost:   53
c ---[1397]---> BDD-cost:   53
c ---[1396]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1395]---> BDD-cost:   23
c ---[1393]---> BDD-cost:   53
c ---[1391]---> BDD-cost:   53
c ---[1389]---> BDD-cost:   53
c ---[1387]---> BDD-cost:   53
c ---[1385]---> BDD-cost:   53
c ---[1383]---> BDD-cost:   53
c ---[1381]---> BDD-cost:   53
c ---[1379]---> BDD-cost:   53
c ---[1377]---> BDD-cost:   53
c ---[1375]---> BDD-cost:   53
c ---[1374]---> BDD-cost:   23
c ---[1372]---> BDD-cost:   53
c ---[1370]---> BDD-cost:   53
c ---[1368]---> BDD-cost:   53
c ---[1366]---> BDD-cost:   53
c ---[1364]---> BDD-cost:   53
c ---[1362]---> BDD-cost:   53
c ---[1360]---> BDD-cost:   53
c ---[1358]---> BDD-cost:   53
c ---[1356]---> BDD-cost:   53
c ---[1354]---> BDD-cost:   53
c ---[1353]---> BDD-cost:   23
c ---[1351]---> BDD-cost:   53
c ---[1349]---> BDD-cost:   53
c ---[1347]---> BDD-cost:   53
c ---[1345]---> BDD-cost:   53
c ---[1343]---> BDD-cost:   53
c ---[1341]---> BDD-cost:   53
c ---[1339]---> BDD-cost:   53
c ---[1337]---> BDD-cost:   53
c ---[1335]---> BDD-cost:   53
c ---[1333]---> BDD-cost:   53
c ---[1332]---> BDD-cost:   23
c ---[1330]---> BDD-cost:   53
c ---[1328]---> BDD-cost:   53
c ---[1326]---> BDD-cost:   53
c ---[1324]---> BDD-cost:   53
c ---[1322]---> BDD-cost:   53
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:   53
c ---[1316]---> BDD-cost:   53
c ---[1314]---> BDD-cost:   53
c ---[1312]---> BDD-cost:   53
c ---[1311]---> BDD-cost:   23
c ---[1309]---> BDD-cost:   53
c ---[1307]---> BDD-cost:   53
c ---[1305]---> BDD-cost:   53
c ---[1303]---> BDD-cost:   53
c ---[1301]---> BDD-cost:   53
c ---[1299]---> BDD-cost:   53
c ---[1297]---> BDD-cost:   53
c ---[1295]---> BDD-cost:   53
c ---[1293]---> BDD-cost:   53
c ---[1291]---> BDD-cost:   53
c ---[1290]---> BDD-cost:   23
c ---[1288]---> BDD-cost:   53
c ---[1286]---> BDD-cost:   53
c ---[1284]---> BDD-cost:   53
c ---[1282]---> BDD-cost:   53
c ---[1280]---> BDD-cost:   53
c ---[1278]---> BDD-cost:   53
c ---[1276]---> BDD-cost:   53
c ---[1274]---> BDD-cost:   53
c ---[1272]---> BDD-cost:   53
c ---[1270]---> BDD-cost:   53
c ---[1269]---> BDD-cost:   23
c ---[1267]---> BDD-cost:   53
c ---[1265]---> BDD-cost:   53
c ---[1263]---> BDD-cost:   53
c ---[1261]---> BDD-cost:   53
c ---[1259]---> BDD-cost:   53
c ---[1257]---> BDD-cost:   53
c ---[1255]---> BDD-cost:   53
c ---[1253]---> BDD-cost:   53
c ---[1251]---> BDD-cost:   53
c ---[1249]---> BDD-cost:   53
c ---[1248]---> BDD-cost:   23
c ---[1246]---> BDD-cost:   53
c ---[1244]---> BDD-cost:   53
c ---[1242]---> BDD-cost:   53
c ---[1240]---> BDD-cost:   53
c ---[1238]---> BDD-cost:   53
c ---[1236]---> BDD-cost:   53
c ---[1234]---> BDD-cost:   53
c ---[1232]---> BDD-cost:   53
c ---[1230]---> BDD-cost:   53
c ---[1228]---> BDD-cost:   53
c ---[1227]---> BDD-cost:   23
c ---[1225]---> BDD-cost:   53
c ---[1223]---> BDD-cost:   53
c ---[1221]---> BDD-cost:   53
c ---[1219]---> BDD-cost:   53
c ---[1217]---> BDD-cost:   53
c ---[1215]---> BDD-cost:   53
c ---[1213]---> BDD-cost:   53
c ---[1211]---> BDD-cost:   53
c ---[1209]---> BDD-cost:   53
c ---[1207]---> BDD-cost:   53
c ---[1206]---> BDD-cost:   23
c ---[1204]---> BDD-cost:   53
c ---[1202]---> BDD-cost:   53
c ---[1200]---> BDD-cost:   53
c ---[1198]---> BDD-cost:   53
c ---[1196]---> BDD-cost:   53
c ---[1194]---> BDD-cost:   53
c ---[1192]---> BDD-cost:   53
c ---[1190]---> BDD-cost:   53
c ---[1188]---> BDD-cost:   53
c ---[1186]---> BDD-cost:   53
c ---[1185]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1184]---> BDD-cost:   23
c ---[1182]---> BDD-cost:   53
c ---[1180]---> BDD-cost:   53
c ---[1178]---> BDD-cost:   53
c ---[1176]---> BDD-cost:   53
c ---[1174]---> BDD-cost:   53
c ---[1172]---> BDD-cost:   53
c ---[1170]---> BDD-cost:   53
c ---[1168]---> BDD-cost:   53
c ---[1166]---> BDD-cost:   53
c ---[1164]---> BDD-cost:   53
c ---[1163]---> BDD-cost:   23
c ---[1161]---> BDD-cost:   53
c ---[1159]---> BDD-cost:   53
c ---[1157]---> BDD-cost:   53
c ---[1155]---> BDD-cost:   53
c ---[1153]---> BDD-cost:   53
c ---[1151]---> BDD-cost:   53
c ---[1149]---> BDD-cost:   53
c ---[1147]---> BDD-cost:   53
c ---[1145]---> BDD-cost:   53
c ---[1143]---> BDD-cost:   53
c ---[1142]---> BDD-cost:   23
c ---[1140]---> BDD-cost:   53
c ---[1138]---> BDD-cost:   53
c ---[1136]---> BDD-cost:   53
c ---[1134]---> BDD-cost:   53
c ---[1132]---> BDD-cost:   53
c ---[1130]---> BDD-cost:   53
c ---[1128]---> BDD-cost:   53
c ---[1126]---> BDD-cost:   53
c ---[1124]---> BDD-cost:   53
c ---[1122]---> BDD-cost:   53
c ---[1121]---> BDD-cost:   23
c ---[1119]---> BDD-cost:   53
c ---[1117]---> BDD-cost:   53
c ---[1115]---> BDD-cost:   53
c ---[1113]---> BDD-cost:   53
c ---[1111]---> BDD-cost:   53
c ---[1109]---> BDD-cost:   53
c ---[1107]---> BDD-cost:   53
c ---[1105]---> BDD-cost:   53
c ---[1103]---> BDD-cost:   53
c ---[1101]---> BDD-cost:   53
c ---[1100]---> BDD-cost:   23
c ---[1098]---> BDD-cost:   53
c ---[1096]---> BDD-cost:   53
c ---[1094]---> BDD-cost:   53
c ---[1092]---> BDD-cost:   53
c ---[1090]---> BDD-cost:   53
c ---[1088]---> BDD-cost:   53
c ---[1086]---> BDD-cost:   53
c ---[1084]---> BDD-cost:   53
c ---[1082]---> BDD-cost:   53
c ---[1080]---> BDD-cost:   53
c ---[1079]---> BDD-cost:   23
c ---[1077]---> BDD-cost:   53
c ---[1075]---> BDD-cost:   53
c ---[1073]---> BDD-cost:   53
c ---[1071]---> BDD-cost:   53
c ---[1069]---> BDD-cost:   53
c ---[1067]---> BDD-cost:   53
c ---[1065]---> BDD-cost:   53
c ---[1063]---> BDD-cost:   53
c ---[1061]---> BDD-cost:   53
c ---[1059]---> BDD-cost:   53
c ---[1058]---> BDD-cost:   23
c ---[1056]---> BDD-cost:   53
c ---[1054]---> BDD-cost:   53
c ---[1052]---> BDD-cost:   53
c ---[1050]---> BDD-cost:   53
c ---[1048]---> BDD-cost:   53
c ---[1046]---> BDD-cost:   53
c ---[1044]---> BDD-cost:   53
c ---[1042]---> BDD-cost:   53
c ---[1040]---> BDD-cost:   53
c ---[1038]---> BDD-cost:   53
c ---[1037]---> BDD-cost:   23
c ---[1035]---> BDD-cost:   53
c ---[1033]---> BDD-cost:   53
c ---[1031]---> BDD-cost:   53
c ---[1029]---> BDD-cost:   53
c ---[1027]---> BDD-cost:   53
c ---[1025]---> BDD-cost:   53
c ---[1023]---> BDD-cost:   53
c ---[1021]---> BDD-cost:   53
c ---[1019]---> BDD-cost:   53
c ---[1017]---> BDD-cost:   53
c ---[1016]---> BDD-cost:   23
c ---[1014]---> BDD-cost:   53
c ---[1012]---> BDD-cost:   53
c ---[1010]---> BDD-cost:   53
c ---[1008]---> BDD-cost:   53
c ---[1006]---> BDD-cost:   53
c ---[1004]---> BDD-cost:   53
c ---[1002]---> BDD-cost:   53
c ---[1000]---> BDD-cost:   53
c ---[ 998]---> BDD-cost:   53
c ---[ 996]---> BDD-cost:   53
c ---[ 995]---> BDD-cost:   23
c ---[ 993]---> BDD-cost:   53
c ---[ 991]---> BDD-cost:   53
c ---[ 989]---> BDD-cost:   53
c ---[ 987]---> BDD-cost:   53
c ---[ 985]---> BDD-cost:   53
c ---[ 983]---> BDD-cost:   53
c ---[ 981]---> BDD-cost:   53
c ---[ 979]---> BDD-cost:   53
c ---[ 977]---> BDD-cost:   53
c ---[ 975]---> BDD-cost:   53
c ---[ 974]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 973]---> BDD-cost:   23
c ---[ 971]---> BDD-cost:   53
c ---[ 969]---> BDD-cost:   53
c ---[ 967]---> BDD-cost:   53
c ---[ 965]---> BDD-cost:   53
c ---[ 963]---> BDD-cost:   53
c ---[ 961]---> BDD-cost:   53
c ---[ 959]---> BDD-cost:   53
c ---[ 957]---> BDD-cost:   53
c ---[ 955]---> BDD-cost:   53
c ---[ 953]---> BDD-cost:   53
c ---[ 952]---> BDD-cost:   23
c ---[ 950]---> BDD-cost:   53
c ---[ 948]---> BDD-cost:   53
c ---[ 946]---> BDD-cost:   53
c ---[ 944]---> BDD-cost:   53
c ---[ 942]---> BDD-cost:   53
c ---[ 940]---> BDD-cost:   53
c ---[ 938]---> BDD-cost:   53
c ---[ 936]---> BDD-cost:   53
c ---[ 934]---> BDD-cost:   53
c ---[ 932]---> BDD-cost:   53
c ---[ 931]---> BDD-cost:   23
c ---[ 929]---> BDD-cost:   53
c ---[ 927]---> BDD-cost:   53
c ---[ 925]---> BDD-cost:   53
c ---[ 923]---> BDD-cost:   53
c ---[ 921]---> BDD-cost:   53
c ---[ 919]---> BDD-cost:   53
c ---[ 917]---> BDD-cost:   53
c ---[ 915]---> BDD-cost:   53
c ---[ 913]---> BDD-cost:   53
c ---[ 911]---> BDD-cost:   53
c ---[ 910]---> BDD-cost:   23
c ---[ 908]---> BDD-cost:   53
c ---[ 906]---> BDD-cost:   53
c ---[ 904]---> BDD-cost:   53
c ---[ 902]---> BDD-cost:   53
c ---[ 900]---> BDD-cost:   53
c ---[ 898]---> BDD-cost:   53
c ---[ 896]---> BDD-cost:   53
c ---[ 894]---> BDD-cost:   53
c ---[ 892]---> BDD-cost:   53
c ---[ 890]---> BDD-cost:   53
c ---[ 889]---> BDD-cost:   23
c ---[ 887]---> BDD-cost:   53
c ---[ 885]---> BDD-cost:   53
c ---[ 876]---> BDD-cost:   23
c ---[ 865]---> BDD-cost:   23
c ---[ 854]---> BDD-cost:   17
c ---[ 843]---> BDD-cost:   17
c ---[ 832]---> BDD-cost:   17
c ---[ 821]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 820]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 819]---> BDD-cost:   17
c ---[ 808]---> BDD-cost:   17
c ---[ 797]---> BDD-cost:   17
c ---[ 786]---> BDD-cost:   17
c ---[ 775]---> BDD-cost:   17
c ---[ 764]---> BDD-cost:   17
c ---[ 758]---> BDD-cost:   17
c ---[ 757]---> BDD-cost:   17
c ---[ 756]---> BDD-cost:   17
c ---[ 755]---> BDD-cost:   17
c ---[ 754]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 753]---> BDD-cost:   17
c ---[ 752]---> BDD-cost:   17
c ---[ 751]---> BDD-cost:   17
c ---[ 750]---> BDD-cost:   17
c ---[ 749]---> BDD-cost:   17
c ---[ 748]---> BDD-cost:   17
c ---[ 747]---> BDD-cost:   17
c ---[ 746]---> BDD-cost:   17
c ---[ 745]---> BDD-cost:   17
c ---[ 744]---> BDD-cost:   17
c ---[ 743]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 742]---> BDD-cost:   17
c ---[ 741]---> BDD-cost:   17
c ---[ 740]---> BDD-cost:   17
c ---[ 739]---> BDD-cost:   17
c ---[ 738]---> BDD-cost:   17
c ---[ 737]---> BDD-cost:    5
c ---[ 736]---> BDD-cost:    5
c ---[ 735]---> BDD-cost:    5
c ---[ 734]---> BDD-cost:    5
c ---[ 733]---> BDD-cost:    5
c ---[ 732]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 731]---> BDD-cost:    5
c ---[ 730]---> BDD-cost:    5
c ---[ 729]---> BDD-cost:    5
c ---[ 728]---> BDD-cost:    5
c ---[ 727]---> BDD-cost:    5
c ---[ 726]---> BDD-cost:    5
c ---[ 725]---> BDD-cost:    5
c ---[ 724]---> BDD-cost:    5
c ---[ 723]---> BDD-cost:    5
c ---[ 722]---> BDD-cost:    5
c ---[ 721]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 720]---> BDD-cost:    5
c ---[ 719]---> BDD-cost:    5
c ---[ 718]---> BDD-cost:    5
c ---[ 717]---> BDD-cost:    5
c ---[ 716]---> BDD-cost:    5
c ---[ 715]---> BDD-cost:    5
c ---[ 714]---> BDD-cost:    5
c ---[ 713]---> BDD-cost:    5
c ---[ 712]---> BDD-cost:    5
c ---[ 711]---> BDD-cost:    5
c ---[ 710]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 709]---> BDD-cost:    5
c ---[ 708]---> BDD-cost:    5
c ---[ 707]---> BDD-cost:    5
c ---[ 706]---> BDD-cost:   14
c ---[ 705]---> BDD-cost:   14
c ---[ 704]---> BDD-cost:   14
c ---[ 703]---> BDD-cost:   14
c ---[ 702]---> BDD-cost:   14
c ---[ 701]---> BDD-cost:   14
c ---[ 700]---> BDD-cost:   14
c ---[ 699]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 698]---> BDD-cost:   14
c ---[ 697]---> BDD-cost:   14
c ---[ 696]---> BDD-cost:   14
c ---[ 695]---> BDD-cost:   14
c ---[ 694]---> BDD-cost:   14
c ---[ 693]---> BDD-cost:   14
c ---[ 692]---> BDD-cost:   14
c ---[ 691]---> BDD-cost:   14
c ---[ 690]---> BDD-cost:   14
c ---[ 689]---> BDD-cost:   14
c ---[ 688]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 687]---> BDD-cost:   14
c ---[ 686]---> BDD-cost:   14
c ---[ 685]---> BDD-cost:   14
c ---[ 684]---> BDD-cost:   14
c ---[ 683]---> BDD-cost:   14
c ---[ 682]---> BDD-cost:   14
c ---[ 681]---> BDD-cost:   14
c ---[ 680]---> BDD-cost:   14
c ---[ 679]---> BDD-cost:   14
c ---[ 678]---> BDD-cost:   14
c ---[ 677]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 676]---> BDD-cost:   14
c ---[ 675]---> BDD-cost:   17
c ---[ 674]---> BDD-cost:   17
c ---[ 673]---> BDD-cost:   17
c ---[ 672]---> BDD-cost:   17
c ---[ 671]---> BDD-cost:   17
c ---[ 670]---> BDD-cost:   17
c ---[ 669]---> BDD-cost:   17
c ---[ 668]---> BDD-cost:   17
c ---[ 667]---> BDD-cost:   17
c ---[ 666]---> BDD-cost:   32
c ---[ 665]---> BDD-cost:   17
c ---[ 664]---> BDD-cost:   17
c ---[ 663]---> BDD-cost:   17
c ---[ 662]---> BDD-cost:   17
c ---[ 661]---> BDD-cost:   17
c ---[ 660]---> BDD-cost:   17
c ---[ 659]---> BDD-cost:   17
c ---[ 658]---> BDD-cost:   17
c ---[ 657]---> BDD-cost:   17
c ---[ 656]---> BDD-cost:   17
c ---[ 655]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 654]---> BDD-cost:   32
c ---[ 653]---> BDD-cost:   17
c ---[ 652]---> BDD-cost:   17
c ---[ 651]---> BDD-cost:   17
c ---[ 650]---> BDD-cost:   17
c ---[ 649]---> BDD-cost:   17
c ---[ 648]---> BDD-cost:   17
c ---[ 647]---> BDD-cost:   17
c ---[ 646]---> BDD-cost:   17
c ---[ 645]---> BDD-cost:   17
c ---[ 644]---> BDD-cost:   31
c ---[ 643]---> BDD-cost:   32
c ---[ 642]---> BDD-cost:   31
c ---[ 641]---> BDD-cost:   31
c ---[ 640]---> BDD-cost:   31
c ---[ 639]---> BDD-cost:   31
c ---[ 638]---> BDD-cost:   31
c ---[ 637]---> BDD-cost:   31
c ---[ 636]---> BDD-cost:   31
c ---[ 635]---> BDD-cost:   31
c ---[ 634]---> BDD-cost:   31
c ---[ 633]---> BDD-cost:   31
c ---[ 632]---> BDD-cost:   32
c ---[ 631]---> BDD-cost:   31
c ---[ 630]---> BDD-cost:   31
c ---[ 629]---> BDD-cost:   31
c ---[ 628]---> BDD-cost:   31
c ---[ 627]---> BDD-cost:   31
c ---[ 626]---> BDD-cost:   31
c ---[ 625]---> BDD-cost:   31
c ---[ 624]---> BDD-cost:   31
c ---[ 623]---> BDD-cost:   31
c ---[ 622]---> BDD-cost:   31
c ---[ 621]---> BDD-cost:   32
c ---[ 620]---> BDD-cost:   31
c ---[ 619]---> BDD-cost:   31
c ---[ 618]---> BDD-cost:   31
c ---[ 617]---> BDD-cost:   31
c ---[ 616]---> BDD-cost:   31
c ---[ 615]---> BDD-cost:   31
c ---[ 614]---> BDD-cost:   31
c ---[ 613]---> BDD-cost:   32
c ---[ 612]---> BDD-cost:   32
c ---[ 611]---> BDD-cost:   32
c ---[ 605]---> BDD-cost:   32
c ---[ 594]---> BDD-cost:   32
c ---[ 583]---> BDD-cost:   32
c ---[ 579]---> BDD-cost:    7
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:    7
c ---[ 576]---> BDD-cost:    7
c ---[ 575]---> BDD-cost:    7
c ---[ 574]---> BDD-cost:    7
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 571]---> BDD-cost:   32
c ---[ 570]---> BDD-cost:    7
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    7
c ---[ 567]---> BDD-cost:    7
c ---[ 566]---> BDD-cost:    7
c ---[ 565]---> BDD-cost:    7
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    7
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:   32
c ---[ 559]---> BDD-cost:    7
c ---[ 558]---> BDD-cost:    7
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    7
c ---[ 554]---> BDD-cost:    7
c ---[ 553]---> BDD-cost:    7
c ---[ 552]---> BDD-cost:    7
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    7
c ---[ 549]---> BDD-cost:   32
c ---[ 548]---> BDD-cost:    7
c ---[ 547]---> BDD-cost:   32
c ---[ 546]---> BDD-cost:   32
c ---[ 545]---> BDD-cost:   32
c ---[ 544]---> BDD-cost:   32
c ---[ 543]---> BDD-cost:   32
c ---[ 542]---> BDD-cost:   11
c ---[ 541]---> BDD-cost:   11
c ---[ 540]---> BDD-cost:   11
c ---[ 539]---> BDD-cost:   32
c ---[ 538]---> BDD-cost:   11
c ---[ 537]---> BDD-cost:   11
c ---[ 536]---> BDD-cost:   11
c ---[ 535]---> BDD-cost:   11
c ---[ 534]---> BDD-cost:   11
c ---[ 533]---> BDD-cost:   11
c ---[ 532]---> BDD-cost:   11
c ---[ 531]---> BDD-cost:   11
c ---[ 530]---> BDD-cost:   11
c ---[ 529]---> BDD-cost:   11
c ---[ 528]---> BDD-cost:   32
c ---[ 527]---> BDD-cost:   11
c ---[ 526]---> BDD-cost:   11
c ---[ 525]---> BDD-cost:   11
c ---[ 524]---> BDD-cost:   11
c ---[ 523]---> BDD-cost:   11
c ---[ 522]---> BDD-cost:   11
c ---[ 521]---> BDD-cost:   11
c ---[ 520]---> BDD-cost:   11
c ---[ 519]---> BDD-cost:   11
c ---[ 518]---> BDD-cost:   11
c ---[ 517]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 516]---> BDD-cost:   32
c ---[ 515]---> BDD-cost:   11
c ---[ 514]---> BDD-cost:   11
c ---[ 513]---> BDD-cost:   11
c ---[ 512]---> BDD-cost:   11
c ---[ 511]---> BDD-cost:   11
c ---[ 510]---> BDD-cost:   11
c ---[ 509]---> BDD-cost:   11
c ---[ 508]---> BDD-cost:   11
c ---[ 507]---> BDD-cost:   11
c ---[ 506]---> BDD-cost:   11
c ---[ 505]---> BDD-cost:   32
c ---[ 504]---> BDD-cost:   11
c ---[ 503]---> BDD-cost:   11
c ---[ 502]---> BDD-cost:   11
c ---[ 501]---> BDD-cost:   11
c ---[ 500]---> BDD-cost:   11
c ---[ 499]---> BDD-cost:   11
c ---[ 498]---> BDD-cost:   11
c ---[ 497]---> BDD-cost:   11
c ---[ 496]---> BDD-cost:   11
c ---[ 495]---> BDD-cost:   11
c ---[ 494]---> BDD-cost:   32
c ---[ 493]---> BDD-cost:   11
c ---[ 492]---> BDD-cost:   11
c ---[ 491]---> BDD-cost:   11
c ---[ 490]---> BDD-cost:   11
c ---[ 489]---> BDD-cost:   11
c ---[ 488]---> BDD-cost:   11
c ---[ 487]---> BDD-cost:   11
c ---[ 486]---> BDD-cost:   11
c ---[ 485]---> BDD-cost:   11
c ---[ 484]---> BDD-cost:   11
c ---[ 483]---> BDD-cost:   32
c ---[ 482]---> BDD-cost:   11
c ---[ 481]---> BDD-cost:   11
c ---[ 480]---> BDD-cost:   11
c ---[ 479]---> BDD-cost:   11
c ---[ 478]---> BDD-cost:   11
c ---[ 477]---> BDD-cost:   11
c ---[ 476]---> BDD-cost:   11
c ---[ 475]---> BDD-cost:   11
c ---[ 474]---> BDD-cost:   11
c ---[ 473]---> BDD-cost:   11
c ---[ 472]---> BDD-cost:   32
c ---[ 471]---> BDD-cost:   11
c ---[ 470]---> BDD-cost:   11
c ---[ 469]---> BDD-cost:   11
c ---[ 468]---> BDD-cost:   11
c ---[ 467]---> BDD-cost:   11
c ---[ 466]---> BDD-cost:   11
c ---[ 465]---> BDD-cost:   11
c ---[ 464]---> BDD-cost:   11
c ---[ 463]---> BDD-cost:   11
c ---[ 462]---> BDD-cost:   11
c ---[ 461]---> BDD-cost:   32
c ---[ 460]---> BDD-cost:   11
c ---[ 459]---> BDD-cost:   11
c ---[ 458]---> BDD-cost:   11
c ---[ 457]---> BDD-cost:   11
c ---[ 456]---> BDD-cost:   11
c ---[ 455]---> BDD-cost:   11
c ---[ 454]---> BDD-cost:   11
c ---[ 453]---> BDD-cost:   11
c ---[ 452]---> BDD-cost:   11
c ---[ 451]---> BDD-cost:   11
c ---[ 450]---> BDD-cost:   32
c ---[ 449]---> BDD-cost:   11
c ---[ 448]---> BDD-cost:   14
c ---[ 447]---> BDD-cost:   14
c ---[ 446]---> BDD-cost:   14
c ---[ 445]---> BDD-cost:   14
c ---[ 444]---> BDD-cost:   14
c ---[ 443]---> BDD-cost:   14
c ---[ 442]---> BDD-cost:   14
c ---[ 441]---> BDD-cost:   14
c ---[ 440]---> BDD-cost:   14
c ---[ 439]---> BDD-cost:   14
c ---[ 438]---> BDD-cost:   14
c ---[ 437]---> BDD-cost:   14
c ---[ 436]---> BDD-cost:   14
c ---[ 435]---> BDD-cost:   14
c ---[ 434]---> BDD-cost:   14
c ---[ 433]---> BDD-cost:   14
c ---[ 432]---> BDD-cost:   14
c ---[ 431]---> BDD-cost:   14
c ---[ 430]---> BDD-cost:   14
c ---[ 429]---> BDD-cost:   14
c ---[ 428]---> BDD-cost:   14
c ---[ 427]---> BDD-cost:   14
c ---[ 426]---> BDD-cost:   14
c ---[ 425]---> BDD-cost:   14
c ---[ 424]---> BDD-cost:   14
c ---[ 423]---> BDD-cost:   14
c ---[ 422]---> BDD-cost:   14
c ---[ 421]---> BDD-cost:   14
c ---[ 420]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 419]---> BDD-cost:   14
c ---[ 418]---> BDD-cost:   14
c ---[ 417]---> BDD-cost:   14
c ---[ 416]---> BDD-cost:   14
c ---[ 415]---> BDD-cost:   14
c ---[ 414]---> BDD-cost:   14
c ---[ 413]---> BDD-cost:   14
c ---[ 412]---> BDD-cost:   14
c ---[ 411]---> BDD-cost:   14
c ---[ 410]---> BDD-cost:   14
c ---[ 409]---> BDD-cost:   14
c ---[ 408]---> BDD-cost:   14
c ---[ 407]---> BDD-cost:   14
c ---[ 406]---> BDD-cost:   14
c ---[ 405]---> BDD-cost:   14
c ---[ 404]---> BDD-cost:   14
c ---[ 403]---> BDD-cost:   14
c ---[ 402]---> BDD-cost:   14
c ---[ 401]---> BDD-cost:   14
c ---[ 400]---> BDD-cost:   14
c ---[ 399]---> BDD-cost:   14
c ---[ 398]---> BDD-cost:   14
c ---[ 397]---> BDD-cost:   14
c ---[ 396]---> BDD-cost:   14
c ---[ 395]---> BDD-cost:   14
c ---[ 394]---> BDD-cost:   14
c ---[ 393]---> BDD-cost:   14
c ---[ 392]---> BDD-cost:   14
c ---[ 391]---> BDD-cost:   17
c ---[ 390]---> BDD-cost:   17
c ---[ 389]---> BDD-cost:   17
c ---[ 388]---> BDD-cost:   17
c ---[ 387]---> BDD-cost:   17
c ---[ 386]---> BDD-cost:   17
c ---[ 385]---> BDD-cost:   17
c ---[ 384]---> BDD-cost:   17
c ---[ 383]---> BDD-cost:   17
c ---[ 382]---> BDD-cost:   17
c ---[ 381]---> BDD-cost:   17
c ---[ 380]---> BDD-cost:   17
c ---[ 379]---> BDD-cost:   17
c ---[ 378]---> BDD-cost:   17
c ---[ 377]---> BDD-cost:   17
c ---[ 376]---> BDD-cost:   17
c ---[ 375]---> BDD-cost:   17
c ---[ 374]---> BDD-cost:   17
c ---[ 373]---> BDD-cost:   17
c ---[ 372]---> BDD-cost:   17
c ---[ 371]---> BDD-cost:   17
c ---[ 370]---> BDD-cost:   17
c ---[ 369]---> BDD-cost:   17
c ---[ 368]---> BDD-cost:   17
c ---[ 367]---> BDD-cost:   17
c ---[ 366]---> BDD-cost:   17
c ---[ 365]---> BDD-cost:   17
c ---[ 364]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 363]---> BDD-cost:   17
c ---[ 362]---> BDD-cost:   14
c ---[ 361]---> BDD-cost:   14
c ---[ 360]---> BDD-cost:   14
c ---[ 359]---> BDD-cost:   14
c ---[ 358]---> BDD-cost:   14
c ---[ 357]---> BDD-cost:   14
c ---[ 356]---> BDD-cost:   14
c ---[ 355]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   14
c ---[ 353]---> BDD-cost:   14
c ---[ 352]---> BDD-cost:   14
c ---[ 351]---> BDD-cost:   14
c ---[ 350]---> BDD-cost:   14
c ---[ 349]---> BDD-cost:   14
c ---[ 348]---> BDD-cost:   14
c ---[ 347]---> BDD-cost:   14
c ---[ 346]---> BDD-cost:   14
c ---[ 345]---> BDD-cost:   14
c ---[ 344]---> BDD-cost:   14
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:   14
c ---[ 341]---> BDD-cost:   14
c ---[ 340]---> BDD-cost:   14
c ---[ 339]---> BDD-cost:   14
c ---[ 338]---> BDD-cost:   14
c ---[ 337]---> BDD-cost:   14
c ---[ 336]---> BDD-cost:   14
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:    5
c ---[ 333]---> BDD-cost:    5
c ---[ 332]---> BDD-cost:    5
c ---[ 331]---> BDD-cost:    5
c ---[ 330]---> BDD-cost:    5
c ---[ 329]---> BDD-cost:    5
c ---[ 328]---> BDD-cost:    5
c ---[ 327]---> BDD-cost:    5
c ---[ 326]---> BDD-cost:    5
c ---[ 325]---> BDD-cost:    5
c ---[ 324]---> BDD-cost:    5
c ---[ 323]---> BDD-cost:    5
c ---[ 322]---> BDD-cost:    5
c ---[ 321]---> BDD-cost:    5
c ---[ 320]---> BDD-cost:    5
c ---[ 319]---> BDD-cost:    5
c ---[ 318]---> BDD-cost:    5
c ---[ 317]---> BDD-cost:    5
c ---[ 316]---> BDD-cost:    5
c ---[ 315]---> BDD-cost:    5
c ---[ 314]---> BDD-cost:    5
c ---[ 313]---> BDD-cost:    5
c ---[ 312]---> BDD-cost:    5
c ---[ 311]---> BDD-cost:    5
c ---[ 310]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    5
c ---[ 308]---> BDD-cost:    5
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:   44
c ---[ 305]---> BDD-cost:   44
c ---[ 304]---> BDD-cost:   44
c ---[ 303]---> BDD-cost:   44
c ---[ 302]---> BDD-cost:   44
c ---[ 301]---> BDD-cost:   44
c ---[ 300]---> BDD-cost:   44
c ---[ 299]---> BDD-cost:   44
c ---[ 298]---> BDD-cost:   44
c ---[ 297]---> BDD-cost:   44
c ---[ 296]---> BDD-cost:   44
c ---[ 295]---> BDD-cost:   44
c ---[ 294]---> BDD-cost:   44
c ---[ 293]---> BDD-cost:   44
c ---[ 292]---> BDD-cost:   44
c ---[ 291]---> BDD-cost:   44
c ---[ 290]---> BDD-cost:   44
c ---[ 289]---> BDD-cost:   44
c ---[ 288]---> BDD-cost:   44
c ---[ 287]---> BDD-cost:   44
c ---[ 286]---> BDD-cost:   44
c ---[ 285]---> BDD-cost:   44
c ---[ 284]---> BDD-cost:   44
c ---[ 283]---> BDD-cost:   44
c ---[ 282]---> BDD-cost:   44
c ---[ 281]---> BDD-cost:   44
c ---[ 280]---> BDD-cost:   44
c ---[ 279]---> BDD-cost:   44
c ---[ 278]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    5
c ---[ 276]---> BDD-cost:    5
c ---[ 275]---> BDD-cost:    5
c ---[ 274]---> BDD-cost:    5
c ---[ 273]---> BDD-cost:    5
c ---[ 272]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    5
c ---[ 270]---> BDD-cost:    5
c ---[ 269]---> BDD-cost:    5
c ---[ 268]---> BDD-cost:    5
c ---[ 267]---> BDD-cost:    5
c ---[ 266]---> BDD-cost:    5
c ---[ 265]---> BDD-cost:    5
c ---[ 264]---> BDD-cost:    5
c ---[ 263]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 262]---> BDD-cost:    5
c ---[ 261]---> BDD-cost:    5
c ---[ 260]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    5
c ---[ 258]---> BDD-cost:    5
c ---[ 257]---> BDD-cost:    5
c ---[ 256]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    5
c ---[ 252]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    5
c ---[ 250]---> BDD-cost:    5
c ---[ 221]---> BDD-cost:   35
c ---[ 220]---> BDD-cost:   35
c ---[ 219]---> BDD-cost:   35
c ---[ 218]---> BDD-cost:   35
c ---[ 217]---> BDD-cost:   35
c ---[ 216]---> BDD-cost:   35
c ---[ 215]---> BDD-cost:   35
c ---[ 214]---> BDD-cost:   35
c ---[ 213]---> BDD-cost:   35
c ---[ 212]---> BDD-cost:   41
c ---[ 211]---> BDD-cost:   35
c ---[ 210]---> BDD-cost:   35
c ---[ 209]---> BDD-cost:   35
c ---[ 208]---> BDD-cost:   35
c ---[ 207]---> BDD-cost:   35
c ---[ 206]---> BDD-cost:   35
c ---[ 205]---> BDD-cost:   35
c ---[ 204]---> BDD-cost:   35
c ---[ 203]---> BDD-cost:   35
c ---[ 202]---> BDD-cost:   35
c ---[ 201]---> BDD-cost:   41
c ---[ 200]---> BDD-cost:   35
c ---[ 199]---> BDD-cost:   35
c ---[ 198]---> BDD-cost:   35
c ---[ 197]---> BDD-cost:   35
c ---[ 196]---> BDD-cost:   35
c ---[ 195]---> BDD-cost:   35
c ---[ 194]---> BDD-cost:   35
c ---[ 193]---> BDD-cost:   35
c ---[ 192]---> BDD-cost:   35
c ---[ 191]---> BDD-cost:   11
c ---[ 190]---> BDD-cost:   41
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   11
c ---[ 184]---> BDD-cost:   11
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   11
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   11
c ---[ 179]---> BDD-cost:   41
c ---[ 178]---> BDD-cost:   11
c ---[ 177]---> BDD-cost:   11
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:   11
c ---[ 173]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   11
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   11
c ---[ 168]---> BDD-cost:   41
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   11
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   11
c ---[ 161]---> BDD-cost:   11
c ---[ 160]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 159]---> BDD-cost:   41
c ---[ 158]---> BDD-cost:   41
c ---[ 157]---> BDD-cost:   41
c ---[ 156]---> BDD-cost:   14
c ---[ 155]---> BDD-cost:   14
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:   14
c ---[ 152]---> BDD-cost:   14
c ---[ 151]---> BDD-cost:   41
c ---[ 150]---> BDD-cost:   14
c ---[ 149]---> BDD-cost:   14
c ---[ 148]---> BDD-cost:   14
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   14
c ---[ 145]---> BDD-cost:   14
c ---[ 144]---> BDD-cost:   14
c ---[ 143]---> BDD-cost:   14
c ---[ 142]---> BDD-cost:   14
c ---[ 141]---> BDD-cost:   14
c ---[ 140]---> BDD-cost:   41
c ---[ 139]---> BDD-cost:   14
c ---[ 138]---> BDD-cost:   14
c ---[ 137]---> BDD-cost:   14
c ---[ 136]---> BDD-cost:   14
c ---[ 135]---> BDD-cost:   14
c ---[ 134]---> BDD-cost:   14
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:   14
c ---[ 131]---> BDD-cost:   14
c ---[ 130]---> BDD-cost:   14
c ---[ 129]---> BDD-cost:   41
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:   14
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   41
c ---[ 124]---> BDD-cost:   41
c ---[ 123]---> BDD-cost:   41
c ---[ 113]---> BDD-cost:   41
c ---[ 102]---> BDD-cost:    4
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    3
c ---[  98]---> BDD-cost:    4
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   12
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    4
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:    6
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:    7
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:    4
c ---[  83]---> BDD-cost:    5
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:    8
c ---[  80]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    2
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:   14
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:   13
c ---[  74]---> BDD-cost:    7
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:   12
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   13
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    6
c ---[  65]---> BDD-cost:   16
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:    2
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:    6
c ---[  60]---> BDD-cost:    6
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:    6
c ---[  53]---> BDD-cost:    6
c ---[  52]---> BDD-cost:    6
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:    6
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:    7
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    5
c ---[  41]---> BDD-cost:    2
c ---[  40]---> BDD-cost:   20
c ---[  39]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   19
c ---[  37]---> BDD-cost:    5
c ---[  36]---> BDD-cost:   12
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   20
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:    6
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    4
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:    3
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:    4
c ---[  21]---> BDD-cost:    2
c ---[  20]---> BDD-cost:   12
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    2
c ---[  17]---> BDD-cost:    8
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    4
c ---[  14]---> BDD-cost:    8
c ---[  13]---> BDD-cost:    2
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:    7
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1028559  3258490 |  342853       0        0     nan |  0.000 % |
c |       100 | 1027607  3255279 |  377138      65      238     3.7 |  1.166 % |
c |       250 | 1026498  3251569 |  414852     179     3741    20.9 |  1.220 % |
c |       476 | 1026498  3251569 |  456337     405     6844    16.9 |  1.220 % |
c |       814 | 1025381  3248136 |  501971     698    13011    18.6 |  1.291 % |
c |      1323 | 1025355  3248043 |  552168    1131    26979    23.9 |  1.292 % |
c |      2083 | 1023324  3241696 |  607385    1830    43302    23.7 |  1.439 % |
c |      3222 | 1018762  3228409 |  668123    2606    69271    26.6 |  1.851 % |
c |      4930 | 1011772  3209760 |  734935    3789   107989    28.5 |  2.536 % |
c |      7495 | 1003639  3187602 |  808429    5889   177365    30.1 |  3.282 % |
c |     11339 |  997079  3171495 |  889272    9315   279366    30.0 |  4.037 % |
c |     17105 |  989617  3152786 |  978199   14275   431609    30.2 |  4.897 % |
c |     25755 |  982598  3135762 | 1076019   22358   677020    30.3 |  5.751 % |
c |     38731 |  976522  3120034 | 1183621   34357  1088620    31.7 |  6.392 % |
c |     58198 |  937834  3026045 | 1301983   50279  1574050    31.3 | 11.099 % |
c |     87390 |  880430  2884096 | 1432182   72444  2192297    30.3 | 18.201 % |
c |    131179 |  848466  2797324 | 1575400  107050  3134553    29.3 | 21.527 % |
c |    196863 |  796757  2641676 | 1732940  152053  4292100    28.2 | 26.061 % |

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/791/stat): 791 (minisat+_script) R 790 791 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855650986 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/791/statm): 174 3 169 147 0 27 0
[pid=791] 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=792
New process pid=793
New process pid=794
execve syscall for /bin/sed executable
One traced child (pid=793) 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=794) exited with status: 0
One traced child (pid=792) exited with status: 0
New process pid=795
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-mitre.opb

[startup+10.0043 s]
Raw data (loadavg): 0.91 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 3076 0 0 0 971 13 0 0 25 0 1 0 1855650991 12926976 2671 4294967295 134512640 135094434 3221224432 3221222304 134677147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 3156 2671 145 145 0 3011 0
[pid=795] vsize: 12624
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 14748

[startup+20.0051 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 18966 0 0 0 1838 79 0 0 21 0 1 0 1855650991 84090880 18224 4294967295 134512640 135094434 3221224432 3221219808 134525177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 20530 18224 145 145 0 20385 0
[pid=795] vsize: 82120
Current children cumulated CPU time (s) 19.17
Current children cumulated vsize (Kb) 84244

[startup+30.0069 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23194 0 0 0 2802 95 0 0 25 0 1 0 1855650991 99258368 22452 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 24233 22452 145 145 0 24088 0
[pid=795] vsize: 96932
Current children cumulated CPU time (s) 28.97
Current children cumulated vsize (Kb) 99056

[startup+40.0077 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23262 0 0 0 3800 96 0 0 25 0 1 0 1855650991 99536896 22520 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 24301 22520 145 145 0 24156 0
[pid=795] vsize: 97204
Current children cumulated CPU time (s) 38.96
Current children cumulated vsize (Kb) 99328

[startup+50.0085 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23274 0 0 0 4799 97 0 0 25 0 1 0 1855650991 99586048 22532 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 24313 22532 145 145 0 24168 0
[pid=795] vsize: 97252
Current children cumulated CPU time (s) 48.96
Current children cumulated vsize (Kb) 99376

[startup+60.0093 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23309 0 0 0 5799 97 0 0 25 0 1 0 1855650991 99733504 22567 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24349 22567 145 145 0 24204 0
[pid=795] vsize: 97396
Current children cumulated CPU time (s) 58.96
Current children cumulated vsize (Kb) 99520

[startup+70.0101 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23356 0 0 0 6798 98 0 0 25 0 1 0 1855650991 99905536 22614 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24391 22614 145 145 0 24246 0
[pid=795] vsize: 97564
Current children cumulated CPU time (s) 68.96
Current children cumulated vsize (Kb) 99688

[startup+80.0119 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23436 0 0 0 7797 98 0 0 25 0 1 0 1855650991 100167680 22694 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24455 22694 145 145 0 24310 0
[pid=795] vsize: 97820
Current children cumulated CPU time (s) 78.95
Current children cumulated vsize (Kb) 99944

[startup+90.0127 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23510 0 0 0 8796 99 0 0 25 0 1 0 1855650991 100487168 22768 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24533 22768 145 145 0 24388 0
[pid=795] vsize: 98132
Current children cumulated CPU time (s) 88.95
Current children cumulated vsize (Kb) 100256

[startup+100.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23545 0 0 0 9796 99 0 0 25 0 1 0 1855650991 100618240 22803 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24565 22803 145 145 0 24420 0
[pid=795] vsize: 98260
Current children cumulated CPU time (s) 98.95
Current children cumulated vsize (Kb) 100384

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23595 0 0 0 10795 99 0 0 25 0 1 0 1855650991 100798464 22853 4294967295 134512640 135094434 3221224432 3221223056 134562122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24609 22853 145 145 0 24464 0
[pid=795] vsize: 98436
Current children cumulated CPU time (s) 108.94
Current children cumulated vsize (Kb) 100560

[startup+120.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23678 0 0 0 11794 100 0 0 25 0 1 0 1855650991 101097472 22936 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24682 22936 145 145 0 24537 0
[pid=795] vsize: 98728
Current children cumulated CPU time (s) 118.94
Current children cumulated vsize (Kb) 100852

[startup+130.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23818 0 0 0 12792 101 0 0 25 0 1 0 1855650991 101642240 23076 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24815 23076 145 145 0 24670 0
[pid=795] vsize: 99260
Current children cumulated CPU time (s) 128.93
Current children cumulated vsize (Kb) 101384

[startup+140.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23866 0 0 0 13790 102 0 0 25 0 1 0 1855650991 101830656 23124 4294967295 134512640 135094434 3221224432 3221223024 134556918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24861 23124 145 145 0 24716 0
[pid=795] vsize: 99444
Current children cumulated CPU time (s) 138.92
Current children cumulated vsize (Kb) 101568

[startup+150.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 23905 0 0 0 14789 103 0 0 25 0 1 0 1855650991 101986304 23163 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 24899 23163 145 145 0 24754 0
[pid=795] vsize: 99596
Current children cumulated CPU time (s) 148.92
Current children cumulated vsize (Kb) 101720

[startup+160.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24019 0 0 0 15788 104 0 0 25 0 1 0 1855650991 102445056 23277 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25011 23277 145 145 0 24866 0
[pid=795] vsize: 100044
Current children cumulated CPU time (s) 158.92
Current children cumulated vsize (Kb) 102168

[startup+170.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24099 0 0 0 16787 104 0 0 25 0 1 0 1855650991 102830080 23357 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25105 23357 145 145 0 24960 0
[pid=795] vsize: 100420
Current children cumulated CPU time (s) 168.91
Current children cumulated vsize (Kb) 102544

[startup+180.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24295 0 0 0 17782 108 0 0 25 0 1 0 1855650991 103575552 23553 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25287 23553 145 145 0 25142 0
[pid=795] vsize: 101148
Current children cumulated CPU time (s) 178.9
Current children cumulated vsize (Kb) 103272

[startup+190.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24300 0 0 0 18782 108 0 0 25 0 1 0 1855650991 103591936 23558 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25291 23558 145 145 0 25146 0
[pid=795] vsize: 101164
Current children cumulated CPU time (s) 188.9
Current children cumulated vsize (Kb) 103288

[startup+200.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24479 0 0 0 19779 110 0 0 25 0 1 0 1855650991 104284160 23737 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25460 23737 145 145 0 25315 0
[pid=795] vsize: 101840
Current children cumulated CPU time (s) 198.89
Current children cumulated vsize (Kb) 103964

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24772 0 0 0 20775 113 0 0 25 0 1 0 1855650991 105459712 24030 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25747 24030 145 145 0 25602 0
[pid=795] vsize: 102988
Current children cumulated CPU time (s) 208.88
Current children cumulated vsize (Kb) 105112

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24887 0 0 0 21773 114 0 0 25 0 1 0 1855650991 106053632 24145 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25892 24145 145 145 0 25747 0
[pid=795] vsize: 103568
Current children cumulated CPU time (s) 218.87
Current children cumulated vsize (Kb) 105692

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24918 0 0 0 22773 114 0 0 25 0 1 0 1855650991 106176512 24176 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 25922 24176 145 145 0 25777 0
[pid=795] vsize: 103688
Current children cumulated CPU time (s) 228.87
Current children cumulated vsize (Kb) 105812

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 24982 0 0 0 23771 114 0 0 25 0 1 0 1855650991 106434560 24240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 25985 24240 145 145 0 25840 0
[pid=795] vsize: 103940
Current children cumulated CPU time (s) 238.85
Current children cumulated vsize (Kb) 106064

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25043 0 0 0 24770 115 0 0 25 0 1 0 1855650991 106676224 24301 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 26044 24301 145 145 0 25899 0
[pid=795] vsize: 104176
Current children cumulated CPU time (s) 248.85
Current children cumulated vsize (Kb) 106300

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25062 0 0 0 25769 115 0 0 25 0 1 0 1855650991 106754048 24320 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26063 24320 145 145 0 25918 0
[pid=795] vsize: 104252
Current children cumulated CPU time (s) 258.84
Current children cumulated vsize (Kb) 106376

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25076 0 0 0 26769 115 0 0 25 0 1 0 1855650991 106811392 24334 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26077 24334 145 145 0 25932 0
[pid=795] vsize: 104308
Current children cumulated CPU time (s) 268.84
Current children cumulated vsize (Kb) 106432

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25097 0 0 0 27769 116 0 0 25 0 1 0 1855650991 106889216 24355 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26096 24355 145 145 0 25951 0
[pid=795] vsize: 104384
Current children cumulated CPU time (s) 278.85
Current children cumulated vsize (Kb) 106508

[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25155 0 0 0 28768 116 0 0 25 0 1 0 1855650991 107118592 24413 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26152 24413 145 145 0 26007 0
[pid=795] vsize: 104608
Current children cumulated CPU time (s) 288.84
Current children cumulated vsize (Kb) 106732

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25193 0 0 0 29768 116 0 0 25 0 1 0 1855650991 107249664 24451 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26184 24451 145 145 0 26039 0
[pid=795] vsize: 104736
Current children cumulated CPU time (s) 298.84
Current children cumulated vsize (Kb) 106860

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25252 0 0 0 30767 117 0 0 25 0 1 0 1855650991 107446272 24510 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26232 24510 145 145 0 26087 0
[pid=795] vsize: 104928
Current children cumulated CPU time (s) 308.84
Current children cumulated vsize (Kb) 107052

[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25287 0 0 0 31766 118 0 0 25 0 1 0 1855650991 107585536 24545 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26266 24545 145 145 0 26121 0
[pid=795] vsize: 105064
Current children cumulated CPU time (s) 318.84
Current children cumulated vsize (Kb) 107188

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25315 0 0 0 32766 118 0 0 25 0 1 0 1855650991 107700224 24573 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26294 24573 145 145 0 26149 0
[pid=795] vsize: 105176
Current children cumulated CPU time (s) 328.84
Current children cumulated vsize (Kb) 107300

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25361 0 0 0 33765 119 0 0 25 0 1 0 1855650991 107884544 24619 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26339 24619 145 145 0 26194 0
[pid=795] vsize: 105356
Current children cumulated CPU time (s) 338.84
Current children cumulated vsize (Kb) 107480

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25366 0 0 0 34765 119 0 0 25 0 1 0 1855650991 107905024 24624 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26344 24624 145 145 0 26199 0
[pid=795] vsize: 105376
Current children cumulated CPU time (s) 348.84
Current children cumulated vsize (Kb) 107500

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25383 0 0 0 35765 119 0 0 25 0 1 0 1855650991 107941888 24641 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26353 24641 145 145 0 26208 0
[pid=795] vsize: 105412
Current children cumulated CPU time (s) 358.84
Current children cumulated vsize (Kb) 107536

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25422 0 0 0 36764 120 0 0 25 0 1 0 1855650991 108097536 24680 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26391 24680 145 145 0 26246 0
[pid=795] vsize: 105564
Current children cumulated CPU time (s) 368.84
Current children cumulated vsize (Kb) 107688

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25433 0 0 0 37765 120 0 0 25 0 1 0 1855650991 108142592 24691 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26402 24691 145 145 0 26257 0
[pid=795] vsize: 105608
Current children cumulated CPU time (s) 378.85
Current children cumulated vsize (Kb) 107732

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25453 0 0 0 38764 120 0 0 25 0 1 0 1855650991 108224512 24711 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26422 24711 145 145 0 26277 0
[pid=795] vsize: 105688
Current children cumulated CPU time (s) 388.84
Current children cumulated vsize (Kb) 107812

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25473 0 0 0 39764 120 0 0 25 0 1 0 1855650991 108302336 24731 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26441 24731 145 145 0 26296 0
[pid=795] vsize: 105764
Current children cumulated CPU time (s) 398.84
Current children cumulated vsize (Kb) 107888

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25545 0 0 0 40763 121 0 0 25 0 1 0 1855650991 108589056 24803 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26511 24803 145 145 0 26366 0
[pid=795] vsize: 106044
Current children cumulated CPU time (s) 408.84
Current children cumulated vsize (Kb) 108168

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25563 0 0 0 41763 121 0 0 25 0 1 0 1855650991 108662784 24821 4294967295 134512640 135094434 3221224432 3221223044 134563124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26529 24821 145 145 0 26384 0
[pid=795] vsize: 106116
Current children cumulated CPU time (s) 418.84
Current children cumulated vsize (Kb) 108240

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25600 0 0 0 42762 122 0 0 25 0 1 0 1855650991 108810240 24858 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26565 24858 145 145 0 26420 0
[pid=795] vsize: 106260
Current children cumulated CPU time (s) 428.84
Current children cumulated vsize (Kb) 108384

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25644 0 0 0 43762 122 0 0 25 0 1 0 1855650991 108978176 24902 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26606 24902 145 145 0 26461 0
[pid=795] vsize: 106424
Current children cumulated CPU time (s) 438.84
Current children cumulated vsize (Kb) 108548

[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25673 0 0 0 44761 122 0 0 25 0 1 0 1855650991 109092864 24931 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26634 24931 145 145 0 26489 0
[pid=795] vsize: 106536
Current children cumulated CPU time (s) 448.83
Current children cumulated vsize (Kb) 108660

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25674 0 0 0 45761 123 0 0 25 0 1 0 1855650991 109096960 24932 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26635 24932 145 145 0 26490 0
[pid=795] vsize: 106540
Current children cumulated CPU time (s) 458.84
Current children cumulated vsize (Kb) 108664

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25788 0 0 0 46759 124 0 0 25 0 1 0 1855650991 109531136 25046 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26741 25046 145 145 0 26596 0
[pid=795] vsize: 106964
Current children cumulated CPU time (s) 468.83
Current children cumulated vsize (Kb) 109088

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25801 0 0 0 47759 124 0 0 25 0 1 0 1855650991 109584384 25059 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26754 25059 145 145 0 26609 0
[pid=795] vsize: 107016
Current children cumulated CPU time (s) 478.83
Current children cumulated vsize (Kb) 109140

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25917 0 0 0 48757 125 0 0 25 0 1 0 1855650991 110039040 25175 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26865 25175 145 145 0 26720 0
[pid=795] vsize: 107460
Current children cumulated CPU time (s) 488.82
Current children cumulated vsize (Kb) 109584

[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25917 0 0 0 49758 125 0 0 25 0 1 0 1855650991 110039040 25175 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26865 25175 145 145 0 26720 0
[pid=795] vsize: 107460
Current children cumulated CPU time (s) 498.83
Current children cumulated vsize (Kb) 109584

[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25923 0 0 0 50758 125 0 0 25 0 1 0 1855650991 110063616 25181 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26871 25181 145 145 0 26726 0
[pid=795] vsize: 107484
Current children cumulated CPU time (s) 508.83
Current children cumulated vsize (Kb) 109608

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 25947 0 0 0 51757 125 0 0 25 0 1 0 1855650991 110157824 25205 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26894 25205 145 145 0 26749 0
[pid=795] vsize: 107576
Current children cumulated CPU time (s) 518.82
Current children cumulated vsize (Kb) 109700

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26021 0 0 0 52757 125 0 0 25 0 1 0 1855650991 110452736 25279 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 26966 25279 145 145 0 26821 0
[pid=795] vsize: 107864
Current children cumulated CPU time (s) 528.82
Current children cumulated vsize (Kb) 109988

[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26060 0 0 0 53756 126 0 0 25 0 1 0 1855650991 110608384 25318 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27004 25318 145 145 0 26859 0
[pid=795] vsize: 108016
Current children cumulated CPU time (s) 538.82
Current children cumulated vsize (Kb) 110140

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26089 0 0 0 54756 126 0 0 25 0 1 0 1855650991 110723072 25347 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27032 25347 145 145 0 26887 0
[pid=795] vsize: 108128
Current children cumulated CPU time (s) 548.82
Current children cumulated vsize (Kb) 110252

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26140 0 0 0 55756 126 0 0 25 0 1 0 1855650991 111185920 25398 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27145 25398 145 145 0 27000 0
[pid=795] vsize: 108580
Current children cumulated CPU time (s) 558.82
Current children cumulated vsize (Kb) 110704

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26174 0 0 0 56755 126 0 0 25 0 1 0 1855650991 111321088 25432 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27178 25432 145 145 0 27033 0
[pid=795] vsize: 108712
Current children cumulated CPU time (s) 568.81
Current children cumulated vsize (Kb) 110836

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26197 0 0 0 57756 126 0 0 25 0 1 0 1855650991 111403008 25455 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27198 25455 145 145 0 27053 0
[pid=795] vsize: 108792
Current children cumulated CPU time (s) 578.82
Current children cumulated vsize (Kb) 110916

[startup+590.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26207 0 0 0 58755 127 0 0 25 0 1 0 1855650991 111439872 25465 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27207 25465 145 145 0 27062 0
[pid=795] vsize: 108828
Current children cumulated CPU time (s) 588.82
Current children cumulated vsize (Kb) 110952

[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26315 0 0 0 59754 127 0 0 25 0 1 0 1855650991 111853568 25573 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27308 25573 145 145 0 27163 0
[pid=795] vsize: 109232
Current children cumulated CPU time (s) 598.81
Current children cumulated vsize (Kb) 111356

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26398 0 0 0 60753 128 0 0 25 0 1 0 1855650991 112185344 25656 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27389 25656 145 145 0 27244 0
[pid=795] vsize: 109556
Current children cumulated CPU time (s) 608.81
Current children cumulated vsize (Kb) 111680

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26424 0 0 0 61752 128 0 0 25 0 1 0 1855650991 112287744 25682 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27414 25682 145 145 0 27269 0
[pid=795] vsize: 109656
Current children cumulated CPU time (s) 618.8
Current children cumulated vsize (Kb) 111780

[startup+630.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26496 0 0 0 62752 128 0 0 25 0 1 0 1855650991 112578560 25754 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27485 25754 145 145 0 27340 0
[pid=795] vsize: 109940
Current children cumulated CPU time (s) 628.8
Current children cumulated vsize (Kb) 112064

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26526 0 0 0 63752 128 0 0 25 0 1 0 1855650991 112697344 25784 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27514 25784 145 145 0 27369 0
[pid=795] vsize: 110056
Current children cumulated CPU time (s) 638.8
Current children cumulated vsize (Kb) 112180

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26555 0 0 0 64751 128 0 0 25 0 1 0 1855650991 112812032 25813 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27542 25813 145 145 0 27397 0
[pid=795] vsize: 110168
Current children cumulated CPU time (s) 648.79
Current children cumulated vsize (Kb) 112292

[startup+660.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26625 0 0 0 65750 129 0 0 25 0 1 0 1855650991 113090560 25883 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27610 25883 145 145 0 27465 0
[pid=795] vsize: 110440
Current children cumulated CPU time (s) 658.79
Current children cumulated vsize (Kb) 112564

[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26729 0 0 0 66748 130 0 0 25 0 1 0 1855650991 113504256 25987 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27711 25987 145 145 0 27566 0
[pid=795] vsize: 110844
Current children cumulated CPU time (s) 668.78
Current children cumulated vsize (Kb) 112968

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26737 0 0 0 67749 130 0 0 25 0 1 0 1855650991 113537024 25995 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27719 25995 145 145 0 27574 0
[pid=795] vsize: 110876
Current children cumulated CPU time (s) 678.79
Current children cumulated vsize (Kb) 113000

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26793 0 0 0 68748 131 0 0 25 0 1 0 1855650991 113762304 26051 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27774 26051 145 145 0 27629 0
[pid=795] vsize: 111096
Current children cumulated CPU time (s) 688.79
Current children cumulated vsize (Kb) 113220

[startup+700.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26834 0 0 0 69747 131 0 0 25 0 1 0 1855650991 113922048 26092 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27813 26092 145 145 0 27668 0
[pid=795] vsize: 111252
Current children cumulated CPU time (s) 698.78
Current children cumulated vsize (Kb) 113376

[startup+710.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26920 0 0 0 70746 132 0 0 25 0 1 0 1855650991 114262016 26178 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27896 26178 145 145 0 27751 0
[pid=795] vsize: 111584
Current children cumulated CPU time (s) 708.78
Current children cumulated vsize (Kb) 113708

[startup+720.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 26936 0 0 0 71746 132 0 0 25 0 1 0 1855650991 114327552 26194 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27912 26194 145 145 0 27767 0
[pid=795] vsize: 111648
Current children cumulated CPU time (s) 718.78
Current children cumulated vsize (Kb) 113772

[startup+730.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27009 0 0 0 72745 132 0 0 25 0 1 0 1855650991 114597888 26267 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27978 26267 145 145 0 27833 0
[pid=795] vsize: 111912
Current children cumulated CPU time (s) 728.77
Current children cumulated vsize (Kb) 114036

[startup+740.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27014 0 0 0 73745 132 0 0 25 0 1 0 1855650991 114618368 26272 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 27983 26272 145 145 0 27838 0
[pid=795] vsize: 111932
Current children cumulated CPU time (s) 738.77
Current children cumulated vsize (Kb) 114056

[startup+750.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27269 0 0 0 74741 134 0 0 25 0 1 0 1855650991 115609600 26527 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 28225 26527 145 145 0 28080 0
[pid=795] vsize: 112900
Current children cumulated CPU time (s) 748.75
Current children cumulated vsize (Kb) 115024

[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27365 0 0 0 75740 135 0 0 25 0 1 0 1855650991 115990528 26623 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 28318 26623 145 145 0 28173 0
[pid=795] vsize: 113272
Current children cumulated CPU time (s) 758.75
Current children cumulated vsize (Kb) 115396

[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27420 0 0 0 76739 135 0 0 25 0 1 0 1855650991 116211712 26678 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 28372 26678 145 145 0 28227 0
[pid=795] vsize: 113488
Current children cumulated CPU time (s) 768.74
Current children cumulated vsize (Kb) 115612

[startup+780.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27465 0 0 0 77736 137 0 0 25 0 1 0 1855650991 116387840 26723 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 28415 26723 145 145 0 28270 0
[pid=795] vsize: 113660
Current children cumulated CPU time (s) 778.73
Current children cumulated vsize (Kb) 115784

[startup+790.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27518 0 0 0 78736 138 0 0 25 0 1 0 1855650991 116600832 26776 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 28467 26776 145 145 0 28322 0
[pid=795] vsize: 113868
Current children cumulated CPU time (s) 788.74
Current children cumulated vsize (Kb) 115992

[startup+800.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27586 0 0 0 79735 139 0 0 25 0 1 0 1855650991 116871168 26844 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 28533 26844 145 145 0 28388 0
[pid=795] vsize: 114132
Current children cumulated CPU time (s) 798.74
Current children cumulated vsize (Kb) 116256

[startup+810.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27594 0 0 0 80735 139 0 0 25 0 1 0 1855650991 116903936 26852 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 28541 26852 145 145 0 28396 0
[pid=795] vsize: 114164
Current children cumulated CPU time (s) 808.74
Current children cumulated vsize (Kb) 116288

[startup+820.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27662 0 0 0 81733 140 0 0 25 0 1 0 1855650991 117174272 26920 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28607 26920 145 145 0 28462 0
[pid=795] vsize: 114428
Current children cumulated CPU time (s) 818.73
Current children cumulated vsize (Kb) 116552

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27797 0 0 0 82731 141 0 0 23 0 1 0 1855650991 117706752 27055 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28737 27055 145 145 0 28592 0
[pid=795] vsize: 114948
Current children cumulated CPU time (s) 828.72
Current children cumulated vsize (Kb) 117072

[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27836 0 0 0 83730 141 0 0 25 0 1 0 1855650991 117862400 27094 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28775 27094 145 145 0 28630 0
[pid=795] vsize: 115100
Current children cumulated CPU time (s) 838.71
Current children cumulated vsize (Kb) 117224

[startup+850.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27858 0 0 0 84730 142 0 0 25 0 1 0 1855650991 117952512 27116 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28797 27116 145 145 0 28652 0
[pid=795] vsize: 115188
Current children cumulated CPU time (s) 848.72
Current children cumulated vsize (Kb) 117312

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27942 0 0 0 85729 142 0 0 25 0 1 0 1855650991 118288384 27200 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28879 27200 145 145 0 28734 0
[pid=795] vsize: 115516
Current children cumulated CPU time (s) 858.71
Current children cumulated vsize (Kb) 117640

[startup+870.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27968 0 0 0 86728 143 0 0 25 0 1 0 1855650991 118386688 27226 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28903 27226 145 145 0 28758 0
[pid=795] vsize: 115612
Current children cumulated CPU time (s) 868.71
Current children cumulated vsize (Kb) 117736

[startup+880.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27978 0 0 0 87728 143 0 0 25 0 1 0 1855650991 118427648 27236 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28913 27236 145 145 0 28768 0
[pid=795] vsize: 115652
Current children cumulated CPU time (s) 878.71
Current children cumulated vsize (Kb) 117776

[startup+890.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27991 0 0 0 88728 144 0 0 25 0 1 0 1855650991 118476800 27249 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28925 27249 145 145 0 28780 0
[pid=795] vsize: 115700
Current children cumulated CPU time (s) 888.72
Current children cumulated vsize (Kb) 117824

[startup+900.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 27991 0 0 0 89728 144 0 0 25 0 1 0 1855650991 118476800 27249 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28925 27249 145 145 0 28780 0
[pid=795] vsize: 115700
Current children cumulated CPU time (s) 898.72
Current children cumulated vsize (Kb) 117824

[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28041 0 0 0 90727 144 0 0 25 0 1 0 1855650991 118673408 27299 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 28973 27299 145 145 0 28828 0
[pid=795] vsize: 115892
Current children cumulated CPU time (s) 908.71
Current children cumulated vsize (Kb) 118016

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28072 0 0 0 91726 145 0 0 25 0 1 0 1855650991 118796288 27330 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 29003 27330 145 145 0 28858 0
[pid=795] vsize: 116012
Current children cumulated CPU time (s) 918.71
Current children cumulated vsize (Kb) 118136

[startup+930.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28103 0 0 0 92726 145 0 0 25 0 1 0 1855650991 118915072 27361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 29032 27361 145 145 0 28887 0
[pid=795] vsize: 116128
Current children cumulated CPU time (s) 928.71
Current children cumulated vsize (Kb) 118252

[startup+940.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28103 0 0 0 93725 145 0 0 25 0 1 0 1855650991 118915072 27361 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 29032 27361 145 145 0 28887 0
[pid=795] vsize: 116128
Current children cumulated CPU time (s) 938.7
Current children cumulated vsize (Kb) 118252

[startup+950.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28132 0 0 0 94724 146 0 0 25 0 1 0 1855650991 119025664 27390 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 29059 27390 145 145 0 28914 0
[pid=795] vsize: 116236
Current children cumulated CPU time (s) 948.7
Current children cumulated vsize (Kb) 118360

[startup+960.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28197 0 0 0 95723 147 0 0 25 0 1 0 1855650991 119267328 27455 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/795/statm): 29118 27455 145 145 0 28973 0
[pid=795] vsize: 116472
Current children cumulated CPU time (s) 958.7
Current children cumulated vsize (Kb) 118596

[startup+970.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28205 0 0 0 96723 147 0 0 25 0 1 0 1855650991 119300096 27463 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29126 27463 145 145 0 28981 0
[pid=795] vsize: 116504
Current children cumulated CPU time (s) 968.7
Current children cumulated vsize (Kb) 118628

[startup+980.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28291 0 0 0 97722 148 0 0 25 0 1 0 1855650991 119635968 27549 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29208 27549 145 145 0 29063 0
[pid=795] vsize: 116832
Current children cumulated CPU time (s) 978.7
Current children cumulated vsize (Kb) 118956

[startup+990.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28389 0 0 0 98720 149 0 0 25 0 1 0 1855650991 120029184 27647 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29304 27647 145 145 0 29159 0
[pid=795] vsize: 117216
Current children cumulated CPU time (s) 988.69
Current children cumulated vsize (Kb) 119340

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28437 0 0 0 99719 149 0 0 25 0 1 0 1855650991 120217600 27695 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29350 27695 145 145 0 29205 0
[pid=795] vsize: 117400
Current children cumulated CPU time (s) 998.68
Current children cumulated vsize (Kb) 119524

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28487 0 0 0 100718 150 0 0 25 0 1 0 1855650991 120942592 27745 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29527 27745 145 145 0 29382 0
[pid=795] vsize: 118108
Current children cumulated CPU time (s) 1008.68
Current children cumulated vsize (Kb) 120232

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28498 0 0 0 101719 150 0 0 25 0 1 0 1855650991 120983552 27756 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29537 27756 145 145 0 29392 0
[pid=795] vsize: 118148
Current children cumulated CPU time (s) 1018.69
Current children cumulated vsize (Kb) 120272

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28546 0 0 0 102719 150 0 0 25 0 1 0 1855650991 121176064 27804 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29584 27804 145 145 0 29439 0
[pid=795] vsize: 118336
Current children cumulated CPU time (s) 1028.69
Current children cumulated vsize (Kb) 120460

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28599 0 0 0 103718 150 0 0 25 0 1 0 1855650991 121384960 27857 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29635 27857 145 145 0 29490 0
[pid=795] vsize: 118540
Current children cumulated CPU time (s) 1038.68
Current children cumulated vsize (Kb) 120664

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28608 0 0 0 104718 150 0 0 25 0 1 0 1855650991 121417728 27866 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29643 27866 145 145 0 29498 0
[pid=795] vsize: 118572
Current children cumulated CPU time (s) 1048.68
Current children cumulated vsize (Kb) 120696

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28663 0 0 0 105718 151 0 0 25 0 1 0 1855650991 121634816 27921 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29696 27921 145 145 0 29551 0
[pid=795] vsize: 118784
Current children cumulated CPU time (s) 1058.69
Current children cumulated vsize (Kb) 120908

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28683 0 0 0 106717 151 0 0 25 0 1 0 1855650991 121716736 27941 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29716 27941 145 145 0 29571 0
[pid=795] vsize: 118864
Current children cumulated CPU time (s) 1068.68
Current children cumulated vsize (Kb) 120988

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28683 0 0 0 107718 151 0 0 25 0 1 0 1855650991 121716736 27941 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29716 27941 145 145 0 29571 0
[pid=795] vsize: 118864
Current children cumulated CPU time (s) 1078.69
Current children cumulated vsize (Kb) 120988

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28714 0 0 0 108718 151 0 0 25 0 1 0 1855650991 121839616 27972 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29746 27972 145 145 0 29601 0
[pid=795] vsize: 118984
Current children cumulated CPU time (s) 1088.69
Current children cumulated vsize (Kb) 121108

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28780 0 0 0 109717 152 0 0 25 0 1 0 1855650991 122101760 28038 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29810 28038 145 145 0 29665 0
[pid=795] vsize: 119240
Current children cumulated CPU time (s) 1098.69
Current children cumulated vsize (Kb) 121364

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28794 0 0 0 110717 152 0 0 25 0 1 0 1855650991 122159104 28052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29824 28052 145 145 0 29679 0
[pid=795] vsize: 119296
Current children cumulated CPU time (s) 1108.69
Current children cumulated vsize (Kb) 121420

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28814 0 0 0 111716 153 0 0 25 0 1 0 1855650991 122236928 28072 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29843 28072 145 145 0 29698 0
[pid=795] vsize: 119372
Current children cumulated CPU time (s) 1118.69
Current children cumulated vsize (Kb) 121496

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28855 0 0 0 112716 153 0 0 25 0 1 0 1855650991 122400768 28113 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29883 28113 145 145 0 29738 0
[pid=795] vsize: 119532
Current children cumulated CPU time (s) 1128.69
Current children cumulated vsize (Kb) 121656

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28883 0 0 0 113715 153 0 0 25 0 1 0 1855650991 122511360 28141 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29910 28141 145 145 0 29765 0
[pid=795] vsize: 119640
Current children cumulated CPU time (s) 1138.68
Current children cumulated vsize (Kb) 121764

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28933 0 0 0 114715 153 0 0 25 0 1 0 1855650991 122699776 28191 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 29956 28191 145 145 0 29811 0
[pid=795] vsize: 119824
Current children cumulated CPU time (s) 1148.68
Current children cumulated vsize (Kb) 121948

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 28998 0 0 0 115714 154 0 0 25 0 1 0 1855650991 122933248 28256 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 30013 28256 145 145 0 29868 0
[pid=795] vsize: 120052
Current children cumulated CPU time (s) 1158.68
Current children cumulated vsize (Kb) 122176

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 29067 0 0 0 116713 155 0 0 25 0 1 0 1855650991 123207680 28325 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 30080 28325 145 145 0 29935 0
[pid=795] vsize: 120320
Current children cumulated CPU time (s) 1168.68
Current children cumulated vsize (Kb) 122444

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 29071 0 0 0 117714 155 0 0 25 0 1 0 1855650991 123224064 28329 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 30084 28329 145 145 0 29939 0
[pid=795] vsize: 120336
Current children cumulated CPU time (s) 1178.69
Current children cumulated vsize (Kb) 122460

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 29210 0 0 0 118710 157 0 0 25 0 1 0 1855650991 123764736 28468 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 30216 28468 145 145 0 30071 0
[pid=795] vsize: 120864
Current children cumulated CPU time (s) 1188.67
Current children cumulated vsize (Kb) 122988

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 29212 0 0 0 119710 157 0 0 25 0 1 0 1855650991 123772928 28470 4294967295 134512640 135094434 3221224432 3221223056 134562082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 30218 28470 145 145 0 30073 0
[pid=795] vsize: 120872
Current children cumulated CPU time (s) 1198.67
Current children cumulated vsize (Kb) 122996

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 29212 0 0 0 120711 157 0 0 25 0 1 0 1855650991 123772928 28470 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 30218 28470 145 145 0 30073 0
[pid=795] vsize: 120872
Current children cumulated CPU time (s) 1208.68
Current children cumulated vsize (Kb) 122996



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 795
Raw data (/proc/791/stat): 791 (minisat+_script) S 790 791 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855650986 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/791/statm): 531 226 485 147 0 384 0
[pid=791] vsize: 2124
Raw data (/proc/795/stat): 795 (minisat+_64-bit) R 791 791 5929 0 -1 0 29212 0 0 0 120711 157 0 0 25 0 1 0 1855650991 123772928 28470 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/795/statm): 30218 28470 145 145 0 30073 0
[pid=795] vsize: 120872
Current children cumulated CPU time (s) 1208.68
Current children cumulated vsize (Kb) 122996

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1208.74
CPU user time (s): 1207.11
CPU system time (s): 1.62575
CPU usage (%): 99.8814
Max. virtual memory (cumulated for all children) (Kb): 122996

Verifier Data

ERROR: no interpretation found !