PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/manquinho/ttp/normalized-data6_3.opb
MD5SUM	3ce91e964f348d481da3f7741c5768eb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	25102
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	1380
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	116904
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	1380
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	116904
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	540
Total number of constraints	4476
Number of constraints which are clauses	2532
Number of constraints which are cardinality constraints (but not clauses)	264
Number of constraints which are nor clauses,nor cardinality constraints	1680
Minimum length of a constraint	2
Maximum length of a constraint	20
Trace number 5974

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 02:34:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4398 boxname=wulflinc24 idbench=262 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3ce91e964f348d481da3f7741c5768eb  /oldhome/oroussel/tmp/wulflinc24/normalized-data6_3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-data6_3.opb /oldhome/oroussel/tmp/wulflinc24/normalized-data6_3.opb
IDLAUNCH: 4398
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        833128 kB
Buffers:         35172 kB
Cached:         123792 kB
SwapCached:       3828 kB
Active:          52476 kB
Inactive:       113220 kB
HighTotal:      131008 kB
HighFree:         4872 kB
LowTotal:       903652 kB
LowFree:        828256 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30276 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:54:10 (client local time) WITH STATUS 10 IN 1200.31 SECONDS
stats: 4398 7 1200.31 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4626 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[4624]---> BDD-cost:   17
c ---[4622]---> BDD-cost:   17
c ---[4620]---> BDD-cost:   17
c ---[4618]---> BDD-cost:   17
c ---[4616]---> BDD-cost:   17
c ---[4614]---> BDD-cost:   17
c ---[4612]---> BDD-cost:   17
c ---[4610]---> BDD-cost:   17
c ---[4608]---> BDD-cost:   17
c ---[4606]---> BDD-cost:   17
c ---[4604]---> BDD-cost:   17
c ---[4602]---> BDD-cost:   17
c ---[4600]---> BDD-cost:   17
c ---[4598]---> BDD-cost:   17
c ---[4596]---> BDD-cost:   17
c ---[4594]---> BDD-cost:   17
c ---[4592]---> BDD-cost:   17
c ---[4590]---> BDD-cost:   17
c ---[4588]---> BDD-cost:   17
c ---[4586]---> BDD-cost:   17
c ---[4584]---> BDD-cost:   17
c ---[4582]---> BDD-cost:   17
c ---[4580]---> BDD-cost:   17
c ---[4578]---> BDD-cost:   17
c ---[4576]---> BDD-cost:   17
c ---[4574]---> BDD-cost:   17
c ---[4572]---> BDD-cost:   17
c ---[4570]---> BDD-cost:   17
c ---[4568]---> BDD-cost:   17
c ---[4566]---> BDD-cost:   17
c ---[4265]---> BDD-cost:    7
c ---[4264]---> BDD-cost:    7
c ---[4263]---> BDD-cost:    7
c ---[4262]---> BDD-cost:    7
c ---[4261]---> BDD-cost:    7
c ---[4260]---> BDD-cost:    7
c ---[4259]---> BDD-cost:    7
c ---[4258]---> BDD-cost:    7
c ---[4257]---> BDD-cost:    7
c ---[4256]---> BDD-cost:    7
c ---[4255]---> BDD-cost:    7
c ---[4254]---> BDD-cost:    7
c ---[4253]---> BDD-cost:    7
c ---[4252]---> BDD-cost:    7
c ---[4251]---> BDD-cost:    7
c ---[4250]---> BDD-cost:    7
c ---[4249]---> BDD-cost:    7
c ---[4248]---> BDD-cost:    7
c ---[4247]---> BDD-cost:    7
c ---[4246]---> BDD-cost:    7
c ---[4245]---> BDD-cost:    7
c ---[4244]---> BDD-cost:    7
c ---[4243]---> BDD-cost:    7
c ---[4242]---> BDD-cost:    7
c ---[4241]---> BDD-cost:    7
c ---[4240]---> BDD-cost:    7
c ---[4239]---> BDD-cost:    7
c ---[4238]---> BDD-cost:    7
c ---[4237]---> BDD-cost:    7
c ---[4236]---> BDD-cost:    7
c ---[4235]---> BDD-cost:    7
c ---[4234]---> BDD-cost:    7
c ---[4233]---> BDD-cost:    7
c ---[4232]---> BDD-cost:    7
c ---[4231]---> BDD-cost:    7
c ---[4230]---> BDD-cost:    7
c ---[4229]---> BDD-cost:    7
c ---[4228]---> BDD-cost:    7
c ---[4227]---> BDD-cost:    7
c ---[4226]---> BDD-cost:    7
c ---[4225]---> BDD-cost:    7
c ---[4224]---> BDD-cost:    7
c ---[4223]---> BDD-cost:    7
c ---[4222]---> BDD-cost:    7
c ---[4221]---> BDD-cost:    7
c ---[4220]---> BDD-cost:    7
c ---[4219]---> BDD-cost:    7
c ---[4218]---> BDD-cost:    7
c ---[4217]---> BDD-cost:    7
c ---[4216]---> BDD-cost:    7
c ---[4215]---> BDD-cost:    7
c ---[4214]---> BDD-cost:    7
c ---[4213]---> BDD-cost:    7
c ---[4212]---> BDD-cost:    7
c ---[4211]---> BDD-cost:    7
c ---[4210]---> BDD-cost:    7
c ---[4209]---> BDD-cost:    7
c ---[4208]---> BDD-cost:    7
c ---[4207]---> BDD-cost:    7
c ---[4206]---> BDD-cost:    7
c ---[4204]---> BDD-cost:    9
c ---[4202]---> BDD-cost:    9
c ---[4200]---> BDD-cost:    9
c ---[4198]---> BDD-cost:    9
c ---[4196]---> BDD-cost:    9
c ---[4194]---> BDD-cost:    9
c ---[4192]---> BDD-cost:    9
c ---[4190]---> BDD-cost:    9
c ---[4188]---> BDD-cost:    9
c ---[4186]---> BDD-cost:    9
c ---[4184]---> BDD-cost:    9
c ---[4182]---> BDD-cost:    9
c ---[4180]---> BDD-cost:    9
c ---[4178]---> BDD-cost:    9
c ---[4176]---> BDD-cost:    9
c ---[4174]---> BDD-cost:    9
c ---[4172]---> BDD-cost:    9
c ---[4170]---> BDD-cost:    9
c ---[4168]---> BDD-cost:    9
c ---[4166]---> BDD-cost:    9
c ---[4164]---> BDD-cost:    9
c ---[4162]---> BDD-cost:    9
c ---[4160]---> BDD-cost:    9
c ---[4158]---> BDD-cost:    9
c ---[4156]---> BDD-cost:    9
c ---[4154]---> BDD-cost:    9
c ---[4152]---> BDD-cost:    9
c ---[4150]---> BDD-cost:    9
c ---[4148]---> BDD-cost:    9
c ---[4146]---> BDD-cost:    9
c ---[4144]---> BDD-cost:    9
c ---[4142]---> BDD-cost:    9
c ---[4140]---> BDD-cost:    9
c ---[4138]---> BDD-cost:    9
c ---[4136]---> BDD-cost:    9
c ---[4134]---> BDD-cost:    9
c ---[4132]---> BDD-cost:    9
c ---[4130]---> BDD-cost:    9
c ---[4128]---> BDD-cost:    9
c ---[4126]---> BDD-cost:    9
c ---[4124]---> BDD-cost:    9
c ---[4122]---> BDD-cost:    9
c ---[4120]---> BDD-cost:    9
c ---[4118]---> BDD-cost:    9
c ---[4116]---> BDD-cost:    9
c ---[4114]---> BDD-cost:    9
c ---[4112]---> BDD-cost:    9
c ---[4110]---> BDD-cost:    9
c ---[4108]---> BDD-cost:    9
c ---[4106]---> BDD-cost:    9
c ---[4104]---> BDD-cost:    9
c ---[4102]---> BDD-cost:    9
c ---[4100]---> BDD-cost:    9
c ---[4098]---> BDD-cost:    9
c ---[4096]---> BDD-cost:    9
c ---[4094]---> BDD-cost:    9
c ---[4092]---> BDD-cost:    9
c ---[4090]---> BDD-cost:    9
c ---[4088]---> BDD-cost:    9
c ---[4086]---> BDD-cost:    9
c ---[4079]---> BDD-cost:   64
c ---[4078]---> BDD-cost:   64
c ---[4077]---> BDD-cost:   64
c ---[4076]---> BDD-cost:   64
c ---[4075]---> BDD-cost:   64
c ---[4074]---> BDD-cost:   64
c ---[4067]---> BDD-cost:   67
c ---[4066]---> BDD-cost:   67
c ---[4065]---> BDD-cost:   67
c ---[4064]---> BDD-cost:   67
c ---[4063]---> BDD-cost:   67
c ---[4062]---> BDD-cost:   67
c ---[4055]---> BDD-cost:   67
c ---[4054]---> BDD-cost:   67
c ---[4053]---> BDD-cost:   67
c ---[4052]---> BDD-cost:   67
c ---[4051]---> BDD-cost:   67
c ---[4050]---> BDD-cost:   67
c ---[4043]---> BDD-cost:   67
c ---[4042]---> BDD-cost:   67
c ---[4041]---> BDD-cost:   67
c ---[4040]---> BDD-cost:   67
c ---[4039]---> BDD-cost:   67
c ---[4038]---> BDD-cost:   67
c ---[4031]---> BDD-cost:   67
c ---[4030]---> BDD-cost:   67
c ---[4029]---> BDD-cost:   67
c ---[4028]---> BDD-cost:   67
c ---[4027]---> BDD-cost:   67
c ---[4026]---> BDD-cost:   67
c ---[4019]---> BDD-cost:   67
c ---[4018]---> BDD-cost:   67
c ---[4017]---> BDD-cost:   67
c ---[4016]---> BDD-cost:   67
c ---[4015]---> BDD-cost:   67
c ---[4014]---> BDD-cost:   67
c ---[4007]---> BDD-cost:   67
c ---[4006]---> BDD-cost:   67
c ---[4005]---> BDD-cost:   67
c ---[4004]---> BDD-cost:   67
c ---[4003]---> BDD-cost:   67
c ---[4002]---> BDD-cost:   67
c ---[2050]---> BDD-cost:    7
c ---[2048]---> BDD-cost:    7
c ---[2046]---> BDD-cost:    7
c ---[2044]---> BDD-cost:    7
c ---[2042]---> BDD-cost:    7
c ---[2040]---> BDD-cost:    7
c ---[2038]---> BDD-cost:    7
c ---[2036]---> BDD-cost:    7
c ---[2034]---> BDD-cost:    7
c ---[2032]---> BDD-cost:    7
c ---[2030]---> BDD-cost:    7
c ---[2028]---> BDD-cost:    7
c ---[2026]---> BDD-cost:    7
c ---[2024]---> BDD-cost:    7
c ---[2022]---> BDD-cost:    7
c ---[2020]---> BDD-cost:    7
c ---[2018]---> BDD-cost:    7
c ---[2016]---> BDD-cost:    7
c ---[2014]---> BDD-cost:    7
c ---[2012]---> BDD-cost:    7
c ---[2010]---> BDD-cost:    7
c ---[2008]---> BDD-cost:    7
c ---[2006]---> BDD-cost:    7
c ---[2004]---> BDD-cost:    7
c ---[2002]---> BDD-cost:    7
c ---[2000]---> BDD-cost:    7
c ---[1998]---> BDD-cost:    7
c ---[1996]---> BDD-cost:    7
c ---[1994]---> BDD-cost:    7
c ---[1992]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    7
c ---[1988]---> BDD-cost:    7
c ---[1986]---> BDD-cost:    7
c ---[1984]---> BDD-cost:    7
c ---[1982]---> BDD-cost:    7
c ---[1980]---> BDD-cost:    7
c ---[1978]---> BDD-cost:    7
c ---[1976]---> BDD-cost:    7
c ---[1974]---> BDD-cost:    7
c ---[1972]---> BDD-cost:    7
c ---[1970]---> BDD-cost:    7
c ---[1968]---> BDD-cost:    7
c ---[1966]---> BDD-cost:    7
c ---[1964]---> BDD-cost:    7
c ---[1962]---> BDD-cost:    7
c ---[1960]---> BDD-cost:    7
c ---[1958]---> BDD-cost:    7
c ---[1956]---> BDD-cost:    7
c ---[1954]---> BDD-cost:    7
c ---[1952]---> BDD-cost:    7
c ---[1950]---> BDD-cost:    7
c ---[1948]---> BDD-cost:    7
c ---[1946]---> BDD-cost:    7
c ---[1944]---> BDD-cost:    7
c ---[1942]---> BDD-cost:    7
c ---[1940]---> BDD-cost:    7
c ---[1938]---> BDD-cost:    7
c ---[1936]---> BDD-cost:    7
c ---[1934]---> BDD-cost:    7
c ---[1932]---> BDD-cost:    7
c ---[1931]---> BDD-cost:    7
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:    7
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:    7
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1923]---> BDD-cost:    7
c ---[1922]---> BDD-cost:    7
c ---[1921]---> BDD-cost:    7
c ---[1920]---> BDD-cost:    7
c ---[1919]---> BDD-cost:    9
c ---[1918]---> BDD-cost:    2
c ---[1917]---> BDD-cost:    9
c ---[1916]---> BDD-cost:    2
c ---[1915]---> BDD-cost:    9
c ---[1914]---> BDD-cost:    2
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    2
c ---[1911]---> BDD-cost:    8
c ---[1910]---> BDD-cost:    2
c ---[1909]---> BDD-cost:    8
c ---[1908]---> BDD-cost:    2
c ---[1907]---> BDD-cost:    8
c ---[1906]---> BDD-cost:    2
c ---[1905]---> BDD-cost:    8
c ---[1904]---> BDD-cost:    2
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:    2
c ---[1901]---> BDD-cost:    7
c ---[1900]---> BDD-cost:    2
c ---[1899]---> BDD-cost:    7
c ---[1898]---> BDD-cost:    2
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:    2
c ---[1895]---> BDD-cost:    6
c ---[1894]---> BDD-cost:    2
c ---[1893]---> BDD-cost:    6
c ---[1892]---> BDD-cost:    2
c ---[1891]---> BDD-cost:    6
c ---[1890]---> BDD-cost:    2
c ---[1889]---> BDD-cost:    6
c ---[1888]---> BDD-cost:    2
c ---[1887]---> BDD-cost:    5
c ---[1886]---> BDD-cost:    2
c ---[1885]---> BDD-cost:    5
c ---[1884]---> BDD-cost:    2
c ---[1883]---> BDD-cost:    5
c ---[1882]---> BDD-cost:    2
c ---[1881]---> BDD-cost:    5
c ---[1880]---> BDD-cost:    2
c ---[1879]---> BDD-cost:    4
c ---[1878]---> BDD-cost:    2
c ---[1877]---> BDD-cost:    4
c ---[1876]---> BDD-cost:    2
c ---[1875]---> BDD-cost:    4
c ---[1874]---> BDD-cost:    2
c ---[1873]---> BDD-cost:    4
c ---[1872]---> BDD-cost:    2
c ---[1871]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    2
c ---[1869]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    2
c ---[1867]---> BDD-cost:    3
c ---[1866]---> BDD-cost:    2
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    2
c ---[1855]---> BDD-cost:    6
c ---[1854]---> BDD-cost:    2
c ---[1853]---> BDD-cost:    2
c ---[1852]---> BDD-cost:    2
c ---[1851]---> BDD-cost:    2
c ---[1850]---> BDD-cost:    2
c ---[1849]---> BDD-cost:    2
c ---[1848]---> BDD-cost:    2
c ---[1847]---> BDD-cost:    5
c ---[1846]---> BDD-cost:    2
c ---[1845]---> BDD-cost:    2
c ---[1844]---> BDD-cost:    2
c ---[1843]---> BDD-cost:    2
c ---[1842]---> BDD-cost:    2
c ---[1841]---> BDD-cost:    2
c ---[1840]---> BDD-cost:    2
c ---[1839]---> BDD-cost:    4
c ---[1838]---> BDD-cost:    2
c ---[1837]---> BDD-cost:    2
c ---[1836]---> BDD-cost:    2
c ---[1835]---> BDD-cost:    2
c ---[1834]---> BDD-cost:    2
c ---[1833]---> BDD-cost:    2
c ---[1832]---> BDD-cost:    2
c ---[1831]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    2
c ---[1829]---> BDD-cost:    2
c ---[1828]---> BDD-cost:    2
c ---[1827]---> BDD-cost:    2
c ---[1826]---> BDD-cost:    2
c ---[1825]---> BDD-cost:    2
c ---[1824]---> BDD-cost:    2
c ---[1823]---> BDD-cost:    2
c ---[1822]---> BDD-cost:    2
c ---[1821]---> BDD-cost:    2
c ---[1820]---> BDD-cost:    2
c ---[1819]---> BDD-cost:    2
c ---[1818]---> BDD-cost:    2
c ---[1817]---> BDD-cost:    2
c ---[1816]---> BDD-cost:    2
c ---[1815]---> BDD-cost:    4
c ---[1814]---> BDD-cost:    2
c ---[1813]---> BDD-cost:    2
c ---[1812]---> BDD-cost:    2
c ---[1811]---> BDD-cost:    2
c ---[1810]---> BDD-cost:    2
c ---[1809]---> BDD-cost:    2
c ---[1808]---> BDD-cost:    2
c ---[1807]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    2
c ---[1805]---> BDD-cost:    2
c ---[1804]---> BDD-cost:    2
c ---[1803]---> BDD-cost:    2
c ---[1802]---> BDD-cost:    2
c ---[1801]---> BDD-cost:    2
c ---[1800]---> BDD-cost:    2
c ---[1791]---> BDD-cost:    2
c ---[1790]---> BDD-cost:    2
c ---[1789]---> BDD-cost:    2
c ---[1788]---> BDD-cost:    2
c ---[1787]---> BDD-cost:    2
c ---[1786]---> BDD-cost:    2
c ---[1785]---> BDD-cost:    2
c ---[1784]---> BDD-cost:    2
c ---[1783]---> BDD-cost:    2
c ---[1782]---> BDD-cost:    2
c ---[1781]---> BDD-cost:    2
c ---[1780]---> BDD-cost:    2
c ---[1779]---> BDD-cost:    2
c ---[1778]---> BDD-cost:    2
c ---[1777]---> BDD-cost:    2
c ---[1776]---> BDD-cost:    2
c ---[1775]---> BDD-cost:    2
c ---[1774]---> BDD-cost:    2
c ---[1773]---> BDD-cost:    2
c ---[1772]---> BDD-cost:    2
c ---[1771]---> BDD-cost:    2
c ---[1770]---> BDD-cost:    2
c ---[1769]---> BDD-cost:    2
c ---[1768]---> BDD-cost:    2
c ---[1767]---> BDD-cost:    2
c ---[1766]---> BDD-cost:    2
c ---[1765]---> BDD-cost:    2
c ---[1764]---> BDD-cost:    2
c ---[1763]---> BDD-cost:    2
c ---[1762]---> BDD-cost:    2
c ---[1761]---> BDD-cost:    2
c ---[1760]---> BDD-cost:    2
c ---[1759]---> BDD-cost:    2
c ---[1758]---> BDD-cost:    2
c ---[1757]---> BDD-cost:    2
c ---[1756]---> BDD-cost:    2
c ---[1755]---> BDD-cost:    2
c ---[1754]---> BDD-cost:    2
c ---[1753]---> BDD-cost:    2
c ---[1752]---> BDD-cost:    2
c ---[1751]---> BDD-cost:    2
c ---[1750]---> BDD-cost:    2
c ---[1749]---> BDD-cost:    2
c ---[1748]---> BDD-cost:    2
c ---[1747]---> BDD-cost:    2
c ---[1746]---> BDD-cost:    2
c ---[1745]---> BDD-cost:    2
c ---[1744]---> BDD-cost:    2
c ---[1743]---> BDD-cost:    2
c ---[1742]---> BDD-cost:    2
c ---[1741]---> BDD-cost:    2
c ---[1740]---> BDD-cost:    2
c ---[1739]---> BDD-cost:    2
c ---[1738]---> BDD-cost:    2
c ---[1737]---> BDD-cost:    2
c ---[1736]---> BDD-cost:    2
c ---[1727]---> BDD-cost:    2
c ---[1726]---> BDD-cost:    2
c ---[1725]---> BDD-cost:    2
c ---[1724]---> BDD-cost:    2
c ---[1723]---> BDD-cost:    2
c ---[1722]---> BDD-cost:    2
c ---[1721]---> BDD-cost:    2
c ---[1720]---> BDD-cost:    2
c ---[1719]---> BDD-cost:    2
c ---[1718]---> BDD-cost:    2
c ---[1717]---> BDD-cost:    2
c ---[1716]---> BDD-cost:    2
c ---[1715]---> BDD-cost:    2
c ---[1714]---> BDD-cost:    2
c ---[1713]---> BDD-cost:    2
c ---[1712]---> BDD-cost:    2
c ---[1711]---> BDD-cost:    2
c ---[1710]---> BDD-cost:    2
c ---[1709]---> BDD-cost:    2
c ---[1708]---> BDD-cost:    2
c ---[1707]---> BDD-cost:    2
c ---[1706]---> BDD-cost:    2
c ---[1705]---> BDD-cost:    2
c ---[1704]---> BDD-cost:    2
c ---[1703]---> BDD-cost:    2
c ---[1702]---> BDD-cost:    2
c ---[1701]---> BDD-cost:    2
c ---[1700]---> BDD-cost:    2
c ---[1699]---> BDD-cost:    2
c ---[1698]---> BDD-cost:    2
c ---[1697]---> BDD-cost:    2
c ---[1696]---> BDD-cost:    2
c ---[1695]---> BDD-cost:    2
c ---[1694]---> BDD-cost:    2
c ---[1693]---> BDD-cost:    2
c ---[1692]---> BDD-cost:    2
c ---[1691]---> BDD-cost:    2
c ---[1690]---> BDD-cost:    2
c ---[1689]---> BDD-cost:    2
c ---[1688]---> BDD-cost:    2
c ---[1687]---> BDD-cost:    2
c ---[1686]---> BDD-cost:    2
c ---[1685]---> BDD-cost:    2
c ---[1684]---> BDD-cost:    2
c ---[1683]---> BDD-cost:    2
c ---[1682]---> BDD-cost:    2
c ---[1681]---> BDD-cost:    2
c ---[1680]---> BDD-cost:    2
c ---[1679]---> BDD-cost:    2
c ---[1678]---> BDD-cost:    2
c ---[1677]---> BDD-cost:    2
c ---[1676]---> BDD-cost:    2
c ---[1675]---> BDD-cost:    2
c ---[1674]---> BDD-cost:    2
c ---[1673]---> BDD-cost:    2
c ---[1672]---> BDD-cost:    2
c ---[1663]---> BDD-cost:    2
c ---[1662]---> BDD-cost:    2
c ---[1661]---> BDD-cost:    2
c ---[1660]---> BDD-cost:    2
c ---[1659]---> BDD-cost:    2
c ---[1658]---> BDD-cost:    2
c ---[1657]---> BDD-cost:    2
c ---[1656]---> BDD-cost:    2
c ---[1655]---> BDD-cost:    2
c ---[1654]---> BDD-cost:    2
c ---[1653]---> BDD-cost:    2
c ---[1652]---> BDD-cost:    2
c ---[1651]---> BDD-cost:    2
c ---[1650]---> BDD-cost:    2
c ---[1649]---> BDD-cost:    2
c ---[1648]---> BDD-cost:    2
c ---[1647]---> BDD-cost:    2
c ---[1646]---> BDD-cost:    2
c ---[1645]---> BDD-cost:    2
c ---[1644]---> BDD-cost:    2
c ---[1643]---> BDD-cost:    2
c ---[1642]---> BDD-cost:    2
c ---[1641]---> BDD-cost:    2
c ---[1640]---> BDD-cost:    2
c ---[1639]---> BDD-cost:    2
c ---[1638]---> BDD-cost:    2
c ---[1637]---> BDD-cost:    2
c ---[1636]---> BDD-cost:    2
c ---[1635]---> BDD-cost:    2
c ---[1634]---> BDD-cost:    2
c ---[1633]---> BDD-cost:    2
c ---[1632]---> BDD-cost:    2
c ---[1631]---> BDD-cost:    2
c ---[1630]---> BDD-cost:    2
c ---[1629]---> BDD-cost:    2
c ---[1628]---> BDD-cost:    2
c ---[1627]---> BDD-cost:    2
c ---[1626]---> BDD-cost:    2
c ---[1625]---> BDD-cost:    2
c ---[1624]---> BDD-cost:    2
c ---[1623]---> BDD-cost:    2
c ---[1622]---> BDD-cost:    2
c ---[1621]---> BDD-cost:    2
c ---[1620]---> BDD-cost:    2
c ---[1619]---> BDD-cost:    2
c ---[1618]---> BDD-cost:    2
c ---[1617]---> BDD-cost:    2
c ---[1616]---> BDD-cost:    2
c ---[1615]---> BDD-cost:    2
c ---[1614]---> BDD-cost:    2
c ---[1613]---> BDD-cost:    2
c ---[1612]---> BDD-cost:    2
c ---[1611]---> BDD-cost:    2
c ---[1610]---> BDD-cost:    2
c ---[1609]---> BDD-cost:    2
c ---[1608]---> BDD-cost:    2
c ---[1599]---> BDD-cost:    9
c ---[1598]---> BDD-cost:    2
c ---[1597]---> BDD-cost:    9
c ---[1596]---> BDD-cost:    2
c ---[1595]---> BDD-cost:    9
c ---[1594]---> BDD-cost:    2
c ---[1593]---> BDD-cost:    9
c ---[1592]---> BDD-cost:    2
c ---[1591]---> BDD-cost:    8
c ---[1590]---> BDD-cost:    2
c ---[1589]---> BDD-cost:    8
c ---[1588]---> BDD-cost:    2
c ---[1587]---> BDD-cost:    8
c ---[1586]---> BDD-cost:    2
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    2
c ---[1583]---> BDD-cost:    7
c ---[1582]---> BDD-cost:    2
c ---[1581]---> BDD-cost:    7
c ---[1580]---> BDD-cost:    2
c ---[1579]---> BDD-cost:    7
c ---[1578]---> BDD-cost:    2
c ---[1577]---> BDD-cost:    7
c ---[1576]---> BDD-cost:    2
c ---[1575]---> BDD-cost:    6
c ---[1574]---> BDD-cost:    2
c ---[1573]---> BDD-cost:    6
c ---[1572]---> BDD-cost:    2
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    2
c ---[1569]---> BDD-cost:    6
c ---[1568]---> BDD-cost:    2
c ---[1567]---> BDD-cost:    5
c ---[1566]---> BDD-cost:    2
c ---[1565]---> BDD-cost:    5
c ---[1564]---> BDD-cost:    2
c ---[1563]---> BDD-cost:    5
c ---[1562]---> BDD-cost:    2
c ---[1561]---> BDD-cost:    5
c ---[1560]---> BDD-cost:    2
c ---[1559]---> BDD-cost:    4
c ---[1558]---> BDD-cost:    2
c ---[1557]---> BDD-cost:    4
c ---[1556]---> BDD-cost:    2
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    2
c ---[1553]---> BDD-cost:    4
c ---[1552]---> BDD-cost:    2
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    2
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    2
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    2
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    2
c ---[1535]---> BDD-cost:    6
c ---[1534]---> BDD-cost:    2
c ---[1533]---> BDD-cost:    2
c ---[1532]---> BDD-cost:    2
c ---[1531]---> BDD-cost:    2
c ---[1530]---> BDD-cost:    2
c ---[1529]---> BDD-cost:    2
c ---[1528]---> BDD-cost:    2
c ---[1527]---> BDD-cost:    5
c ---[1526]---> BDD-cost:    2
c ---[1525]---> BDD-cost:    2
c ---[1524]---> BDD-cost:    2
c ---[1523]---> BDD-cost:    2
c ---[1522]---> BDD-cost:    2
c ---[1521]---> BDD-cost:    2
c ---[1520]---> BDD-cost:    2
c ---[1519]---> BDD-cost:    4
c ---[1518]---> BDD-cost:    2
c ---[1517]---> BDD-cost:    2
c ---[1516]---> BDD-cost:    2
c ---[1515]---> BDD-cost:    2
c ---[1514]---> BDD-cost:    2
c ---[1513]---> BDD-cost:    2
c ---[1512]---> BDD-cost:    2
c ---[1511]---> BDD-cost:    3
c ---[1510]---> BDD-cost:    2
c ---[1509]---> BDD-cost:    2
c ---[1508]---> BDD-cost:    2
c ---[1507]---> BDD-cost:    2
c ---[1506]---> BDD-cost:    2
c ---[1505]---> BDD-cost:    2
c ---[1504]---> BDD-cost:    2
c ---[1503]---> BDD-cost:    2
c ---[1502]---> BDD-cost:    2
c ---[1501]---> BDD-cost:    2
c ---[1500]---> BDD-cost:    2
c ---[1499]---> BDD-cost:    2
c ---[1498]---> BDD-cost:    2
c ---[1497]---> BDD-cost:    2
c ---[1496]---> BDD-cost:    2
c ---[1495]---> BDD-cost:    4
c ---[1494]---> BDD-cost:    2
c ---[1493]---> BDD-cost:    2
c ---[1492]---> BDD-cost:    2
c ---[1491]---> BDD-cost:    2
c ---[1490]---> BDD-cost:    2
c ---[1489]---> BDD-cost:    2
c ---[1488]---> BDD-cost:    2
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    2
c ---[1485]---> BDD-cost:    2
c ---[1484]---> BDD-cost:    2
c ---[1483]---> BDD-cost:    2
c ---[1482]---> BDD-cost:    2
c ---[1481]---> BDD-cost:    2
c ---[1480]---> BDD-cost:    2
c ---[1471]---> BDD-cost:    2
c ---[1470]---> BDD-cost:    2
c ---[1469]---> BDD-cost:    2
c ---[1468]---> BDD-cost:    2
c ---[1467]---> BDD-cost:    2
c ---[1466]---> BDD-cost:    2
c ---[1465]---> BDD-cost:    2
c ---[1464]---> BDD-cost:    2
c ---[1463]---> BDD-cost:    2
c ---[1462]---> BDD-cost:    2
c ---[1461]---> BDD-cost:    2
c ---[1460]---> BDD-cost:    2
c ---[1459]---> BDD-cost:    2
c ---[1458]---> BDD-cost:    2
c ---[1457]---> BDD-cost:    2
c ---[1456]---> BDD-cost:    2
c ---[1455]---> BDD-cost:    2
c ---[1454]---> BDD-cost:    2
c ---[1453]---> BDD-cost:    2
c ---[1452]---> BDD-cost:    2
c ---[1451]---> BDD-cost:    2
c ---[1450]---> BDD-cost:    2
c ---[1449]---> BDD-cost:    2
c ---[1448]---> BDD-cost:    2
c ---[1447]---> BDD-cost:    2
c ---[1446]---> BDD-cost:    2
c ---[1445]---> BDD-cost:    2
c ---[1444]---> BDD-cost:    2
c ---[1443]---> BDD-cost:    2
c ---[1442]---> BDD-cost:    2
c ---[1441]---> BDD-cost:    2
c ---[1440]---> BDD-cost:    2
c ---[1439]---> BDD-cost:    2
c ---[1438]---> BDD-cost:    2
c ---[1437]---> BDD-cost:    2
c ---[1436]---> BDD-cost:    2
c ---[1435]---> BDD-cost:    2
c ---[1434]---> BDD-cost:    2
c ---[1433]---> BDD-cost:    2
c ---[1432]---> BDD-cost:    2
c ---[1431]---> BDD-cost:    2
c ---[1430]---> BDD-cost:    2
c ---[1429]---> BDD-cost:    2
c ---[1428]---> BDD-cost:    2
c ---[1427]---> BDD-cost:    2
c ---[1426]---> BDD-cost:    2
c ---[1425]---> BDD-cost:    2
c ---[1424]---> BDD-cost:    2
c ---[1423]---> BDD-cost:    2
c ---[1422]---> BDD-cost:    2
c ---[1421]---> BDD-cost:    2
c ---[1420]---> BDD-cost:    2
c ---[1419]---> BDD-cost:    2
c ---[1418]---> BDD-cost:    2
c ---[1417]---> BDD-cost:    2
c ---[1416]---> BDD-cost:    2
c ---[1407]---> BDD-cost:    2
c ---[1406]---> BDD-cost:    2
c ---[1405]---> BDD-cost:    2
c ---[1404]---> BDD-cost:    2
c ---[1403]---> BDD-cost:    2
c ---[1402]---> BDD-cost:    2
c ---[1401]---> BDD-cost:    2
c ---[1400]---> BDD-cost:    2
c ---[1399]---> BDD-cost:    2
c ---[1398]---> BDD-cost:    2
c ---[1397]---> BDD-cost:    2
c ---[1396]---> BDD-cost:    2
c ---[1395]---> BDD-cost:    2
c ---[1394]---> BDD-cost:    2
c ---[1393]---> BDD-cost:    2
c ---[1392]---> BDD-cost:    2
c ---[1391]---> BDD-cost:    2
c ---[1390]---> BDD-cost:    2
c ---[1389]---> BDD-cost:    2
c ---[1388]---> BDD-cost:    2
c ---[1387]---> BDD-cost:    2
c ---[1386]---> BDD-cost:    2
c ---[1385]---> BDD-cost:    2
c ---[1384]---> BDD-cost:    2
c ---[1383]---> BDD-cost:    2
c ---[1382]---> BDD-cost:    2
c ---[1381]---> BDD-cost:    2
c ---[1380]---> BDD-cost:    2
c ---[1379]---> BDD-cost:    2
c ---[1378]---> BDD-cost:    2
c ---[1377]---> BDD-cost:    2
c ---[1376]---> BDD-cost:    2
c ---[1375]---> BDD-cost:    2
c ---[1374]---> BDD-cost:    2
c ---[1373]---> BDD-cost:    2
c ---[1372]---> BDD-cost:    2
c ---[1371]---> BDD-cost:    2
c ---[1370]---> BDD-cost:    2
c ---[1369]---> BDD-cost:    2
c ---[1368]---> BDD-cost:    2
c ---[1367]---> BDD-cost:    2
c ---[1366]---> BDD-cost:    2
c ---[1365]---> BDD-cost:    2
c ---[1364]---> BDD-cost:    2
c ---[1363]---> BDD-cost:    2
c ---[1362]---> BDD-cost:    2
c ---[1361]---> BDD-cost:    2
c ---[1360]---> BDD-cost:    2
c ---[1359]---> BDD-cost:    2
c ---[1358]---> BDD-cost:    2
c ---[1357]---> BDD-cost:    2
c ---[1356]---> BDD-cost:    2
c ---[1355]---> BDD-cost:    2
c ---[1354]---> BDD-cost:    2
c ---[1353]---> BDD-cost:    2
c ---[1352]---> BDD-cost:    2
c ---[1343]---> BDD-cost:    2
c ---[1342]---> BDD-cost:    2
c ---[1341]---> BDD-cost:    2
c ---[1340]---> BDD-cost:    2
c ---[1339]---> BDD-cost:    2
c ---[1338]---> BDD-cost:    2
c ---[1337]---> BDD-cost:    2
c ---[1336]---> BDD-cost:    2
c ---[1335]---> BDD-cost:    2
c ---[1334]---> BDD-cost:    2
c ---[1333]---> BDD-cost:    2
c ---[1332]---> BDD-cost:    2
c ---[1331]---> BDD-cost:    2
c ---[1330]---> BDD-cost:    2
c ---[1329]---> BDD-cost:    2
c ---[1328]---> BDD-cost:    2
c ---[1327]---> BDD-cost:    2
c ---[1326]---> BDD-cost:    2
c ---[1325]---> BDD-cost:    2
c ---[1324]---> BDD-cost:    2
c ---[1323]---> BDD-cost:    2
c ---[1322]---> BDD-cost:    2
c ---[1321]---> BDD-cost:    2
c ---[1320]---> BDD-cost:    2
c ---[1319]---> BDD-cost:    2
c ---[1318]---> BDD-cost:    2
c ---[1317]---> BDD-cost:    2
c ---[1316]---> BDD-cost:    2
c ---[1315]---> BDD-cost:    2
c ---[1314]---> BDD-cost:    2
c ---[1313]---> BDD-cost:    2
c ---[1312]---> BDD-cost:    2
c ---[1311]---> BDD-cost:    2
c ---[1310]---> BDD-cost:    2
c ---[1309]---> BDD-cost:    2
c ---[1308]---> BDD-cost:    2
c ---[1307]---> BDD-cost:    2
c ---[1306]---> BDD-cost:    2
c ---[1305]---> BDD-cost:    2
c ---[1304]---> BDD-cost:    2
c ---[1303]---> BDD-cost:    2
c ---[1302]---> BDD-cost:    2
c ---[1301]---> BDD-cost:    2
c ---[1300]---> BDD-cost:    2
c ---[1299]---> BDD-cost:    2
c ---[1298]---> BDD-cost:    2
c ---[1297]---> BDD-cost:    2
c ---[1296]---> BDD-cost:    2
c ---[1295]---> BDD-cost:    2
c ---[1294]---> BDD-cost:    2
c ---[1293]---> BDD-cost:    2
c ---[1292]---> BDD-cost:    2
c ---[1291]---> BDD-cost:    2
c ---[1290]---> BDD-cost:    2
c ---[1289]---> BDD-cost:    2
c ---[1288]---> BDD-cost:    2
c ---[1279]---> BDD-cost:    9
c ---[1278]---> BDD-cost:    2
c ---[1277]---> BDD-cost:    9
c ---[1276]---> BDD-cost:    2
c ---[1275]---> BDD-cost:    9
c ---[1274]---> BDD-cost:    2
c ---[1273]---> BDD-cost:    9
c ---[1272]---> BDD-cost:    2
c ---[1271]---> BDD-cost:    8
c ---[1270]---> BDD-cost:    2
c ---[1269]---> BDD-cost:    8
c ---[1268]---> BDD-cost:    2
c ---[1267]---> BDD-cost:    8
c ---[1266]---> BDD-cost:    2
c ---[1265]---> BDD-cost:    8
c ---[1264]---> BDD-cost:    2
c ---[1263]---> BDD-cost:    7
c ---[1262]---> BDD-cost:    2
c ---[1261]---> BDD-cost:    7
c ---[1260]---> BDD-cost:    2
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    2
c ---[1257]---> BDD-cost:    7
c ---[1256]---> BDD-cost:    2
c ---[1255]---> BDD-cost:    6
c ---[1254]---> BDD-cost:    2
c ---[1253]---> BDD-cost:    6
c ---[1252]---> BDD-cost:    2
c ---[1251]---> BDD-cost:    6
c ---[1250]---> BDD-cost:    2
c ---[1249]---> BDD-cost:    6
c ---[1248]---> BDD-cost:    2
c ---[1247]---> BDD-cost:    5
c ---[1246]---> BDD-cost:    2
c ---[1245]---> BDD-cost:    5
c ---[1244]---> BDD-cost:    2
c ---[1243]---> BDD-cost:    5
c ---[1242]---> BDD-cost:    2
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    2
c ---[1239]---> BDD-cost:    4
c ---[1238]---> BDD-cost:    2
c ---[1237]---> BDD-cost:    4
c ---[1236]---> BDD-cost:    2
c ---[1235]---> BDD-cost:    4
c ---[1234]---> BDD-cost:    2
c ---[1233]---> BDD-cost:    4
c ---[1232]---> BDD-cost:    2
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    2
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    2
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    2
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    2
c ---[1215]---> BDD-cost:    6
c ---[1214]---> BDD-cost:    2
c ---[1213]---> BDD-cost:    2
c ---[1212]---> BDD-cost:    2
c ---[1211]---> BDD-cost:    2
c ---[1210]---> BDD-cost:    2
c ---[1209]---> BDD-cost:    2
c ---[1208]---> BDD-cost:    2
c ---[1207]---> BDD-cost:    5
c ---[1206]---> BDD-cost:    2
c ---[1205]---> BDD-cost:    2
c ---[1204]---> BDD-cost:    2
c ---[1203]---> BDD-cost:    2
c ---[1202]---> BDD-cost:    2
c ---[1201]---> BDD-cost:    2
c ---[1200]---> BDD-cost:    2
c ---[1199]---> BDD-cost:    4
c ---[1198]---> BDD-cost:    2
c ---[1197]---> BDD-cost:    2
c ---[1196]---> BDD-cost:    2
c ---[1195]---> BDD-cost:    2
c ---[1194]---> BDD-cost:    2
c ---[1193]---> BDD-cost:    2
c ---[1192]---> BDD-cost:    2
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    2
c ---[1189]---> BDD-cost:    2
c ---[1188]---> BDD-cost:    2
c ---[1187]---> BDD-cost:    2
c ---[1186]---> BDD-cost:    2
c ---[1185]---> BDD-cost:    2
c ---[1184]---> BDD-cost:    2
c ---[1183]---> BDD-cost:    2
c ---[1182]---> BDD-cost:    2
c ---[1181]---> BDD-cost:    2
c ---[1180]---> BDD-cost:    2
c ---[1179]---> BDD-cost:    2
c ---[1178]---> BDD-cost:    2
c ---[1177]---> BDD-cost:    2
c ---[1176]---> BDD-cost:    2
c ---[1175]---> BDD-cost:    4
c ---[1174]---> BDD-cost:    2
c ---[1173]---> BDD-cost:    2
c ---[1172]---> BDD-cost:    2
c ---[1171]---> BDD-cost:    2
c ---[1170]---> BDD-cost:    2
c ---[1169]---> BDD-cost:    2
c ---[1168]---> BDD-cost:    2
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    2
c ---[1165]---> BDD-cost:    2
c ---[1164]---> BDD-cost:    2
c ---[1163]---> BDD-cost:    2
c ---[1162]---> BDD-cost:    2
c ---[1161]---> BDD-cost:    2
c ---[1160]---> BDD-cost:    2
c ---[1151]---> BDD-cost:    2
c ---[1150]---> BDD-cost:    2
c ---[1149]---> BDD-cost:    2
c ---[1148]---> BDD-cost:    2
c ---[1147]---> BDD-cost:    2
c ---[1146]---> BDD-cost:    2
c ---[1145]---> BDD-cost:    2
c ---[1144]---> BDD-cost:    2
c ---[1143]---> BDD-cost:    2
c ---[1142]---> BDD-cost:    2
c ---[1141]---> BDD-cost:    2
c ---[1140]---> BDD-cost:    2
c ---[1139]---> BDD-cost:    2
c ---[1138]---> BDD-cost:    2
c ---[1137]---> BDD-cost:    2
c ---[1136]---> BDD-cost:    2
c ---[1135]---> BDD-cost:    2
c ---[1134]---> BDD-cost:    2
c ---[1133]---> BDD-cost:    2
c ---[1132]---> BDD-cost:    2
c ---[1131]---> BDD-cost:    2
c ---[1130]---> BDD-cost:    2
c ---[1129]---> BDD-cost:    2
c ---[1128]---> BDD-cost:    2
c ---[1127]---> BDD-cost:    2
c ---[1126]---> BDD-cost:    2
c ---[1125]---> BDD-cost:    2
c ---[1124]---> BDD-cost:    2
c ---[1123]---> BDD-cost:    2
c ---[1122]---> BDD-cost:    2
c ---[1121]---> BDD-cost:    2
c ---[1120]---> BDD-cost:    2
c ---[1119]---> BDD-cost:    2
c ---[1118]---> BDD-cost:    2
c ---[1117]---> BDD-cost:    2
c ---[1116]---> BDD-cost:    2
c ---[1115]---> BDD-cost:    2
c ---[1114]---> BDD-cost:    2
c ---[1113]---> BDD-cost:    2
c ---[1112]---> BDD-cost:    2
c ---[1111]---> BDD-cost:    2
c ---[1110]---> BDD-cost:    2
c ---[1109]---> BDD-cost:    2
c ---[1108]---> BDD-cost:    2
c ---[1107]---> BDD-cost:    2
c ---[1106]---> BDD-cost:    2
c ---[1105]---> BDD-cost:    2
c ---[1104]---> BDD-cost:    2
c ---[1103]---> BDD-cost:    2
c ---[1102]---> BDD-cost:    2
c ---[1101]---> BDD-cost:    2
c ---[1100]---> BDD-cost:    2
c ---[1099]---> BDD-cost:    2
c ---[1098]---> BDD-cost:    2
c ---[1097]---> BDD-cost:    2
c ---[1096]---> BDD-cost:    2
c ---[1087]---> BDD-cost:    2
c ---[1086]---> BDD-cost:    2
c ---[1085]---> BDD-cost:    2
c ---[1084]---> BDD-cost:    2
c ---[1083]---> BDD-cost:    2
c ---[1082]---> BDD-cost:    2
c ---[1081]---> BDD-cost:    2
c ---[1080]---> BDD-cost:    2
c ---[1079]---> BDD-cost:    2
c ---[1078]---> BDD-cost:    2
c ---[1077]---> BDD-cost:    2
c ---[1076]---> BDD-cost:    2
c ---[1075]---> BDD-cost:    2
c ---[1074]---> BDD-cost:    2
c ---[1073]---> BDD-cost:    2
c ---[1072]---> BDD-cost:    2
c ---[1071]---> BDD-cost:    2
c ---[1070]---> BDD-cost:    2
c ---[1069]---> BDD-cost:    2
c ---[1068]---> BDD-cost:    2
c ---[1067]---> BDD-cost:    2
c ---[1066]---> BDD-cost:    2
c ---[1065]---> BDD-cost:    2
c ---[1064]---> BDD-cost:    2
c ---[1063]---> BDD-cost:    2
c ---[1062]---> BDD-cost:    2
c ---[1061]---> BDD-cost:    2
c ---[1060]---> BDD-cost:    2
c ---[1059]---> BDD-cost:    2
c ---[1058]---> BDD-cost:    2
c ---[1057]---> BDD-cost:    2
c ---[1056]---> BDD-cost:    2
c ---[1055]---> BDD-cost:    2
c ---[1054]---> BDD-cost:    2
c ---[1053]---> BDD-cost:    2
c ---[1052]---> BDD-cost:    2
c ---[1051]---> BDD-cost:    2
c ---[1050]---> BDD-cost:    2
c ---[1049]---> BDD-cost:    2
c ---[1048]---> BDD-cost:    2
c ---[1047]---> BDD-cost:    2
c ---[1046]---> BDD-cost:    2
c ---[1045]---> BDD-cost:    2
c ---[1044]---> BDD-cost:    2
c ---[1043]---> BDD-cost:    2
c ---[1042]---> BDD-cost:    2
c ---[1041]---> BDD-cost:    2
c ---[1040]---> BDD-cost:    2
c ---[1039]---> BDD-cost:    2
c ---[1038]---> BDD-cost:    2
c ---[1037]---> BDD-cost:    2
c ---[1036]---> BDD-cost:    2
c ---[1035]---> BDD-cost:    2
c ---[1034]---> BDD-cost:    2
c ---[1033]---> BDD-cost:    2
c ---[1032]---> BDD-cost:    2
c ---[1023]---> BDD-cost:    2
c ---[1022]---> BDD-cost:    2
c ---[1021]---> BDD-cost:    2
c ---[1020]---> BDD-cost:    2
c ---[1019]---> BDD-cost:    2
c ---[1018]---> BDD-cost:    2
c ---[1017]---> BDD-cost:    2
c ---[1016]---> BDD-cost:    2
c ---[1015]---> BDD-cost:    2
c ---[1014]---> BDD-cost:    2
c ---[1013]---> BDD-cost:    2
c ---[1012]---> BDD-cost:    2
c ---[1011]---> BDD-cost:    2
c ---[1010]---> BDD-cost:    2
c ---[1009]---> BDD-cost:    2
c ---[1008]---> BDD-cost:    2
c ---[1007]---> BDD-cost:    2
c ---[1006]---> BDD-cost:    2
c ---[1005]---> BDD-cost:    2
c ---[1004]---> BDD-cost:    2
c ---[1003]---> BDD-cost:    2
c ---[1002]---> BDD-cost:    2
c ---[1001]---> BDD-cost:    2
c ---[1000]---> BDD-cost:    2
c ---[ 999]---> BDD-cost:    2
c ---[ 998]---> BDD-cost:    2
c ---[ 997]---> BDD-cost:    2
c ---[ 996]---> BDD-cost:    2
c ---[ 995]---> BDD-cost:    2
c ---[ 994]---> BDD-cost:    2
c ---[ 993]---> BDD-cost:    2
c ---[ 992]---> BDD-cost:    2
c ---[ 991]---> BDD-cost:    2
c ---[ 990]---> BDD-cost:    2
c ---[ 989]---> BDD-cost:    2
c ---[ 988]---> BDD-cost:    2
c ---[ 987]---> BDD-cost:    2
c ---[ 986]---> BDD-cost:    2
c ---[ 985]---> BDD-cost:    2
c ---[ 984]---> BDD-cost:    2
c ---[ 983]---> BDD-cost:    2
c ---[ 982]---> BDD-cost:    2
c ---[ 981]---> BDD-cost:    2
c ---[ 980]---> BDD-cost:    2
c ---[ 979]---> BDD-cost:    2
c ---[ 978]---> BDD-cost:    2
c ---[ 977]---> BDD-cost:    2
c ---[ 976]---> BDD-cost:    2
c ---[ 975]---> BDD-cost:    2
c ---[ 974]---> BDD-cost:    2
c ---[ 973]---> BDD-cost:    2
c ---[ 972]---> BDD-cost:    2
c ---[ 971]---> BDD-cost:    2
c ---[ 970]---> BDD-cost:    2
c ---[ 969]---> BDD-cost:    2
c ---[ 968]---> BDD-cost:    2
c ---[ 959]---> BDD-cost:    9
c ---[ 958]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    9
c ---[ 956]---> BDD-cost:    2
c ---[ 955]---> BDD-cost:    9
c ---[ 954]---> BDD-cost:    2
c ---[ 953]---> BDD-cost:    9
c ---[ 952]---> BDD-cost:    2
c ---[ 951]---> BDD-cost:    8
c ---[ 950]---> BDD-cost:    2
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    2
c ---[ 947]---> BDD-cost:    8
c ---[ 946]---> BDD-cost:    2
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    2
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    2
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    2
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    2
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    2
c ---[ 935]---> BDD-cost:    6
c ---[ 934]---> BDD-cost:    2
c ---[ 933]---> BDD-cost:    6
c ---[ 932]---> BDD-cost:    2
c ---[ 931]---> BDD-cost:    6
c ---[ 930]---> BDD-cost:    2
c ---[ 929]---> BDD-cost:    6
c ---[ 928]---> BDD-cost:    2
c ---[ 927]---> BDD-cost:    5
c ---[ 926]---> BDD-cost:    2
c ---[ 925]---> BDD-cost:    5
c ---[ 924]---> BDD-cost:    2
c ---[ 923]---> BDD-cost:    5
c ---[ 922]---> BDD-cost:    2
c ---[ 921]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:    2
c ---[ 919]---> BDD-cost:    4
c ---[ 918]---> BDD-cost:    2
c ---[ 917]---> BDD-cost:    4
c ---[ 916]---> BDD-cost:    2
c ---[ 915]---> BDD-cost:    4
c ---[ 914]---> BDD-cost:    2
c ---[ 913]---> BDD-cost:    4
c ---[ 912]---> BDD-cost:    2
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    2
c ---[ 909]---> BDD-cost:    3
c ---[ 908]---> BDD-cost:    2
c ---[ 907]---> BDD-cost:    3
c ---[ 906]---> BDD-cost:    2
c ---[ 905]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    2
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    2
c ---[ 893]---> BDD-cost:    2
c ---[ 892]---> BDD-cost:    2
c ---[ 891]---> BDD-cost:    2
c ---[ 890]---> BDD-cost:    2
c ---[ 889]---> BDD-cost:    2
c ---[ 888]---> BDD-cost:    2
c ---[ 887]---> BDD-cost:    5
c ---[ 886]---> BDD-cost:    2
c ---[ 885]---> BDD-cost:    2
c ---[ 884]---> BDD-cost:    2
c ---[ 883]---> BDD-cost:    2
c ---[ 882]---> BDD-cost:    2
c ---[ 881]---> BDD-cost:    2
c ---[ 880]---> BDD-cost:    2
c ---[ 879]---> BDD-cost:    4
c ---[ 878]---> BDD-cost:    2
c ---[ 877]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    2
c ---[ 875]---> BDD-cost:    2
c ---[ 874]---> BDD-cost:    2
c ---[ 873]---> BDD-cost:    2
c ---[ 872]---> BDD-cost:    2
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    2
c ---[ 869]---> BDD-cost:    2
c ---[ 868]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 866]---> BDD-cost:    2
c ---[ 865]---> BDD-cost:    2
c ---[ 864]---> BDD-cost:    2
c ---[ 863]---> BDD-cost:    2
c ---[ 862]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 859]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    2
c ---[ 857]---> BDD-cost:    2
c ---[ 856]---> BDD-cost:    2
c ---[ 855]---> BDD-cost:    4
c ---[ 854]---> BDD-cost:    2
c ---[ 853]---> BDD-cost:    2
c ---[ 852]---> BDD-cost:    2
c ---[ 851]---> BDD-cost:    2
c ---[ 850]---> BDD-cost:    2
c ---[ 849]---> BDD-cost:    2
c ---[ 848]---> BDD-cost:    2
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 844]---> BDD-cost:    2
c ---[ 843]---> BDD-cost:    2
c ---[ 842]---> BDD-cost:    2
c ---[ 841]---> BDD-cost:    2
c ---[ 840]---> BDD-cost:    2
c ---[ 831]---> BDD-cost:    2
c ---[ 830]---> BDD-cost:    2
c ---[ 829]---> BDD-cost:    2
c ---[ 828]---> BDD-cost:    2
c ---[ 827]---> BDD-cost:    2
c ---[ 826]---> BDD-cost:    2
c ---[ 825]---> BDD-cost:    2
c ---[ 824]---> BDD-cost:    2
c ---[ 823]---> BDD-cost:    2
c ---[ 822]---> BDD-cost:    2
c ---[ 821]---> BDD-cost:    2
c ---[ 820]---> BDD-cost:    2
c ---[ 819]---> BDD-cost:    2
c ---[ 818]---> BDD-cost:    2
c ---[ 817]---> BDD-cost:    2
c ---[ 816]---> BDD-cost:    2
c ---[ 815]---> BDD-cost:    2
c ---[ 814]---> BDD-cost:    2
c ---[ 813]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 811]---> BDD-cost:    2
c ---[ 810]---> BDD-cost:    2
c ---[ 809]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    2
c ---[ 807]---> BDD-cost:    2
c ---[ 806]---> BDD-cost:    2
c ---[ 805]---> BDD-cost:    2
c ---[ 804]---> BDD-cost:    2
c ---[ 803]---> BDD-cost:    2
c ---[ 802]---> BDD-cost:    2
c ---[ 801]---> BDD-cost:    2
c ---[ 800]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 798]---> BDD-cost:    2
c ---[ 797]---> BDD-cost:    2
c ---[ 796]---> BDD-cost:    2
c ---[ 795]---> BDD-cost:    2
c ---[ 794]---> BDD-cost:    2
c ---[ 793]---> BDD-cost:    2
c ---[ 792]---> BDD-cost:    2
c ---[ 791]---> BDD-cost:    2
c ---[ 790]---> BDD-cost:    2
c ---[ 789]---> BDD-cost:    2
c ---[ 788]---> BDD-cost:    2
c ---[ 787]---> BDD-cost:    2
c ---[ 786]---> BDD-cost:    2
c ---[ 785]---> BDD-cost:    2
c ---[ 784]---> BDD-cost:    2
c ---[ 783]---> BDD-cost:    2
c ---[ 782]---> BDD-cost:    2
c ---[ 781]---> BDD-cost:    2
c ---[ 780]---> BDD-cost:    2
c ---[ 779]---> BDD-cost:    2
c ---[ 778]---> BDD-cost:    2
c ---[ 777]---> BDD-cost:    2
c ---[ 776]---> BDD-cost:    2
c ---[ 767]---> BDD-cost:    2
c ---[ 766]---> BDD-cost:    2
c ---[ 765]---> BDD-cost:    2
c ---[ 764]---> BDD-cost:    2
c ---[ 763]---> BDD-cost:    2
c ---[ 762]---> BDD-cost:    2
c ---[ 761]---> BDD-cost:    2
c ---[ 760]---> BDD-cost:    2
c ---[ 759]---> BDD-cost:    2
c ---[ 758]---> BDD-cost:    2
c ---[ 757]---> BDD-cost:    2
c ---[ 756]---> BDD-cost:    2
c ---[ 755]---> BDD-cost:    2
c ---[ 754]---> BDD-cost:    2
c ---[ 753]---> BDD-cost:    2
c ---[ 752]---> BDD-cost:    2
c ---[ 751]---> BDD-cost:    2
c ---[ 750]---> BDD-cost:    2
c ---[ 749]---> BDD-cost:    2
c ---[ 748]---> BDD-cost:    2
c ---[ 747]---> BDD-cost:    2
c ---[ 746]---> BDD-cost:    2
c ---[ 745]---> BDD-cost:    2
c ---[ 744]---> BDD-cost:    2
c ---[ 743]---> BDD-cost:    2
c ---[ 742]---> BDD-cost:    2
c ---[ 741]---> BDD-cost:    2
c ---[ 740]---> BDD-cost:    2
c ---[ 739]---> BDD-cost:    2
c ---[ 738]---> BDD-cost:    2
c ---[ 737]---> BDD-cost:    2
c ---[ 736]---> BDD-cost:    2
c ---[ 735]---> BDD-cost:    2
c ---[ 734]---> BDD-cost:    2
c ---[ 733]---> BDD-cost:    2
c ---[ 732]---> BDD-cost:    2
c ---[ 731]---> BDD-cost:    2
c ---[ 730]---> BDD-cost:    2
c ---[ 729]---> BDD-cost:    2
c ---[ 728]---> BDD-cost:    2
c ---[ 727]---> BDD-cost:    2
c ---[ 726]---> BDD-cost:    2
c ---[ 725]---> BDD-cost:    2
c ---[ 724]---> BDD-cost:    2
c ---[ 723]---> BDD-cost:    2
c ---[ 722]---> BDD-cost:    2
c ---[ 721]---> BDD-cost:    2
c ---[ 720]---> BDD-cost:    2
c ---[ 719]---> BDD-cost:    2
c ---[ 718]---> BDD-cost:    2
c ---[ 717]---> BDD-cost:    2
c ---[ 716]---> BDD-cost:    2
c ---[ 715]---> BDD-cost:    2
c ---[ 714]---> BDD-cost:    2
c ---[ 713]---> BDD-cost:    2
c ---[ 712]---> BDD-cost:    2
c ---[ 703]---> BDD-cost:    2
c ---[ 702]---> BDD-cost:    2
c ---[ 701]---> BDD-cost:    2
c ---[ 700]---> BDD-cost:    2
c ---[ 699]---> BDD-cost:    2
c ---[ 698]---> BDD-cost:    2
c ---[ 697]---> BDD-cost:    2
c ---[ 696]---> BDD-cost:    2
c ---[ 695]---> BDD-cost:    2
c ---[ 694]---> BDD-cost:    2
c ---[ 693]---> BDD-cost:    2
c ---[ 692]---> BDD-cost:    2
c ---[ 691]---> BDD-cost:    2
c ---[ 690]---> BDD-cost:    2
c ---[ 689]---> BDD-cost:    2
c ---[ 688]---> BDD-cost:    2
c ---[ 687]---> BDD-cost:    2
c ---[ 686]---> BDD-cost:    2
c ---[ 685]---> BDD-cost:    2
c ---[ 684]---> BDD-cost:    2
c ---[ 683]---> BDD-cost:    2
c ---[ 682]---> BDD-cost:    2
c ---[ 681]---> BDD-cost:    2
c ---[ 680]---> BDD-cost:    2
c ---[ 679]---> BDD-cost:    2
c ---[ 678]---> BDD-cost:    2
c ---[ 677]---> BDD-cost:    2
c ---[ 676]---> BDD-cost:    2
c ---[ 675]---> BDD-cost:    2
c ---[ 674]---> BDD-cost:    2
c ---[ 673]---> BDD-cost:    2
c ---[ 672]---> BDD-cost:    2
c ---[ 671]---> BDD-cost:    2
c ---[ 670]---> BDD-cost:    2
c ---[ 669]---> BDD-cost:    2
c ---[ 668]---> BDD-cost:    2
c ---[ 667]---> BDD-cost:    2
c ---[ 666]---> BDD-cost:    2
c ---[ 665]---> BDD-cost:    2
c ---[ 664]---> BDD-cost:    2
c ---[ 663]---> BDD-cost:    2
c ---[ 662]---> BDD-cost:    2
c ---[ 661]---> BDD-cost:    2
c ---[ 660]---> BDD-cost:    2
c ---[ 659]---> BDD-cost:    2
c ---[ 658]---> BDD-cost:    2
c ---[ 657]---> BDD-cost:    2
c ---[ 656]---> BDD-cost:    2
c ---[ 655]---> BDD-cost:    2
c ---[ 654]---> BDD-cost:    2
c ---[ 653]---> BDD-cost:    2
c ---[ 652]---> BDD-cost:    2
c ---[ 651]---> BDD-cost:    2
c ---[ 650]---> BDD-cost:    2
c ---[ 649]---> BDD-cost:    2
c ---[ 648]---> BDD-cost:    2
c ---[ 639]---> BDD-cost:    9
c ---[ 638]---> BDD-cost:    2
c ---[ 637]---> BDD-cost:    9
c ---[ 636]---> BDD-cost:    2
c ---[ 635]---> BDD-cost:    9
c ---[ 634]---> BDD-cost:    2
c ---[ 633]---> BDD-cost:    9
c ---[ 632]---> BDD-cost:    2
c ---[ 631]---> BDD-cost:    8
c ---[ 630]---> BDD-cost:    2
c ---[ 629]---> BDD-cost:    8
c ---[ 628]---> BDD-cost:    2
c ---[ 627]---> BDD-cost:    8
c ---[ 626]---> BDD-cost:    2
c ---[ 625]---> BDD-cost:    8
c ---[ 624]---> BDD-cost:    2
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    2
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    2
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    2
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    2
c ---[ 615]---> BDD-cost:    6
c ---[ 614]---> BDD-cost:    2
c ---[ 613]---> BDD-cost:    6
c ---[ 612]---> BDD-cost:    2
c ---[ 611]---> BDD-cost:    6
c ---[ 610]---> BDD-cost:    2
c ---[ 609]---> BDD-cost:    6
c ---[ 608]---> BDD-cost:    2
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:    2
c ---[ 605]---> BDD-cost:    5
c ---[ 604]---> BDD-cost:    2
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    2
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost:    2
c ---[ 599]---> BDD-cost:    4
c ---[ 598]---> BDD-cost:    2
c ---[ 597]---> BDD-cost:    4
c ---[ 596]---> BDD-cost:    2
c ---[ 595]---> BDD-cost:    4
c ---[ 594]---> BDD-cost:    2
c ---[ 593]---> BDD-cost:    4
c ---[ 592]---> BDD-cost:    2
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    2
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    2
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    2
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    2
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    2
c ---[ 573]---> BDD-cost:    2
c ---[ 572]---> BDD-cost:    2
c ---[ 571]---> BDD-cost:    2
c ---[ 570]---> BDD-cost:    2
c ---[ 569]---> BDD-cost:    2
c ---[ 568]---> BDD-cost:    2
c ---[ 567]---> BDD-cost:    5
c ---[ 566]---> BDD-cost:    2
c ---[ 565]---> BDD-cost:    2
c ---[ 564]---> BDD-cost:    2
c ---[ 563]---> BDD-cost:    2
c ---[ 562]---> BDD-cost:    2
c ---[ 561]---> BDD-cost:    2
c ---[ 560]---> BDD-cost:    2
c ---[ 559]---> BDD-cost:    4
c ---[ 558]---> BDD-cost:    2
c ---[ 557]---> BDD-cost:    2
c ---[ 556]---> BDD-cost:    2
c ---[ 555]---> BDD-cost:    2
c ---[ 554]---> BDD-cost:    2
c ---[ 553]---> BDD-cost:    2
c ---[ 552]---> BDD-cost:    2
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    2
c ---[ 549]---> BDD-cost:    2
c ---[ 548]---> BDD-cost:    2
c ---[ 547]---> BDD-cost:    2
c ---[ 546]---> BDD-cost:    2
c ---[ 545]---> BDD-cost:    2
c ---[ 544]---> BDD-cost:    2
c ---[ 543]---> BDD-cost:    2
c ---[ 542]---> BDD-cost:    2
c ---[ 541]---> BDD-cost:    2
c ---[ 540]---> BDD-cost:    2
c ---[ 539]---> BDD-cost:    2
c ---[ 538]---> BDD-cost:    2
c ---[ 537]---> BDD-cost:    2
c ---[ 536]---> BDD-cost:    2
c ---[ 535]---> BDD-cost:    4
c ---[ 534]---> BDD-cost:    2
c ---[ 533]---> BDD-cost:    2
c ---[ 532]---> BDD-cost:    2
c ---[ 531]---> BDD-cost:    2
c ---[ 530]---> BDD-cost:    2
c ---[ 529]---> BDD-cost:    2
c ---[ 528]---> BDD-cost:    2
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    2
c ---[ 525]---> BDD-cost:    2
c ---[ 524]---> BDD-cost:    2
c ---[ 523]---> BDD-cost:    2
c ---[ 522]---> BDD-cost:    2
c ---[ 521]---> BDD-cost:    2
c ---[ 520]---> BDD-cost:    2
c ---[ 511]---> BDD-cost:    2
c ---[ 510]---> BDD-cost:    2
c ---[ 509]---> BDD-cost:    2
c ---[ 508]---> BDD-cost:    2
c ---[ 507]---> BDD-cost:    2
c ---[ 506]---> BDD-cost:    2
c ---[ 505]---> BDD-cost:    2
c ---[ 504]---> BDD-cost:    2
c ---[ 503]---> BDD-cost:    2
c ---[ 502]---> BDD-cost:    2
c ---[ 501]---> BDD-cost:    2
c ---[ 500]---> BDD-cost:    2
c ---[ 499]---> BDD-cost:    2
c ---[ 498]---> BDD-cost:    2
c ---[ 497]---> BDD-cost:    2
c ---[ 496]---> BDD-cost:    2
c ---[ 495]---> BDD-cost:    2
c ---[ 494]---> BDD-cost:    2
c ---[ 493]---> BDD-cost:    2
c ---[ 492]---> BDD-cost:    2
c ---[ 491]---> BDD-cost:    2
c ---[ 490]---> BDD-cost:    2
c ---[ 489]---> BDD-cost:    2
c ---[ 488]---> BDD-cost:    2
c ---[ 487]---> BDD-cost:    2
c ---[ 486]---> BDD-cost:    2
c ---[ 485]---> BDD-cost:    2
c ---[ 484]---> BDD-cost:    2
c ---[ 483]---> BDD-cost:    2
c ---[ 482]---> BDD-cost:    2
c ---[ 481]---> BDD-cost:    2
c ---[ 480]---> BDD-cost:    2
c ---[ 479]---> BDD-cost:    2
c ---[ 478]---> BDD-cost:    2
c ---[ 477]---> BDD-cost:    2
c ---[ 476]---> BDD-cost:    2
c ---[ 475]---> BDD-cost:    2
c ---[ 474]---> BDD-cost:    2
c ---[ 473]---> BDD-cost:    2
c ---[ 472]---> BDD-cost:    2
c ---[ 471]---> BDD-cost:    2
c ---[ 470]---> BDD-cost:    2
c ---[ 469]---> BDD-cost:    2
c ---[ 468]---> BDD-cost:    2
c ---[ 467]---> BDD-cost:    2
c ---[ 466]---> BDD-cost:    2
c ---[ 465]---> BDD-cost:    2
c ---[ 464]---> BDD-cost:    2
c ---[ 463]---> BDD-cost:    2
c ---[ 462]---> BDD-cost:    2
c ---[ 461]---> BDD-cost:    2
c ---[ 460]---> BDD-cost:    2
c ---[ 459]---> BDD-cost:    2
c ---[ 458]---> BDD-cost:    2
c ---[ 457]---> BDD-cost:    2
c ---[ 456]---> BDD-cost:    2
c ---[ 447]---> BDD-cost:    2
c ---[ 446]---> BDD-cost:    2
c ---[ 445]---> BDD-cost:    2
c ---[ 444]---> BDD-cost:    2
c ---[ 443]---> BDD-cost:    2
c ---[ 442]---> BDD-cost:    2
c ---[ 441]---> BDD-cost:    2
c ---[ 440]---> BDD-cost:    2
c ---[ 439]---> BDD-cost:    2
c ---[ 438]---> BDD-cost:    2
c ---[ 437]---> BDD-cost:    2
c ---[ 436]---> BDD-cost:    2
c ---[ 435]---> BDD-cost:    2
c ---[ 434]---> BDD-cost:    2
c ---[ 433]---> BDD-cost:    2
c ---[ 432]---> BDD-cost:    2
c ---[ 431]---> BDD-cost:    2
c ---[ 430]---> BDD-cost:    2
c ---[ 429]---> BDD-cost:    2
c ---[ 428]---> BDD-cost:    2
c ---[ 427]---> BDD-cost:    2
c ---[ 426]---> BDD-cost:    2
c ---[ 425]---> BDD-cost:    2
c ---[ 424]---> BDD-cost:    2
c ---[ 423]---> BDD-cost:    2
c ---[ 422]---> BDD-cost:    2
c ---[ 421]---> BDD-cost:    2
c ---[ 420]---> BDD-cost:    2
c ---[ 419]---> BDD-cost:    2
c ---[ 418]---> BDD-cost:    2
c ---[ 417]---> BDD-cost:    2
c ---[ 416]---> BDD-cost:    2
c ---[ 415]---> BDD-cost:    2
c ---[ 414]---> BDD-cost:    2
c ---[ 413]---> BDD-cost:    2
c ---[ 412]---> BDD-cost:    2
c ---[ 411]---> BDD-cost:    2
c ---[ 410]---> BDD-cost:    2
c ---[ 409]---> BDD-cost:    2
c ---[ 408]---> BDD-cost:    2
c ---[ 407]---> BDD-cost:    2
c ---[ 406]---> BDD-cost:    2
c ---[ 405]---> BDD-cost:    2
c ---[ 404]---> BDD-cost:    2
c ---[ 403]---> BDD-cost:    2
c ---[ 402]---> BDD-cost:    2
c ---[ 401]---> BDD-cost:    2
c ---[ 400]---> BDD-cost:    2
c ---[ 399]---> BDD-cost:    2
c ---[ 398]---> BDD-cost:    2
c ---[ 397]---> BDD-cost:    2
c ---[ 396]---> BDD-cost:    2
c ---[ 395]---> BDD-cost:    2
c ---[ 394]---> BDD-cost:    2
c ---[ 393]---> BDD-cost:    2
c ---[ 392]---> BDD-cost:    2
c ---[ 383]---> BDD-cost:    2
c ---[ 382]---> BDD-cost:    2
c ---[ 381]---> BDD-cost:    2
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:    2
c ---[ 378]---> BDD-cost:    2
c ---[ 377]---> BDD-cost:    2
c ---[ 376]---> BDD-cost:    2
c ---[ 375]---> BDD-cost:    2
c ---[ 374]---> BDD-cost:    2
c ---[ 373]---> BDD-cost:    2
c ---[ 372]---> BDD-cost:    2
c ---[ 371]---> BDD-cost:    2
c ---[ 370]---> BDD-cost:    2
c ---[ 369]---> BDD-cost:    2
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:    2
c ---[ 366]---> BDD-cost:    2
c ---[ 365]---> BDD-cost:    2
c ---[ 364]---> BDD-cost:    2
c ---[ 363]---> BDD-cost:    2
c ---[ 362]---> BDD-cost:    2
c ---[ 361]---> BDD-cost:    2
c ---[ 360]---> BDD-cost:    2
c ---[ 359]---> BDD-cost:    2
c ---[ 358]---> BDD-cost:    2
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:    2
c ---[ 355]---> BDD-cost:    2
c ---[ 354]---> BDD-cost:    2
c ---[ 353]---> BDD-cost:    2
c ---[ 352]---> BDD-cost:    2
c ---[ 351]---> BDD-cost:    2
c ---[ 350]---> BDD-cost:    2
c ---[ 349]---> BDD-cost:    2
c ---[ 348]---> BDD-cost:    2
c ---[ 347]---> BDD-cost:    2
c ---[ 346]---> BDD-cost:    2
c ---[ 345]---> BDD-cost:    2
c ---[ 344]---> BDD-cost:    2
c ---[ 343]---> BDD-cost:    2
c ---[ 342]---> BDD-cost:    2
c ---[ 341]---> BDD-cost:    2
c ---[ 340]---> BDD-cost:    2
c ---[ 339]---> BDD-cost:    2
c ---[ 338]---> BDD-cost:    2
c ---[ 337]---> BDD-cost:    2
c ---[ 336]---> BDD-cost:    2
c ---[ 335]---> BDD-cost:    2
c ---[ 334]---> BDD-cost:    2
c ---[ 333]---> BDD-cost:    2
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    2
c ---[ 330]---> BDD-cost:    2
c ---[ 329]---> BDD-cost:    2
c ---[ 328]---> BDD-cost:    2
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    2
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    2
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    2
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    2
c ---[ 311]---> BDD-cost:    8
c ---[ 310]---> BDD-cost:    2
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    2
c ---[ 307]---> BDD-cost:    8
c ---[ 306]---> BDD-cost:    2
c ---[ 305]---> BDD-cost:    8
c ---[ 304]---> BDD-cost:    2
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    2
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    2
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    2
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    2
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    2
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    2
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    2
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    2
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:    2
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:    2
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    2
c ---[ 281]---> BDD-cost:    5
c ---[ 280]---> BDD-cost:    2
c ---[ 279]---> BDD-cost:    4
c ---[ 278]---> BDD-cost:    2
c ---[ 277]---> BDD-cost:    4
c ---[ 276]---> BDD-cost:    2
c ---[ 275]---> BDD-cost:    4
c ---[ 274]---> BDD-cost:    2
c ---[ 273]---> BDD-cost:    4
c ---[ 272]---> BDD-cost:    2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    2
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    2
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    2
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    2
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    2
c ---[ 253]---> BDD-cost:    2
c ---[ 252]---> BDD-cost:    2
c ---[ 251]---> BDD-cost:    2
c ---[ 250]---> BDD-cost:    2
c ---[ 249]---> BDD-cost:    2
c ---[ 248]---> BDD-cost:    2
c ---[ 247]---> BDD-cost:    5
c ---[ 246]---> BDD-cost:    2
c ---[ 245]---> BDD-cost:    2
c ---[ 244]---> BDD-cost:    2
c ---[ 243]---> BDD-cost:    2
c ---[ 242]---> BDD-cost:    2
c ---[ 241]---> BDD-cost:    2
c ---[ 240]---> BDD-cost:    2
c ---[ 239]---> BDD-cost:    4
c ---[ 238]---> BDD-cost:    2
c ---[ 237]---> BDD-cost:    2
c ---[ 236]---> BDD-cost:    2
c ---[ 235]---> BDD-cost:    2
c ---[ 234]---> BDD-cost:    2
c ---[ 233]---> BDD-cost:    2
c ---[ 232]---> BDD-cost:    2
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    2
c ---[ 229]---> BDD-cost:    2
c ---[ 228]---> BDD-cost:    2
c ---[ 227]---> BDD-cost:    2
c ---[ 226]---> BDD-cost:    2
c ---[ 225]---> BDD-cost:    2
c ---[ 224]---> BDD-cost:    2
c ---[ 223]---> BDD-cost:    2
c ---[ 222]---> BDD-cost:    2
c ---[ 221]---> BDD-cost:    2
c ---[ 220]---> BDD-cost:    2
c ---[ 219]---> BDD-cost:    2
c ---[ 218]---> BDD-cost:    2
c ---[ 217]---> BDD-cost:    2
c ---[ 216]---> BDD-cost:    2
c ---[ 215]---> BDD-cost:    4
c ---[ 214]---> BDD-cost:    2
c ---[ 213]---> BDD-cost:    2
c ---[ 212]---> BDD-cost:    2
c ---[ 211]---> BDD-cost:    2
c ---[ 210]---> BDD-cost:    2
c ---[ 209]---> BDD-cost:    2
c ---[ 208]---> BDD-cost:    2
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    2
c ---[ 205]---> BDD-cost:    2
c ---[ 204]---> BDD-cost:    2
c ---[ 203]---> BDD-cost:    2
c ---[ 202]---> BDD-cost:    2
c ---[ 201]---> BDD-cost:    2
c ---[ 200]---> BDD-cost:    2
c ---[ 191]---> BDD-cost:    2
c ---[ 190]---> BDD-cost:    2
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 181]---> BDD-cost:    2
c ---[ 180]---> BDD-cost:    2
c ---[ 179]---> BDD-cost:    2
c ---[ 178]---> BDD-cost:    2
c ---[ 177]---> BDD-cost:    2
c ---[ 176]---> BDD-cost:    2
c ---[ 175]---> BDD-cost:    2
c ---[ 174]---> BDD-cost:    2
c ---[ 173]---> BDD-cost:    2
c ---[ 172]---> BDD-cost:    2
c ---[ 171]---> BDD-cost:    2
c ---[ 170]---> BDD-cost:    2
c ---[ 169]---> BDD-cost:    2
c ---[ 168]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 166]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 164]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 162]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    2
c ---[ 159]---> BDD-cost:    2
c ---[ 158]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    2
c ---[ 156]---> BDD-cost:    2
c ---[ 155]---> BDD-cost:    2
c ---[ 154]---> BDD-cost:    2
c ---[ 153]---> BDD-cost:    2
c ---[ 152]---> BDD-cost:    2
c ---[ 151]---> BDD-cost:    2
c ---[ 150]---> BDD-cost:    2
c ---[ 149]---> BDD-cost:    2
c ---[ 148]---> BDD-cost:    2
c ---[ 147]---> BDD-cost:    2
c ---[ 146]---> BDD-cost:    2
c ---[ 145]---> BDD-cost:    2
c ---[ 144]---> BDD-cost:    2
c ---[ 143]---> BDD-cost:    2
c ---[ 142]---> BDD-cost:    2
c ---[ 141]---> BDD-cost:    2
c ---[ 140]---> BDD-cost:    2
c ---[ 139]---> BDD-cost:    2
c ---[ 138]---> BDD-cost:    2
c ---[ 137]---> BDD-cost:    2
c ---[ 136]---> BDD-cost:    2
c ---[ 127]---> BDD-cost:    2
c ---[ 126]---> BDD-cost:    2
c ---[ 125]---> BDD-cost:    2
c ---[ 124]---> BDD-cost:    2
c ---[ 123]---> BDD-cost:    2
c ---[ 122]---> BDD-cost:    2
c ---[ 121]---> BDD-cost:    2
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 118]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 116]---> BDD-cost:    2
c ---[ 115]---> BDD-cost:    2
c ---[ 114]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 111]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 109]---> BDD-cost:    2
c ---[ 108]---> BDD-cost:    2
c ---[ 107]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 104]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[ 102]---> BDD-cost:    2
c ---[ 101]---> BDD-cost:    2
c ---[ 100]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  94]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  88]---> BDD-cost:    2
c ---[  87]---> BDD-cost:    2
c ---[  86]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  83]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  81]---> BDD-cost:    2
c ---[  80]---> BDD-cost:    2
c ---[  79]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  76]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  74]---> BDD-cost:    2
c ---[  73]---> BDD-cost:    2
c ---[  72]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  62]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  60]---> BDD-cost:    2
c ---[  59]---> BDD-cost:    2
c ---[  58]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  55]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  53]---> BDD-cost:    2
c ---[  52]---> BDD-cost:    2
c ---[  51]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  48]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  46]---> BDD-cost:    2
c ---[  45]---> BDD-cost:    2
c ---[  44]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  41]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  39]---> BDD-cost:    2
c ---[  38]---> BDD-cost:    2
c ---[  37]---> BDD-cost:    2
c ---[  36]---> BDD-cost:    2
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:    2
c ---[  33]---> BDD-cost:    2
c ---[  32]---> BDD-cost:    2
c ---[  31]---> BDD-cost:    2
c ---[  30]---> BDD-cost:    2
c ---[  29]---> BDD-cost:    2
c ---[  28]---> BDD-cost:    2
c ---[  27]---> BDD-cost:    2
c ---[  26]---> BDD-cost:    2
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost:    2
c ---[  23]---> BDD-cost:    2
c ---[  22]---> BDD-cost:    2
c ---[  21]---> BDD-cost:    2
c ---[  20]---> BDD-cost:    2
c ---[  19]---> BDD-cost:    2
c ---[  18]---> BDD-cost:    2
c ---[  17]---> BDD-cost:    2
c ---[  16]---> BDD-cost:    2
c ---[  15]---> BDD-cost:    2
c ---[  14]---> BDD-cost:    2
c ---[  13]---> BDD-cost:    2
c ---[  12]---> BDD-cost:    2
c ---[  11]---> BDD-cost:    2
c ---[  10]---> BDD-cost:    2
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17376    49254 |    5792       0        0     nan |  0.000 % |
c |       100 |   17376    49254 |    6371     100     1326    13.3 | 27.023 % |
c ==============================================================================
c [1mFound solution: 31956[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36248     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       147 |  112281   271036 |   37427     147     1914    13.0 | 27.023 % |
c ==============================================================================
c [1mFound solution: 31563[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       176 |  113591   274375 |   37863     176     2430    13.8 | 27.023 % |
c |       277 |  113591   274375 |   41649     277     5251    19.0 |  4.757 % |
c ==============================================================================
c [1mFound solution: 31343[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       382 |  113629   274546 |   37876     382     6306    16.5 |  4.757 % |
c ==============================================================================
c [1mFound solution: 31013[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       387 |  113644   274619 |   37881     387     6362    16.4 |  4.757 % |
c |       487 |  113644   274619 |   41669     487     9135    18.8 |  4.758 % |
c |       637 |  113596   274511 |   45836     635    10811    17.0 |  4.787 % |
c ==============================================================================
c [1mFound solution: 30586[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       675 |  113901   275318 |   37967     673    15256    22.7 |  4.787 % |
c ==============================================================================
c [1mFound solution: 28916[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       739 |  113929   275393 |   37976     737    16345    22.2 |  4.787 % |
c ==============================================================================
c [1mFound solution: 28339[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       811 |  114074   275750 |   38024     809    17738    21.9 |  4.787 % |
c ==============================================================================
c [1mFound solution: 28118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       869 |  114087   275872 |   38029     867    20760    23.9 |  4.787 % |
c |       969 |  114073   275840 |   41831     966    24217    25.1 |  4.772 % |
c |      1120 |  114073   275840 |   46015    1117    39019    34.9 |  4.772 % |
c |      1345 |  114073   275840 |   50616    1342    43692    32.6 |  4.772 % |
c |      1683 |  114073   275840 |   55678    1680    47677    28.4 |  4.772 % |
c |      2195 |  114073   275840 |   61246    2192    54895    25.0 |  4.772 % |
c |      2954 |  114073   275840 |   67370    2951   171086    58.0 |  4.772 % |
c ==============================================================================
c [1mFound solution: 27817[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3367 |  114212   276177 |   38070    3364   192128    57.1 |  4.772 % |
c |      3467 |  114212   276177 |   41877    3464   194840    56.2 |  4.765 % |
c |      3617 |  114212   276177 |   46064    3614   206716    57.2 |  4.765 % |
c |      3842 |  114212   276177 |   50671    3839   213401    55.6 |  4.765 % |
c |      4179 |  114212   276177 |   55738    4176   230255    55.1 |  4.765 % |
c |      4686 |  114212   276177 |   61312    4683   242856    51.9 |  4.765 % |
c |      5450 |  114212   276177 |   67443    5447   272764    50.1 |  4.765 % |
c |      6590 |  113989   275672 |   74187    6582   322347    49.0 |  4.915 % |
c |      8299 |  113989   275672 |   81606    8291   447067    53.9 |  4.915 % |
c |     10861 |  113758   275143 |   89767   10843   584131    53.9 |  5.066 % |
c ==============================================================================
c [1mFound solution: 27813[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14491 |  113191   273859 |   37730   14454   705837    48.8 |  5.066 % |
c |     14592 |  113118   273692 |   41503   14554   708940    48.7 |  5.499 % |
c |     14742 |  112774   272909 |   45653   14702   711851    48.4 |  5.717 % |
c |     14970 |  112774   272909 |   50218   14930   730505    48.9 |  5.717 % |
c |     15307 |  112774   272909 |   55240   15267   756401    49.5 |  5.717 % |
c |     15813 |  112774   272909 |   60764   15773   787871    50.0 |  5.717 % |
c ==============================================================================
c [1mFound solution: 27795[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16057 |  112800   272984 |   37600   16017   809097    50.5 |  5.717 % |
c |     16157 |  112800   272984 |   41360   16117   813107    50.5 |  5.717 % |
c ==============================================================================
c [1mFound solution: 27501[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16294 |  112808   273013 |   37602   16254   820930    50.5 |  5.717 % |
c |     16396 |  112808   273013 |   41362   16356   832545    50.9 |  5.718 % |
c |     16547 |  112744   272871 |   45498   16504   833734    50.5 |  5.764 % |
c |     16773 |  112580   272501 |   50048   16707   843676    50.5 |  5.876 % |
c |     17110 |  112580   272501 |   55053   17044   877938    51.5 |  5.876 % |
c |     17616 |  112580   272501 |   60558   17550   917907    52.3 |  5.876 % |
c |     18377 |  112580   272501 |   66614   18311   997681    54.5 |  5.876 % |
c |     19519 |  112545   272422 |   73275   19452  1030099    53.0 |  5.900 % |
c |     21228 |  112157   271542 |   80603   21144  1265877    59.9 |  6.151 % |
c |     23790 |  112109   271433 |   88663   23702  1325656    55.9 |  6.190 % |
c ==============================================================================
c [1mFound solution: 27457[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25312 |  112118   271454 |   37372   25224  1393087    55.2 |  6.190 % |
c |     25413 |  112118   271454 |   41109   25325  1396262    55.1 |  6.192 % |
c |     25565 |  112118   271454 |   45220   25477  1400766    55.0 |  6.192 % |
c |     25791 |  112118   271454 |   49742   25703  1417812    55.2 |  6.192 % |
c |     26128 |  112118   271454 |   54716   26040  1426891    54.8 |  6.192 % |
c |     26634 |  112118   271454 |   60187   26546  1439549    54.2 |  6.192 % |
c |     27393 |  112118   271454 |   66206   27305  1524061    55.8 |  6.192 % |
c |     28532 |  111938   271046 |   72827   28436  1620084    57.0 |  6.315 % |
c |     30240 |  111684   270463 |   80110   30142  1789816    59.4 |  6.499 % |
c |     32802 |  111684   270463 |   88121   32704  1914290    58.5 |  6.499 % |
c |     36646 |  111684   270463 |   96933   36548  2269361    62.1 |  6.499 % |
c ==============================================================================
c [1mFound solution: 27360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38116 |  111697   270494 |   37232   38018  2366385    62.2 |  6.499 % |
c |     38217 |  111697   270494 |   40955   38119  2377846    62.4 |  6.500 % |
c |     38368 |  111697   270494 |   45050   38270  2384323    62.3 |  6.500 % |
c |     38593 |  111697   270494 |   49555   38495  2405792    62.5 |  6.500 % |
c |     38930 |  111697   270494 |   54511   38832  2429420    62.6 |  6.500 % |
c |     39437 |  109953   266516 |   59962   39301  2436439    62.0 |  7.736 % |
c |     40196 |  109953   266516 |   65958   40060  2571897    64.2 |  7.736 % |
c |     41335 |  109953   266516 |   72554   41199  2708593    65.7 |  7.736 % |
c ==============================================================================
c [1mFound solution: 27257[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42092 |  109961   266535 |   36653   41956  2793630    66.6 |  7.736 % |
c |     42193 |  109961   266535 |   40318   16732  1033515    61.8 |  7.738 % |
c |     42344 |  109961   266535 |   44350   16883  1042761    61.8 |  7.738 % |
c |     42570 |  109961   266535 |   48785   17109  1058246    61.9 |  7.738 % |
c |     42908 |  109961   266535 |   53663   17447  1085007    62.2 |  7.738 % |
c |     43416 |  109961   266535 |   59030   17955  1140854    63.5 |  7.738 % |
c |     44175 |  109961   266535 |   64933   18714  1171895    62.6 |  7.738 % |
c |     45316 |  109961   266535 |   71426   19855  1219126    61.4 |  7.738 % |
c |     47027 |  108578   263358 |   78568   21347  1337574    62.7 |  8.749 % |
c |     49590 |  108578   263358 |   86425   23910  1804189    75.5 |  8.749 % |
c |     53436 |  107972   261973 |   95068   27732  2316612    83.5 |  9.198 % |
c |     59204 |  106915   259561 |  104575   33279  2706898    81.3 |  9.953 % |
c |     67855 |  104663   254383 |  115032   41755  3303359    79.1 | 11.578 % |
c ==============================================================================
c [1mFound solution: 27201[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72316 |  104667   254392 |   34889   46216  3745394    81.0 | 11.578 % |
c |     72417 |  104667   254392 |   38377   18616   964264    51.8 | 11.580 % |
c |     72567 |  104667   254392 |   42215   18766   968857    51.6 | 11.580 % |
c |     72792 |  104667   254392 |   46437   18991   976186    51.4 | 11.580 % |
c |     73130 |  104667   254392 |   51080   19329   987298    51.1 | 11.580 % |
c |     73637 |  104667   254392 |   56189   19836  1004080    50.6 | 11.580 % |
c |     74398 |  104667   254392 |   61807   20597  1062430    51.6 | 11.580 % |
c |     75537 |  104667   254392 |   67988   21736  1110020    51.1 | 11.580 % |
c |     77246 |  104667   254392 |   74787   23445  1156496    49.3 | 11.580 % |
c ==============================================================================
c [1mFound solution: 26793[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77295 |  104678   254423 |   34892   23494  1161038    49.4 | 11.580 % |
c |     77395 |  104414   253816 |   38381   23586  1162616    49.3 | 11.786 % |
c |     77545 |  104414   253816 |   42219   23736  1166062    49.1 | 11.786 % |
c |     77770 |  104414   253816 |   46441   23961  1184154    49.4 | 11.786 % |
c |     78109 |  104414   253816 |   51085   24300  1191266    49.0 | 11.786 % |
c |     78615 |  104414   253816 |   56193   24806  1203274    48.5 | 11.786 % |
c |     79374 |  104414   253816 |   61813   25565  1260624    49.3 | 11.786 % |
c |     80515 |  104414   253816 |   67994   26706  1379561    51.7 | 11.786 % |
c |     82225 |  104414   253816 |   74794   28416  1486335    52.3 | 11.786 % |
c |     84789 |  104303   253562 |   82273   30430  1604311    52.7 | 11.883 % |
c ==============================================================================
c [1mFound solution: 26443[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88501 |  104313   253585 |   34771   34142  1877163    55.0 | 11.883 % |
c |     88601 |  104313   253585 |   38248   34242  1881540    54.9 | 11.884 % |
c |     88752 |  104313   253585 |   42072   34393  1899019    55.2 | 11.884 % |
c |     88978 |  104313   253585 |   46280   34619  1915760    55.3 | 11.884 % |
c |     89315 |  104120   253139 |   50908   34918  1920410    55.0 | 12.031 % |
c |     89822 |  104076   253043 |   55999   35420  1977425    55.8 | 12.072 % |
c |     90582 |  104076   253043 |   61598   36180  2032359    56.2 | 12.072 % |
c |     91722 |  104076   253043 |   67758   37320  2142490    57.4 | 12.072 % |
c |     93432 |  104076   253043 |   74534   39030  2221665    56.9 | 12.072 % |
c |     95995 |  104076   253043 |   81988   41593  2714177    65.3 | 12.072 % |
c |     99840 |  103852   252527 |   90187   45433  2925008    64.4 | 12.234 % |
c |    105606 |  102236   248798 |   99205   51130  3306514    64.7 | 13.455 % |
c |    114257 |  101251   246513 |  109126   59672  3654481    61.2 | 14.215 % |
c ==============================================================================
c [1mFound solution: 26442[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122777 |  101262   246540 |   33754   68192  4590117    67.3 | 14.215 % |
c |    122877 |  101262   246540 |   37129   22956  1167913    50.9 | 14.215 % |
c |    123027 |  101262   246540 |   40842   23106  1175108    50.9 | 14.215 % |
c |    123253 |  101262   246540 |   44926   23332  1184804    50.8 | 14.215 % |
c |    123590 |  101262   246540 |   49419   23669  1207074    51.0 | 14.215 % |
c |    124096 |  101262   246540 |   54361   24175  1259017    52.1 | 14.215 % |
c |    124859 |  101262   246540 |   59797   24938  1364639    54.7 | 14.215 % |
c |    126000 |  101262   246540 |   65776   26079  1414687    54.2 | 14.215 % |
c |    127708 |  101262   246540 |   72354   27787  1547195    55.7 | 14.215 % |
c |    130270 |  101262   246540 |   79590   30349  1854960    61.1 | 14.215 % |
c |    134116 |  100870   245638 |   87549   34177  2194864    64.2 | 14.495 % |
c |    139883 |  100870   245638 |   96304   39944  2475013    62.0 | 14.495 % |
c |    148532 |  100870   245638 |  105934   48593  3332642    68.6 | 14.495 % |
c |    161506 |  100870   245638 |  116527   61567  4104866    66.7 | 14.495 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.92 0.89 2/54 2828
Raw data (stat): 2828 (runsolver) R 2827 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481022829 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99992 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 3908 0 0 0 987 11 0 0 25 0 1 0 481022829 18903040 3739 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4615 3739 603 41 0 4574 0
vsize: 18460
[startup+20.0012 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4049 0 0 0 1986 12 0 0 25 0 1 0 481022829 19550208 3880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 3880 603 41 0 4732 0
vsize: 19092
[startup+30.0019 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4159 0 0 0 2985 12 0 0 25 0 1 0 481022829 19922944 3990 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4864 3990 603 41 0 4823 0
vsize: 19456
[startup+40.002 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4294 0 0 0 3984 12 0 0 25 0 1 0 481022829 20451328 4125 4294967295 134512640 134672761 3221224560 3221223696 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4993 4125 603 41 0 4952 0
vsize: 19972
[startup+50.0029 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4399 0 0 0 4984 13 0 0 25 0 1 0 481022829 20983808 4230 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5123 4230 603 41 0 5082 0
vsize: 20492
[startup+60.0026 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4548 0 0 0 5983 13 0 0 25 0 1 0 481022829 21606400 4379 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5275 4379 603 41 0 5234 0
vsize: 21100
[startup+70.0031 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4678 0 0 0 6983 14 0 0 25 0 1 0 481022829 22138880 4509 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5405 4509 603 41 0 5364 0
vsize: 21620
[startup+80.0031 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4791 0 0 0 7983 14 0 0 25 0 1 0 481022829 22536192 4622 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5502 4622 603 41 0 5461 0
vsize: 22008
[startup+90.0037 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 4897 0 0 0 8983 14 0 0 25 0 1 0 481022829 23097344 4728 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5639 4728 603 41 0 5598 0
vsize: 22556
[startup+100.003 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5015 0 0 0 9983 15 0 0 25 0 1 0 481022829 23490560 4846 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5735 4846 603 41 0 5694 0
vsize: 22940
[startup+110.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5249 0 0 0 10982 16 0 0 25 0 1 0 481022829 24555520 5080 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5995 5080 603 41 0 5954 0
vsize: 23980
[startup+120.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5374 0 0 0 11982 16 0 0 25 0 1 0 481022829 24956928 5205 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6093 5205 603 41 0 6052 0
vsize: 24372
[startup+130.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5478 0 0 0 12981 16 0 0 25 0 1 0 481022829 25358336 5309 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6191 5309 603 41 0 6150 0
vsize: 24764
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5582 0 0 0 13981 17 0 0 25 0 1 0 481022829 25886720 5413 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6320 5413 603 41 0 6279 0
vsize: 25280
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5690 0 0 0 14980 18 0 0 25 0 1 0 481022829 26275840 5521 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5521 603 41 0 6374 0
vsize: 25660
[startup+160.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5805 0 0 0 15980 18 0 0 25 0 1 0 481022829 26791936 5636 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6541 5636 603 41 0 6500 0
vsize: 26164
[startup+170.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5906 0 0 0 16980 18 0 0 25 0 1 0 481022829 27193344 5737 4294967295 134512640 134672761 3221224560 3221223744 134558324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 5737 603 41 0 6598 0
vsize: 26556
[startup+180.004 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 5986 0 0 0 17979 19 0 0 25 0 1 0 481022829 27455488 5817 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6703 5817 603 41 0 6662 0
vsize: 26812
[startup+190.005 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6091 0 0 0 18979 19 0 0 25 0 1 0 481022829 27987968 5922 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6833 5922 603 41 0 6792 0
vsize: 27332
[startup+200.005 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6181 0 0 0 19979 19 0 0 25 0 1 0 481022829 28393472 6012 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6932 6012 603 41 0 6891 0
vsize: 27728
[startup+210.005 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6305 0 0 0 20979 20 0 0 25 0 1 0 481022829 28925952 6136 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6136 603 41 0 7021 0
vsize: 28248
[startup+220.006 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6445 0 0 0 21978 20 0 0 25 0 1 0 481022829 29446144 6276 4294967295 134512640 134672761 3221224560 3221223744 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7189 6276 603 41 0 7148 0
vsize: 28756
[startup+230.006 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6525 0 0 0 22978 21 0 0 25 0 1 0 481022829 29843456 6356 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7286 6356 603 41 0 7245 0
vsize: 29144
[startup+240.006 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6640 0 0 0 23978 21 0 0 25 0 1 0 481022829 30220288 6471 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7378 6471 603 41 0 7337 0
vsize: 29512
[startup+250.007 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6758 0 0 0 24978 21 0 0 25 0 1 0 481022829 30736384 6589 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7504 6589 603 41 0 7463 0
vsize: 30016
[startup+260.007 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6900 0 0 0 25977 22 0 0 25 0 1 0 481022829 31252480 6731 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7630 6731 603 41 0 7589 0
vsize: 30520
[startup+270.011 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 6987 0 0 0 26977 23 0 0 25 0 1 0 481022829 31645696 6818 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7726 6818 603 41 0 7685 0
vsize: 30904
[startup+280.011 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 27977 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+290.029 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 28979 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+300.03 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 29979 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+310.029 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 30979 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+320.13 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 31989 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+330.131 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 32989 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+340.131 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 33990 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+350.131 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 34990 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+360.131 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 35990 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+370.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 36990 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+380.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 37990 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+390.132 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7027 0 0 0 38991 23 0 0 25 0 1 0 481022829 31772672 6858 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7757 6858 603 41 0 7716 0
vsize: 31028
[startup+400.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7120 0 0 0 39991 23 0 0 25 0 1 0 481022829 32165888 6951 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 6951 603 41 0 7812 0
vsize: 31412
[startup+410.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7254 0 0 0 40990 23 0 0 25 0 1 0 481022829 32702464 7085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7085 603 41 0 7943 0
vsize: 31936
[startup+420.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7334 0 0 0 41990 24 0 0 25 0 1 0 481022829 33091584 7165 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8079 7165 603 41 0 8038 0
vsize: 32316
[startup+430.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7424 0 0 0 42990 24 0 0 25 0 1 0 481022829 33480704 7255 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8174 7255 603 41 0 8133 0
vsize: 32696
[startup+440.132 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7521 0 0 0 43990 24 0 0 25 0 1 0 481022829 33882112 7352 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8272 7352 603 41 0 8231 0
vsize: 33088
[startup+450.132 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7609 0 0 0 44989 25 0 0 25 0 1 0 481022829 34144256 7440 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8336 7440 603 41 0 8295 0
vsize: 33344
[startup+460.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7712 0 0 0 45989 25 0 0 25 0 1 0 481022829 34668544 7543 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8464 7543 603 41 0 8423 0
vsize: 33856
[startup+470.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7810 0 0 0 46989 26 0 0 25 0 1 0 481022829 35061760 7641 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 7641 603 41 0 8519 0
vsize: 34240
[startup+480.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 7903 0 0 0 47988 27 0 0 25 0 1 0 481022829 35450880 7734 4294967295 134512640 134672761 3221224560 3221223744 134558638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8655 7734 603 41 0 8614 0
vsize: 34620
[startup+490.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8000 0 0 0 48988 27 0 0 25 0 1 0 481022829 35840000 7831 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8750 7831 603 41 0 8709 0
vsize: 35000
[startup+500.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 49988 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+510.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 50988 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+520.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 51988 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+530.131 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 52989 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+540.132 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 53989 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+550.133 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 54989 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+560.133 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 55989 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+570.133 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 56989 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+580.133 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 57989 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+590.134 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 58990 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+600.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 59990 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+610.134 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 60990 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+620.134 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 61990 27 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+630.134 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 62990 28 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223664 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+640.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 63990 28 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+650.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 64991 28 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+660.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 65991 28 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+670.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8055 0 0 0 66991 28 0 0 25 0 1 0 481022829 35966976 7886 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8781 7886 603 41 0 8740 0
vsize: 35124
[startup+680.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8057 0 0 0 67990 28 0 0 25 0 1 0 481022829 35966976 7888 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7888 603 41 0 8740 0
vsize: 35124
[startup+690.136 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8058 0 0 0 68991 28 0 0 25 0 1 0 481022829 35966976 7889 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7889 603 41 0 8740 0
vsize: 35124
[startup+700.136 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8059 0 0 0 69991 28 0 0 25 0 1 0 481022829 35966976 7890 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7890 603 41 0 8740 0
vsize: 35124
[startup+710.136 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8062 0 0 0 70991 28 0 0 25 0 1 0 481022829 35966976 7893 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7893 603 41 0 8740 0
vsize: 35124
[startup+720.137 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8064 0 0 0 71991 28 0 0 25 0 1 0 481022829 35966976 7895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7895 603 41 0 8740 0
vsize: 35124
[startup+730.137 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8065 0 0 0 72991 28 0 0 25 0 1 0 481022829 35966976 7896 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8781 7896 603 41 0 8740 0
vsize: 35124
[startup+740.138 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8080 0 0 0 73991 28 0 0 25 0 1 0 481022829 36098048 7911 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8813 7911 603 41 0 8772 0
vsize: 35252
[startup+750.138 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8194 0 0 0 74991 28 0 0 25 0 1 0 481022829 36487168 8025 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8908 8025 603 41 0 8867 0
vsize: 35632
[startup+760.137 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8310 0 0 0 75991 29 0 0 25 0 1 0 481022829 37015552 8141 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9037 8141 603 41 0 8996 0
vsize: 36148
[startup+770.138 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8395 0 0 0 76992 29 0 0 25 0 1 0 481022829 37404672 8226 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9132 8226 603 41 0 9091 0
vsize: 36528
[startup+780.138 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8498 0 0 0 77992 29 0 0 25 0 1 0 481022829 37801984 8329 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9229 8329 603 41 0 9188 0
vsize: 36916
[startup+790.138 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8601 0 0 0 78992 29 0 0 25 0 1 0 481022829 38195200 8432 4294967295 134512640 134672761 3221224560 3221223696 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9325 8432 603 41 0 9284 0
vsize: 37300
[startup+800.138 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8708 0 0 0 79992 29 0 0 25 0 1 0 481022829 38584320 8539 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9420 8539 603 41 0 9379 0
vsize: 37680
[startup+810.138 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8801 0 0 0 80992 29 0 0 25 0 1 0 481022829 39243776 8632 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9581 8632 603 41 0 9540 0
vsize: 38324
[startup+820.139 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 8909 0 0 0 81992 30 0 0 25 0 1 0 481022829 39632896 8740 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9676 8740 603 41 0 9635 0
vsize: 38704
[startup+830.139 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9025 0 0 0 82991 30 0 0 25 0 1 0 481022829 40165376 8856 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9806 8856 603 41 0 9765 0
vsize: 39224
[startup+840.139 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 83992 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+850.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 84992 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+860.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 85992 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+870.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 86992 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223744 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+880.141 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 87992 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+890.142 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 88992 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+900.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 89992 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+910.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 90993 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+920.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 91993 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223664 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+930.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 92993 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+940.143 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 93993 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+950.144 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 94993 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+960.144 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 95994 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+970.144 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 96994 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+980.144 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 97994 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+990.145 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 98994 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1000.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 99994 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1010.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 100994 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1020.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 101995 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1030.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 102995 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1040.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 103995 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1050.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 104995 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1060.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 105995 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1070.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 106996 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223696 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1080.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 107996 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1090.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 108996 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1100.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 109996 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1110.14 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 110996 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1120.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 111996 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1130.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 112997 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1140.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 113997 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1150.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 114997 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1160.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 115997 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1170.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 116997 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1180.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 117997 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1190.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 118998 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2828
Raw data (stat): 2828 (minisat+) R 2827 28546 28545 0 -1 0 9114 0 0 0 119998 30 0 0 25 0 1 0 481022829 40562688 8945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9903 8945 603 41 0 9862 0
vsize: 39612
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 2828
Raw data (stat): 2828 (minisat+) Z 2827 28546 28545 0 -1 12 9117 0 0 0 119998 32 0 0 25 0 1 0 481022829 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.17
CPU time (s): 1200.31
CPU user time (s): 1199.99
CPU system time (s): 0.32495
CPU usage (%): 100.012
Max. virtual memory (Kb): 39612
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####