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-circ6_3.opb
MD5SUM	509cfdb6810b13d9963718243e9046cd
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	66
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	3
Number of bits for the biggest coefficient in the objective function	2
Sum of the numbers in the objective function	324
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	16
Number of bits of the biggest number in a constraint	5
Biggest sum of numbers in a constraint	324
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.98
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 5007

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-13 21:14:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2318 boxname=wulflinc22 idbench=258 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  509cfdb6810b13d9963718243e9046cd  /oldhome/oroussel/tmp/wulflinc22/normalized-circ6_3.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc22/normalized-circ6_3.opb
IDLAUNCH: 2318
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        869724 kB
Buffers:         31040 kB
Cached:          90904 kB
SwapCached:        524 kB
Active:          42864 kB
Inactive:        82516 kB
HighTotal:      131008 kB
HighFree:        36316 kB
LowTotal:       903652 kB
LowFree:        833408 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34068 kB
Committed_AS:    63496 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:34:11 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 2318 7 1200.09 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: 94[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6902     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       147 |   29604    77814 |    9868     147     1914    13.0 | 27.023 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       157 |   29628    77882 |    9876     157     2045    13.0 | 27.023 % |
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       169 |   29677    78014 |    9892     169     2330    13.8 | 27.023 % |
c |       270 |   29677    78014 |   10881     270     4011    14.9 | 15.098 % |
c |       423 |   29677    78014 |   11969     423     9371    22.2 | 15.098 % |
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       576 |   29684    78035 |    9894     576    13827    24.0 | 15.098 % |
c |       677 |   29684    78035 |   10883     677    16356    24.2 | 15.100 % |
c |       829 |   29684    78035 |   11971     829    21008    25.3 | 15.100 % |
c |      1054 |   29684    78035 |   13168    1054    26665    25.3 | 15.100 % |
c ==============================================================================
c [1mFound solution: 78[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1130 |   29709    78108 |    9903    1130    30644    27.1 | 15.100 % |
c |      1230 |   29709    78108 |   10893    1230    34165    27.8 | 15.089 % |
c |      1380 |   29709    78108 |   11982    1380    39560    28.7 | 15.089 % |
c |      1610 |   29709    78108 |   13180    1610    53619    33.3 | 15.089 % |
c |      1948 |   29709    78108 |   14498    1948    70042    36.0 | 15.089 % |
c |      2454 |   29703    78096 |   15948    2441    81731    33.5 | 15.112 % |
c |      3213 |   29703    78096 |   17543    3200    96302    30.1 | 15.112 % |
c ==============================================================================
c [1mFound solution: 74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3319 |   29726    78161 |    9908    3306   101093    30.6 | 15.112 % |
c |      3419 |   29726    78161 |   10898    3406   105458    31.0 | 15.103 % |
c |      3569 |   29702    78107 |   11988    3555   109222    30.7 | 15.150 % |
c |      3795 |   29702    78107 |   13187    3781   115717    30.6 | 15.150 % |
c |      4134 |   29702    78107 |   14506    4120   124587    30.2 | 15.150 % |
c |      4640 |   29702    78107 |   15956    4626   142719    30.9 | 15.150 % |
c |      5399 |   29702    78107 |   17552    5385   176892    32.8 | 15.150 % |
c |      6539 |   29603    77884 |   19307    6523   202835    31.1 | 15.358 % |
c |      8248 |   29546    77759 |   21238    8222   256204    31.2 | 15.529 % |
c |     10811 |   27933    74071 |   23362   10677   388077    36.3 | 19.442 % |
c |     14656 |   27874    73936 |   25698   14519   560199    38.6 | 19.573 % |
c |     20424 |   27848    73876 |   28268   20284   788884    38.9 | 19.635 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21162 |   27855    73896 |    9285   21022   819277    39.0 | 19.635 % |
c |     21262 |   27855    73896 |   10213   10611   389067    36.7 | 19.635 % |
c |     21412 |   27855    73896 |   11234   10761   396679    36.9 | 19.635 % |
c |     21639 |   27855    73896 |   12358   10988   408948    37.2 | 19.635 % |
c |     21976 |   27786    73736 |   13594   11323   418755    37.0 | 19.813 % |
c |     22483 |   27786    73736 |   14953   11830   453904    38.4 | 19.813 % |
c |     23242 |   27766    73692 |   16448   12586   473453    37.6 | 19.906 % |
c |     24381 |   27766    73692 |   18093   13725   512538    37.3 | 19.906 % |
c |     26090 |   27756    73669 |   19903   15433   581999    37.7 | 19.929 % |
c |     28652 |   27707    73556 |   21893   17993   695501    38.7 | 20.053 % |
c |     32496 |   27552    73200 |   24082   21832   896279    41.1 | 20.431 % |
c |     38262 |   27552    73200 |   26491   27598  1259978    45.7 | 20.431 % |
c |     46912 |   27412    72876 |   29140   19364   974947    50.3 | 20.787 % |
c |     59886 |   27412    72876 |   32054   32338  1785931    55.2 | 20.787 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65047 |   27423    72911 |    9141   17519   828729    47.3 | 20.787 % |
c |     65147 |   27423    72911 |   10055    8860   301591    34.0 | 20.801 % |
c |     65297 |   27423    72911 |   11060    9010   305857    33.9 | 20.801 % |
c |     65524 |   27423    72911 |   12166    9237   319309    34.6 | 20.801 % |
c |     65861 |   27423    72911 |   13383    9574   335917    35.1 | 20.801 % |
c |     66368 |   27423    72911 |   14721   10081   362857    36.0 | 20.801 % |
c |     67130 |   27423    72911 |   16193   10843   393041    36.2 | 20.801 % |
c |     68269 |   27423    72911 |   17813   11982   450874    37.6 | 20.801 % |
c |     69978 |   27357    72760 |   19594   13685   533347    39.0 | 20.964 % |
c |     72540 |   27357    72760 |   21553   16247   636161    39.2 | 20.964 % |
c |     76384 |   27357    72760 |   23709   20091   857300    42.7 | 20.964 % |
c |     82151 |   27357    72760 |   26080   25858  1155049    44.7 | 20.964 % |
c |     90800 |   27249    72512 |   28688   19546   781130    40.0 | 21.226 % |
c |    103776 |   27243    72498 |   31557   32519  1333812    41.0 | 21.242 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103949 |   27250    72518 |    9083   32692  1345412    41.2 | 21.242 % |
c |    104052 |   27250    72518 |    9991    7696   234267    30.4 | 21.241 % |
c |    104202 |   27250    72518 |   10990    7846   238074    30.3 | 21.241 % |
c |    104427 |   27250    72518 |   12089    8071   250546    31.0 | 21.241 % |
c |    104764 |   27250    72518 |   13298    8408   265635    31.6 | 21.241 % |
c |    105270 |   27250    72518 |   14628    8914   292442    32.8 | 21.241 % |
c |    106029 |   27250    72518 |   16091    9673   340647    35.2 | 21.241 % |
c |    107168 |   27250    72518 |   17700   10812   379234    35.1 | 21.241 % |
c |    108876 |   27250    72518 |   19470   12520   427544    34.1 | 21.241 % |
c |    111439 |   27250    72518 |   21417   15083   551813    36.6 | 21.241 % |
c |    115283 |   27233    72481 |   23558   18926   729280    38.5 | 21.280 % |
c |    121049 |   27233    72481 |   25914   24692  1052161    42.6 | 21.280 % |
c |    129698 |   27233    72481 |   28506   18533   827239    44.6 | 21.280 % |
c |    142673 |   27233    72481 |   31356   31508  1631394    51.8 | 21.280 % |
c |    162136 |   27233    72481 |   34492   31357  1740207    55.5 | 21.280 % |
c |    191329 |   27227    72467 |   37941   37878  1391427    36.7 | 21.295 % |
c |    235118 |   27227    72467 |   41736   28909  1189205    41.1 | 21.295 % |
c |    300803 |   27227    72467 |   45909   36618  1226309    33.5 | 21.295 % |
c |    399332 |   27177    72351 |   50500   34237  2759073    80.6 | 21.426 % |
c |    547123 |   27171    72337 |   55550   29585  1217686    41.2 | 21.442 % |
#### 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.91 0.95 0.91 2/54 28841
Raw data (stat): 28841 (runsolver) R 28840 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479104515 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 1648 0 0 0 984 3 0 0 25 0 1 0 479104515 8626176 1626 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1626 603 41 0 2065 0
vsize: 8424
[startup+20.0013 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 2070 0 0 0 1983 4 0 0 25 0 1 0 479104515 10371072 2048 4294967295 134512640 134672761 3221224640 3221223744 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2532 2048 603 41 0 2491 0
vsize: 10128
[startup+30.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 2369 0 0 0 2982 5 0 0 25 0 1 0 479104515 11571200 2347 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2825 2347 603 41 0 2784 0
vsize: 11300
[startup+40.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 2369 0 0 0 3982 5 0 0 25 0 1 0 479104515 11571200 2347 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2347 603 41 0 2784 0
vsize: 11300
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 2496 0 0 0 4982 5 0 0 25 0 1 0 479104515 12107776 2474 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2956 2474 603 41 0 2915 0
vsize: 11824
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 2761 0 0 0 5981 6 0 0 25 0 1 0 479104515 13168640 2739 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3215 2739 603 41 0 3174 0
vsize: 12860
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3004 0 0 0 6979 8 0 0 25 0 1 0 479104515 14233600 2982 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 2982 603 41 0 3434 0
vsize: 13900
[startup+80.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3102 0 0 0 7979 8 0 0 25 0 1 0 479104515 14630912 3080 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3080 603 41 0 3531 0
vsize: 14288
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3102 0 0 0 8979 8 0 0 25 0 1 0 479104515 14630912 3080 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3080 603 41 0 3531 0
vsize: 14288
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3102 0 0 0 9979 8 0 0 25 0 1 0 479104515 14630912 3080 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3080 603 41 0 3531 0
vsize: 14288
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3314 0 0 0 10979 9 0 0 25 0 1 0 479104515 15425536 3292 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3766 3292 603 41 0 3725 0
vsize: 15064
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3577 0 0 0 11978 10 0 0 25 0 1 0 479104515 16621568 3555 4294967295 134512640 134672761 3221224640 3221223800 134561240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4058 3555 603 41 0 4017 0
vsize: 16232
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 12978 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 13978 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 14978 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 15978 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 16978 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 17979 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 18979 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 19979 10 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 20979 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223784 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 21979 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223776 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 22979 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 23979 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 24980 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 25980 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 26980 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223824 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 27980 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 28981 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3659 0 0 0 29981 11 0 0 25 0 1 0 479104515 17014784 3637 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4154 3637 603 41 0 4113 0
vsize: 16616
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3752 0 0 0 30981 11 0 0 25 0 1 0 479104515 17416192 3730 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4252 3730 603 41 0 4211 0
vsize: 17008
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3752 0 0 0 31981 11 0 0 25 0 1 0 479104515 17416192 3730 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4252 3730 603 41 0 4211 0
vsize: 17008
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3752 0 0 0 32981 11 0 0 25 0 1 0 479104515 17416192 3730 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4252 3730 603 41 0 4211 0
vsize: 17008
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3754 0 0 0 33981 11 0 0 25 0 1 0 479104515 17416192 3732 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4252 3732 603 41 0 4211 0
vsize: 17008
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 3911 0 0 0 34980 12 0 0 25 0 1 0 479104515 17948672 3889 4294967295 134512640 134672761 3221224640 3221223776 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4382 3889 603 41 0 4341 0
vsize: 17528
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4008 0 0 0 35980 12 0 0 25 0 1 0 479104515 18341888 3986 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4478 3986 603 41 0 4437 0
vsize: 17912
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4020 0 0 0 36981 12 0 0 25 0 1 0 479104515 18481152 3998 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4512 3998 603 41 0 4471 0
vsize: 18048
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4042 0 0 0 37981 12 0 0 25 0 1 0 479104515 18644992 4020 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4020 603 41 0 4511 0
vsize: 18208
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4068 0 0 0 38981 12 0 0 25 0 1 0 479104515 18644992 4046 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4046 603 41 0 4511 0
vsize: 18208
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4069 0 0 0 39981 12 0 0 25 0 1 0 479104515 18644992 4047 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4047 603 41 0 4511 0
vsize: 18208
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4069 0 0 0 40981 12 0 0 25 0 1 0 479104515 18644992 4047 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4047 603 41 0 4511 0
vsize: 18208
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4069 0 0 0 41981 12 0 0 25 0 1 0 479104515 18644992 4047 4294967295 134512640 134672761 3221224640 3221223776 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4047 603 41 0 4511 0
vsize: 18208
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4069 0 0 0 42982 12 0 0 25 0 1 0 479104515 18644992 4047 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4047 603 41 0 4511 0
vsize: 18208
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4069 0 0 0 43982 12 0 0 25 0 1 0 479104515 18644992 4047 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4047 603 41 0 4511 0
vsize: 18208
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4231 0 0 0 44981 13 0 0 25 0 1 0 479104515 19308544 4209 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4209 603 41 0 4673 0
vsize: 18856
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4352 0 0 0 45982 13 0 0 25 0 1 0 479104515 19845120 4330 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 4330 603 41 0 4804 0
vsize: 19380
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4372 0 0 0 46982 13 0 0 25 0 1 0 479104515 19980288 4350 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4878 4350 603 41 0 4837 0
vsize: 19512
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4407 0 0 0 47982 13 0 0 25 0 1 0 479104515 20127744 4385 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4914 4385 603 41 0 4873 0
vsize: 19656
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4415 0 0 0 48982 13 0 0 25 0 1 0 479104515 20127744 4393 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4914 4393 603 41 0 4873 0
vsize: 19656
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4433 0 0 0 49982 13 0 0 25 0 1 0 479104515 20275200 4411 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4950 4411 603 41 0 4909 0
vsize: 19800
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4444 0 0 0 50982 13 0 0 25 0 1 0 479104515 20275200 4422 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4950 4422 603 41 0 4909 0
vsize: 19800
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4445 0 0 0 51982 13 0 0 25 0 1 0 479104515 20275200 4423 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4950 4423 603 41 0 4909 0
vsize: 19800
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4447 0 0 0 52982 13 0 0 25 0 1 0 479104515 20275200 4425 4294967295 134512640 134672761 3221224640 3221223808 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4950 4425 603 41 0 4909 0
vsize: 19800
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4472 0 0 0 53982 13 0 0 25 0 1 0 479104515 20439040 4450 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4450 603 41 0 4949 0
vsize: 19960
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4501 0 0 0 54983 14 0 0 25 0 1 0 479104515 20439040 4479 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4990 4479 603 41 0 4949 0
vsize: 19960
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4504 0 0 0 55983 14 0 0 25 0 1 0 479104515 20635648 4482 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4482 603 41 0 4997 0
vsize: 20152
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4510 0 0 0 56983 14 0 0 25 0 1 0 479104515 20635648 4488 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4488 603 41 0 4997 0
vsize: 20152
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4520 0 0 0 57983 14 0 0 25 0 1 0 479104515 20635648 4498 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4498 603 41 0 4997 0
vsize: 20152
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4525 0 0 0 58983 14 0 0 25 0 1 0 479104515 20635648 4503 4294967295 134512640 134672761 3221224640 3221223824 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4503 603 41 0 4997 0
vsize: 20152
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4537 0 0 0 59983 14 0 0 25 0 1 0 479104515 20799488 4515 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4515 603 41 0 5037 0
vsize: 20312
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4544 0 0 0 60983 14 0 0 25 0 1 0 479104515 20799488 4522 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4522 603 41 0 5037 0
vsize: 20312
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4544 0 0 0 61983 14 0 0 25 0 1 0 479104515 20799488 4522 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4522 603 41 0 5037 0
vsize: 20312
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4544 0 0 0 62984 14 0 0 25 0 1 0 479104515 20799488 4522 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4522 603 41 0 5037 0
vsize: 20312
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4550 0 0 0 63984 14 0 0 25 0 1 0 479104515 20799488 4528 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4528 603 41 0 5037 0
vsize: 20312
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4550 0 0 0 64984 14 0 0 25 0 1 0 479104515 20799488 4528 4294967295 134512640 134672761 3221224640 3221223744 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4528 603 41 0 5037 0
vsize: 20312
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4555 0 0 0 65984 14 0 0 25 0 1 0 479104515 20799488 4533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4533 603 41 0 5037 0
vsize: 20312
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4555 0 0 0 66984 14 0 0 25 0 1 0 479104515 20799488 4533 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4533 603 41 0 5037 0
vsize: 20312
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4605 0 0 0 67984 14 0 0 25 0 1 0 479104515 21061632 4583 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4583 603 41 0 5101 0
vsize: 20568
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4615 0 0 0 68985 14 0 0 25 0 1 0 479104515 21061632 4593 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4593 603 41 0 5101 0
vsize: 20568
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4627 0 0 0 69985 14 0 0 25 0 1 0 479104515 21061632 4605 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4605 603 41 0 5101 0
vsize: 20568
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4629 0 0 0 70985 14 0 0 25 0 1 0 479104515 21061632 4607 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4607 603 41 0 5101 0
vsize: 20568
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4641 0 0 0 71985 14 0 0 25 0 1 0 479104515 21225472 4619 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5182 4619 603 41 0 5141 0
vsize: 20728
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4641 0 0 0 72985 14 0 0 25 0 1 0 479104515 21225472 4619 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5182 4619 603 41 0 5141 0
vsize: 20728
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4850 0 0 0 73985 15 0 0 25 0 1 0 479104515 22028288 4828 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5378 4828 603 41 0 5337 0
vsize: 21512
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4994 0 0 0 74985 15 0 0 25 0 1 0 479104515 22568960 4972 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5510 4972 603 41 0 5469 0
vsize: 22040
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4999 0 0 0 75985 15 0 0 25 0 1 0 479104515 22728704 4977 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 4977 603 41 0 5508 0
vsize: 22196
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 4999 0 0 0 76985 15 0 0 25 0 1 0 479104515 22728704 4977 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 4977 603 41 0 5508 0
vsize: 22196
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 5018 0 0 0 77985 15 0 0 25 0 1 0 479104515 22728704 4996 4294967295 134512640 134672761 3221224640 3221223824 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 4996 603 41 0 5508 0
vsize: 22196
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 5089 0 0 0 78985 15 0 0 25 0 1 0 479104515 22994944 5067 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5614 5067 603 41 0 5573 0
vsize: 22456
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 5352 0 0 0 79984 17 0 0 25 0 1 0 479104515 24199168 5330 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5908 5330 603 41 0 5867 0
vsize: 23632
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 5610 0 0 0 80984 17 0 0 25 0 1 0 479104515 25264128 5588 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6168 5588 603 41 0 6127 0
vsize: 24672
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 5844 0 0 0 81982 19 0 0 25 0 1 0 479104515 26202112 5822 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6397 5822 603 41 0 6356 0
vsize: 25588
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 6069 0 0 0 82980 20 0 0 25 0 1 0 479104515 27144192 6047 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6627 6047 603 41 0 6586 0
vsize: 26508
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 6291 0 0 0 83980 20 0 0 25 0 1 0 479104515 27942912 6269 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6822 6269 603 41 0 6781 0
vsize: 27288
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 6521 0 0 0 84980 21 0 0 25 0 1 0 479104515 28880896 6499 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7051 6499 603 41 0 7010 0
vsize: 28204
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 6732 0 0 0 85979 22 0 0 25 0 1 0 479104515 29822976 6710 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7281 6710 603 41 0 7240 0
vsize: 29124
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 6931 0 0 0 86979 22 0 0 25 0 1 0 479104515 30629888 6909 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7478 6909 603 41 0 7437 0
vsize: 29912
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7155 0 0 0 87978 23 0 0 25 0 1 0 479104515 31567872 7133 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7707 7133 603 41 0 7666 0
vsize: 30828
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 88978 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+900.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 89978 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 90979 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 91979 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 92979 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 93979 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 94979 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 95979 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 96980 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 97980 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 98980 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 99980 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 100980 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 101981 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 102981 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 103981 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223744 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 104981 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 105981 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 106982 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223744 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 107982 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 108982 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 109982 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 110982 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7275 0 0 0 111983 23 0 0 25 0 1 0 479104515 31965184 7253 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7804 7253 603 41 0 7763 0
vsize: 31216
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7286 0 0 0 112983 23 0 0 25 0 1 0 479104515 32124928 7264 4294967295 134512640 134672761 3221224640 3221223824 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7264 603 41 0 7802 0
vsize: 31372
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7296 0 0 0 113983 23 0 0 25 0 1 0 479104515 32124928 7274 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7274 603 41 0 7802 0
vsize: 31372
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7296 0 0 0 114983 23 0 0 25 0 1 0 479104515 32124928 7274 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7274 603 41 0 7802 0
vsize: 31372
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7296 0 0 0 115984 23 0 0 25 0 1 0 479104515 32124928 7274 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7274 603 41 0 7802 0
vsize: 31372
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7296 0 0 0 116984 23 0 0 25 0 1 0 479104515 32124928 7274 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7274 603 41 0 7802 0
vsize: 31372
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7296 0 0 0 117984 23 0 0 25 0 1 0 479104515 32124928 7274 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7274 603 41 0 7802 0
vsize: 31372
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7296 0 0 0 118983 23 0 0 25 0 1 0 479104515 32124928 7274 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7274 603 41 0 7802 0
vsize: 31372
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28841
Raw data (stat): 28841 (minisat+) R 28840 26298 26297 0 -1 0 7296 0 0 0 119983 23 0 0 25 0 1 0 479104515 32124928 7274 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7843 7274 603 41 0 7802 0
vsize: 31372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28841
Raw data (stat): 28841 (minisat+) Z 28840 26298 26297 0 -1 12 7299 0 0 0 119983 25 0 0 25 0 1 0 479104515 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.04
CPU time (s): 1200.09
CPU user time (s): 1199.84
CPU system time (s): 0.253961
CPU usage (%): 100.004
Max. virtual memory (Kb): 31372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####