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 5594

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 00:41:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4018 boxname=wulflinc17 idbench=258 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  509cfdb6810b13d9963718243e9046cd  /oldhome/oroussel/tmp/wulflinc17/normalized-circ6_3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-circ6_3.opb /oldhome/oroussel/tmp/wulflinc17/normalized-circ6_3.opb
IDLAUNCH: 4018
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        826364 kB
Buffers:         35664 kB
Cached:         137876 kB
SwapCached:       2376 kB
Active:          58168 kB
Inactive:       120732 kB
HighTotal:      131008 kB
HighFree:          336 kB
LowTotal:       903652 kB
LowFree:        826028 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23756 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:01:08 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4018 7 1200.21 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   17376    49254 |    5212       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5250          
c   -- var.elim.:  2000/5250          
c   -- var.elim.:  3000/5250          
c   -- var.elim.:  4000/5250          
c   -- var.elim.:  5000/5250          
c   -- var.elim.:  5250/5250          
c   -- var.elim.:  1000/1626          
c   -- var.elim.:  1626/1626          
c   -- subsuming                       
c   -- var.elim.:  1000/1249          
c   -- var.elim.:  1249/1249          
c   -- var.elim.:  1000/1110          
c   -- var.elim.:  1110/1110          
c   -- subsuming                       
c   -- var.elim.:  601/601          
c |         0 |   15960    43686 |      --       0       --      -- |     --   | -1416/-3096
c |         0 |   15960    43686 |    6384       0        0     nan |  0.000 % |
c |       101 |   15960    43686 |    7022     101     2080    20.6 | 32.207 % |
c ==============================================================================
c (current CPU-time: 0.891864 s)
c ==============================================================================
c [1mFound solution: 86[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6902     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       156 |   28193    72252 |    8457     156     3869    24.8 | 32.207 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5833          
c   -- var.elim.:  2000/5833          
c   -- var.elim.:  3000/5833          
c   -- var.elim.:  4000/5833          
c   -- var.elim.:  5000/5833          
c   -- var.elim.:  5833/5833          
c   -- var.elim.:  1000/3042          
c   -- var.elim.:  2000/3042          
c   -- var.elim.:  3000/3042          
c   -- var.elim.:  3042/3042          
c   -- var.elim.:  725/725          
c   -- var.elim.:  643/643          
c   -- subsuming                       
c   -- var.elim.:  1000/1585          
c   -- var.elim.:  1585/1585          
c   -- var.elim.:  71/71          
c |       156 |   25570    84614 |      --     156       --      -- |     --   | -2623/12363
c |       156 |   25570    84614 |   10228     156     3869    24.8 | 32.207 % |
c |       256 |   25570    84614 |   11250     256    10225    39.9 | 22.540 % |
c |       406 |   24634    80090 |   11922     379    11540    30.4 | 24.092 % |
c |       631 |   24634    80090 |   13115     604    21101    34.9 | 24.092 % |
c ==============================================================================
c (current CPU-time: 4.47832 s)
c ==============================================================================
c [1mFound solution: 84[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       799 |   24599    80028 |    7379     771    23719    30.8 | 24.092 % |
c   -- subsuming                       
c   -- var.elim.:  843/843          
c   -- var.elim.:  788/788          
c   -- var.elim.:  706/706          
c   -- var.elim.:  778/778          
c   -- var.elim.:  804/804          
c   -- var.elim.:  516/516          
c   -- subsuming                       
c   -- var.elim.:  714/714          
c |       799 |   24335    78206 |      --     771       --      -- |     --   | -263/-1819
c |       799 |   24335    78206 |    9734     747    19201    25.7 | 24.092 % |
c ==============================================================================
c (current CPU-time: 6.39003 s)
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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       828 |   25563    81666 |    7668     776    19721    25.4 | 24.092 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2008          
c   -- var.elim.:  2000/2008          
c   -- var.elim.:  2008/2008          
c   -- var.elim.:  1000/1053          
c   -- var.elim.:  1053/1053          
c   -- var.elim.:  536/536          
c   -- var.elim.:  520/520          
c   -- var.elim.:  585/585          
c   -- var.elim.:  577/577          
c   -- subsuming                       
c   -- var.elim.:  684/684          
c |       828 |   24385    78668 |      --     776       --      -- |     --   | -1178/-2997
c |       828 |   24385    78668 |    9754     776    19721    25.4 | 24.092 % |
c |       928 |   24385    78668 |   10729     876    29810    34.0 | 24.656 % |
c |      1078 |   24385    78668 |   11802    1026    34085    33.2 | 24.656 % |
c |      1303 |   24385    78668 |   12982    1251    40960    32.7 | 24.656 % |
c |      1640 |   24385    78668 |   14280    1588    52528    33.1 | 24.656 % |
c ==============================================================================
c (current CPU-time: 9.2136 s)
c ==============================================================================
c [1mFound solution: 76[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1866 |   24403    78763 |    7320    1814    60134    33.1 | 24.656 % |
c   -- subsuming                       
c   -- var.elim.:  75/75          
c   -- var.elim.:  63/63          
c |      1866 |   24392    78798 |      --    1814       --      -- |     --   | -11/36
c |      1866 |   24392    78798 |    9756    1814    60134    33.1 | 24.656 % |
c |      1967 |   24392    78798 |   10732    1915    68177    35.6 | 24.661 % |
c |      2117 |   23872    75571 |   11554    2050    70032    34.2 | 25.515 % |
c |      2342 |   23872    75571 |   12709    2275    77088    33.9 | 25.515 % |
c |      2680 |   23444    74161 |   13729    2594    82381    31.8 | 26.300 % |
c |      3186 |   23444    74161 |   15102    3100   137746    44.4 | 26.300 % |
c |      3946 |   23444    74161 |   16612    3860   165449    42.9 | 26.300 % |
c |      5087 |   23444    74161 |   18274    5001   212533    42.5 | 26.300 % |
c |      6795 |   23444    74161 |   20101    6709   390225    58.2 | 26.300 % |
c ==============================================================================
c (current CPU-time: 18.9241 s)
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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8949 |   23494    74330 |    7048    8863   577791    65.2 | 26.300 % |
c   -- subsuming                       
c   -- var.elim.:  950/950          
c   -- var.elim.:  886/886          
c   -- var.elim.:  592/592          
c   -- var.elim.:  740/740          
c   -- var.elim.:  660/660          
c   -- var.elim.:  524/524          
c   -- subsuming                       
c   -- var.elim.:  653/653          
c   -- var.elim.:  25/25          
c |      8949 |   23196    74213 |      --    8863       --      -- |     --   | -298/-116
c |      8949 |   23196    74213 |    9278    7521   283855    37.7 | 26.300 % |
c |      9050 |   23196    74213 |   10206    7622   287822    37.8 | 26.784 % |
c |      9200 |   23196    74213 |   11226    7772   291851    37.6 | 26.784 % |
c |      9425 |   23196    74213 |   12349    7997   311402    38.9 | 26.784 % |
c |      9762 |   23196    74213 |   13584    8334   318610    38.2 | 26.784 % |
c |     10269 |   23196    74213 |   14942    8841   362427    41.0 | 26.784 % |
c |     11028 |   23196    74213 |   16437    9600   408309    42.5 | 26.784 % |
c |     12169 |   23100    73889 |   18006   10735   487595    45.4 | 26.935 % |
c |     13879 |   23100    73889 |   19806   12445   562969    45.2 | 26.935 % |
c |     16441 |   23100    73889 |   21787   15007   720199    48.0 | 26.935 % |
c ==============================================================================
c (current CPU-time: 34.1898 s)
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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17583 |   23118    73975 |    6935   16149   840638    52.1 | 26.935 % |
c   -- subsuming                       
c   -- var.elim.:  151/151          
c   -- var.elim.:  125/125          
c |     17583 |   23101    74006 |      --   16149       --      -- |     --   | -17/32
c |     17583 |   23101    74006 |    9240   15902   796465    50.1 | 26.935 % |
c |     17683 |   23101    74006 |   10164   10702   574372    53.7 | 26.962 % |
c |     17833 |   23101    74006 |   11180   10852   582054    53.6 | 26.962 % |
c |     18058 |   23101    74006 |   12298   11077   594656    53.7 | 26.962 % |
c |     18395 |   23101    74006 |   13528   11414   608412    53.3 | 26.962 % |
c |     18902 |   23101    74006 |   14881   11921   653876    54.9 | 26.962 % |
c |     19662 |   23101    74006 |   16369   12681   707811    55.8 | 26.962 % |
c |     20801 |   23101    74006 |   18006   13820   775688    56.1 | 26.962 % |
c |     22509 |   23061    73771 |   19773   15527   851963    54.9 | 27.020 % |
c |     25072 |   23061    73771 |   21750   18090  1084353    59.9 | 27.020 % |
c |     28918 |   22982    73473 |   23843   21919  1356274    61.9 | 27.147 % |
c |     34684 |   22982    73473 |   26228   13896  1126686    81.1 | 27.147 % |
c |     43333 |   22982    73473 |   28850   22545  2237520    99.2 | 27.147 % |
c |     56307 |   22964    73355 |   31711   17355  1973797   113.7 | 27.252 % |
c |     75771 |   22964    73355 |   34882   14558  1202362    82.6 | 27.252 % |
c |    104965 |   22964    73355 |   38370   18537  2354745   127.0 | 27.252 % |
c ==============================================================================
c (current CPU-time: 185.744 s)
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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    120250 |   24356    77053 |    7306   33809  3682839   108.9 | 27.252 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2209          
c   -- var.elim.:  2000/2209          
c   -- var.elim.:  2209/2209          
c   -- var.elim.:  1000/1121          
c   -- var.elim.:  1121/1121          
c   -- var.elim.:  831/831          
c   -- var.elim.:  706/706          
c   -- var.elim.:  55/55          
c   -- subsuming                       
c   -- var.elim.:  592/592          
c |    120250 |   22936    73322 |      --   33809       --      -- |     --   | -1420/-3730
c |    120250 |   22936    73322 |    9174   25697  1999436    77.8 | 27.252 % |
c |    120350 |   22936    73322 |   10091    9038   580353    64.2 | 27.326 % |
c |    120502 |   22936    73322 |   11101    9190   591983    64.4 | 27.326 % |
c |    120727 |   22881    73094 |   12181    9413   598201    63.6 | 27.407 % |
c |    121064 |   22881    73094 |   13400    9750   607451    62.3 | 27.407 % |
c |    121570 |   22881    73094 |   14740   10256   634618    61.9 | 27.407 % |
c |    122329 |   22881    73094 |   16214   11015   709707    64.4 | 27.407 % |
c |    123469 |   22881    73094 |   17835   12155   802402    66.0 | 27.407 % |
c |    125178 |   22881    73094 |   19618   13864   981894    70.8 | 27.407 % |
c |    127741 |   22881    73094 |   21580   16427  1238691    75.4 | 27.407 % |
c |    131585 |   22881    73094 |   23738   20271  1696321    83.7 | 27.407 % |
c |    137351 |   22881    73094 |   26112   26037  2383363    91.5 | 27.407 % |
c |    146001 |   22881    73094 |   28724   19750  1848971    93.6 | 27.407 % |
c |    158976 |   22863    72996 |   31571   14606  1627937   111.5 | 27.511 % |
c |    178437 |   22863    72996 |   34728   34067  3746050   110.0 | 27.511 % |
c |    207632 |   22863    72996 |   #### 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.77 0.92 0.89 2/55 27200
Raw data (stat): 27200 (runsolver) R 27199 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480355548 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.81 0.92 0.89 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 3432 0 0 0 985 12 0 0 25 0 1 0 480355548 11423744 2307 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2789 2307 603 41 0 2748 0
vsize: 11156
[startup+19.9998 s]
Raw data (loadavg): 0.84 0.93 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 4236 0 0 0 1981 16 0 0 25 0 1 0 480355548 14176256 2945 4294967295 134512640 134672761 3221224560 3221223008 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2945 603 41 0 3420 0
vsize: 13844
[startup+29.9993 s]
Raw data (loadavg): 0.86 0.93 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 4241 0 0 0 2981 16 0 0 25 0 1 0 480355548 14176256 2950 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3461 2950 603 41 0 3420 0
vsize: 13844
[startup+39.9989 s]
Raw data (loadavg): 0.88 0.93 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 4770 0 0 0 3979 19 0 0 25 0 1 0 480355548 15601664 3313 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3809 3313 603 41 0 3768 0
vsize: 15236
[startup+49.9988 s]
Raw data (loadavg): 0.90 0.93 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 4986 0 0 0 4978 19 0 0 25 0 1 0 480355548 16523264 3529 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4034 3529 603 41 0 3993 0
vsize: 16136
[startup+59.9991 s]
Raw data (loadavg): 0.91 0.93 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 5629 0 0 0 5976 22 0 0 25 0 1 0 480355548 19214336 4172 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 4172 603 41 0 4650 0
vsize: 18764
[startup+69.9987 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 6402 0 0 0 6974 24 0 0 25 0 1 0 480355548 22253568 4945 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5433 4945 603 41 0 5392 0
vsize: 21732
[startup+79.9986 s]
Raw data (loadavg): 0.94 0.94 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7374 0 0 0 7972 27 0 0 25 0 1 0 480355548 26345472 5917 4294967295 134512640 134672761 3221224560 3221223616 134644277 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6432 5917 603 41 0 6391 0
vsize: 25728
[startup+89.9979 s]
Raw data (loadavg): 0.95 0.94 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7393 0 0 0 8972 27 0 0 25 0 1 0 480355548 26345472 5936 4294967295 134512640 134672761 3221224560 3221223496 1075350746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6432 5936 603 41 0 6391 0
vsize: 25728
[startup+99.9975 s]
Raw data (loadavg): 0.95 0.94 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7393 0 0 0 9972 27 0 0 25 0 1 0 480355548 26345472 5936 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6432 5936 603 41 0 6391 0
vsize: 25728
[startup+109.998 s]
Raw data (loadavg): 0.96 0.94 0.90 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7732 0 0 0 10971 28 0 0 25 0 1 0 480355548 27930624 6275 4294967295 134512640 134672761 3221224560 3221223600 134612799 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6275 603 41 0 6778 0
vsize: 27276
[startup+119.999 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7881 0 0 0 11971 28 0 0 25 0 1 0 480355548 28303360 6389 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6910 6389 603 41 0 6869 0
vsize: 27640
[startup+129.998 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7881 0 0 0 12971 28 0 0 25 0 1 0 480355548 28303360 6389 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6910 6389 603 41 0 6869 0
vsize: 27640
[startup+139.998 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7881 0 0 0 13971 28 0 0 25 0 1 0 480355548 28303360 6389 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6910 6389 603 41 0 6869 0
vsize: 27640
[startup+149.998 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 7882 0 0 0 14971 28 0 0 25 0 1 0 480355548 28303360 6390 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6910 6390 603 41 0 6869 0
vsize: 27640
[startup+159.997 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8221 0 0 0 15970 30 0 0 25 0 1 0 480355548 29642752 6721 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6721 603 41 0 7196 0
vsize: 28948
[startup+169.997 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8221 0 0 0 16970 30 0 0 25 0 1 0 480355548 29642752 6721 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6721 603 41 0 7196 0
vsize: 28948
[startup+179.996 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8221 0 0 0 17970 30 0 0 25 0 1 0 480355548 29642752 6721 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6721 603 41 0 7196 0
vsize: 28948
[startup+189.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 18967 32 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+199.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 19967 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+209.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 20966 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+220.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 21967 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 22967 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 23967 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 24967 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+260.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27200
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 25968 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+270.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8635 0 0 0 26968 33 0 0 25 0 1 0 480355548 29642752 6743 4294967295 134512640 134672761 3221224560 3221223744 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6743 603 41 0 7196 0
vsize: 28948
[startup+280.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 8703 0 0 0 27968 34 0 0 25 0 1 0 480355548 30048256 6811 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7336 6811 603 41 0 7295 0
vsize: 29344
[startup+290.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9177 0 0 0 28967 35 0 0 25 0 1 0 480355548 31723520 7248 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7745 7248 603 41 0 7704 0
vsize: 30980
[startup+300.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9177 0 0 0 29967 35 0 0 25 0 1 0 480355548 31723520 7248 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7745 7248 603 41 0 7704 0
vsize: 30980
[startup+310.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9177 0 0 0 30967 35 0 0 25 0 1 0 480355548 31723520 7248 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7745 7248 603 41 0 7704 0
vsize: 30980
[startup+320.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9177 0 0 0 31968 35 0 0 25 0 1 0 480355548 31723520 7248 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7745 7248 603 41 0 7704 0
vsize: 30980
[startup+330.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9215 0 0 0 32967 35 0 0 25 0 1 0 480355548 31703040 7243 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7740 7243 603 41 0 7699 0
vsize: 30960
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9215 0 0 0 33967 35 0 0 25 0 1 0 480355548 31703040 7243 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7740 7243 603 41 0 7699 0
vsize: 30960
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9215 0 0 0 34967 35 0 0 25 0 1 0 480355548 31703040 7243 4294967295 134512640 134672761 3221224560 3221223792 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7740 7243 603 41 0 7699 0
vsize: 30960
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 9908 0 0 0 35965 38 0 0 25 0 1 0 480355548 34594816 7936 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8446 7936 603 41 0 8405 0
vsize: 33784
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 10548 0 0 0 36962 41 0 0 25 0 1 0 480355548 37122048 8566 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9063 8566 603 41 0 9022 0
vsize: 36252
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 10548 0 0 0 37963 41 0 0 25 0 1 0 480355548 37122048 8566 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9063 8566 603 41 0 9022 0
vsize: 36252
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 10548 0 0 0 38964 41 0 0 25 0 1 0 480355548 37122048 8566 4294967295 134512640 134672761 3221224560 3221223600 134612606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9063 8566 603 41 0 9022 0
vsize: 36252
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 10548 0 0 0 39964 41 0 0 25 0 1 0 480355548 37122048 8566 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9063 8566 603 41 0 9022 0
vsize: 36252
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 10548 0 0 0 40964 41 0 0 25 0 1 0 480355548 37122048 8566 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9063 8566 603 41 0 9022 0
vsize: 36252
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 10548 0 0 0 41964 41 0 0 25 0 1 0 480355548 37122048 8566 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9063 8566 603 41 0 9022 0
vsize: 36252
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 10915 0 0 0 42963 42 0 0 25 0 1 0 480355548 38694912 8933 4294967295 134512640 134672761 3221224560 3221223696 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9447 8933 603 41 0 9406 0
vsize: 37788
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11394 0 0 0 43962 43 0 0 25 0 1 0 480355548 40415232 9368 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9368 603 41 0 9826 0
vsize: 39468
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11394 0 0 0 44962 43 0 0 25 0 1 0 480355548 40415232 9368 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9368 603 41 0 9826 0
vsize: 39468
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11394 0 0 0 45962 43 0 0 25 0 1 0 480355548 40415232 9368 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9368 603 41 0 9826 0
vsize: 39468
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11394 0 0 0 46963 43 0 0 25 0 1 0 480355548 40415232 9368 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9368 603 41 0 9826 0
vsize: 39468
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11395 0 0 0 47963 43 0 0 25 0 1 0 480355548 40415232 9369 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9369 603 41 0 9826 0
vsize: 39468
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11395 0 0 0 48963 43 0 0 25 0 1 0 480355548 40415232 9369 4294967295 134512640 134672761 3221224560 3221223452 1075346629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9369 603 41 0 9826 0
vsize: 39468
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11395 0 0 0 49963 43 0 0 25 0 1 0 480355548 40415232 9369 4294967295 134512640 134672761 3221224560 3221223792 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9369 603 41 0 9826 0
vsize: 39468
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11395 0 0 0 50963 44 0 0 25 0 1 0 480355548 40415232 9369 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9369 603 41 0 9826 0
vsize: 39468
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11396 0 0 0 51963 44 0 0 25 0 1 0 480355548 40415232 9370 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9370 603 41 0 9826 0
vsize: 39468
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11397 0 0 0 52963 44 0 0 25 0 1 0 480355548 40415232 9371 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9371 603 41 0 9826 0
vsize: 39468
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11397 0 0 0 53963 44 0 0 25 0 1 0 480355548 40415232 9371 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9371 603 41 0 9826 0
vsize: 39468
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11397 0 0 0 54963 44 0 0 25 0 1 0 480355548 40415232 9371 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9371 603 41 0 9826 0
vsize: 39468
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27202
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11397 0 0 0 55963 44 0 0 25 0 1 0 480355548 40415232 9371 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9371 603 41 0 9826 0
vsize: 39468
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11398 0 0 0 56963 44 0 0 25 0 1 0 480355548 40415232 9372 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9372 603 41 0 9826 0
vsize: 39468
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 57963 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223712 134616683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 58964 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 59964 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 60964 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 61964 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 62964 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 63964 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 64965 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 65965 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11438 0 0 0 66965 44 0 0 25 0 1 0 480355548 40677376 9412 4294967295 134512640 134672761 3221224560 3221223600 134612867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9931 9412 603 41 0 9890 0
vsize: 39724
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11501 0 0 0 67965 44 0 0 25 0 1 0 480355548 40943616 9475 4294967295 134512640 134672761 3221224560 3221223744 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9996 9475 603 41 0 9955 0
vsize: 39984
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 11813 0 0 0 68965 45 0 0 25 0 1 0 480355548 42323968 9787 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10333 9787 603 41 0 10292 0
vsize: 41332
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12104 0 0 0 69964 46 0 0 25 0 1 0 480355548 43515904 10078 4294967295 134512640 134672761 3221224560 3221223696 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10624 10078 603 41 0 10583 0
vsize: 42496
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12433 0 0 0 70963 47 0 0 25 0 1 0 480355548 44826624 10407 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10944 10407 603 41 0 10903 0
vsize: 43776
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12794 0 0 0 71963 47 0 0 25 0 1 0 480355548 46399488 10768 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11328 10768 603 41 0 11287 0
vsize: 45312
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 72962 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 73963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 74963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 75963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 76963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 77963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 78963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 79963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 80963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 81963 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 82964 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 83964 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12910 0 0 0 84964 48 0 0 25 0 1 0 480355548 46718976 10866 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10866 603 41 0 11365 0
vsize: 45624
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27204
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 85964 48 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223600 134613822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 86964 48 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+880.019 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 87965 48 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+890.019 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 88965 48 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+900.018 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 89965 48 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+910.019 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 90965 48 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+920.019 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 91965 48 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+930.018 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 92965 49 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+940.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 93965 49 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+950.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 94965 49 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+960.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 95965 49 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223600 134612510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+970.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12944 0 0 0 96965 49 0 0 25 0 1 0 480355548 46784512 10882 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10882 603 41 0 11381 0
vsize: 45688
[startup+980.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12945 0 0 0 97965 49 0 0 25 0 1 0 480355548 46784512 10883 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10883 603 41 0 11381 0
vsize: 45688
[startup+990.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 12947 0 0 0 98965 49 0 0 25 0 1 0 480355548 46784512 10885 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10885 603 41 0 11381 0
vsize: 45688
[startup+1000.02 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 99965 49 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1010.02 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 100966 49 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1020.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 101966 49 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1030.02 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 102966 49 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1040.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 103966 49 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1050.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 104966 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1060.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 105967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1070.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 106967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1080.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 107967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1090.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 108967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1100.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 109967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1110.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 110967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1120.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 111967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1130.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27206
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 112967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 3/57 27220
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 113967 50 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1150.02 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 27259
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13005 0 0 0 114966 51 0 0 25 0 1 0 480355548 46784512 10890 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10890 603 41 0 11381 0
vsize: 45688
[startup+1160.02 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 27259
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13159 0 0 0 115966 51 0 0 25 0 1 0 480355548 47439872 11044 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11582 11044 603 41 0 11541 0
vsize: 46328
[startup+1170.02 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 27261
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13449 0 0 0 116965 52 0 0 25 0 1 0 480355548 48635904 11334 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11874 11334 603 41 0 11833 0
vsize: 47496
[startup+1180.02 s]
Raw data (loadavg): 1.12 1.03 0.93 2/55 27261
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13595 0 0 0 117965 53 0 0 25 0 1 0 480355548 49004544 11427 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11964 11427 603 41 0 11923 0
vsize: 47856
[startup+1190.02 s]
Raw data (loadavg): 1.10 1.03 0.93 2/55 27261
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13595 0 0 0 118965 53 0 0 25 0 1 0 480355548 49004544 11427 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11964 11427 603 41 0 11923 0
vsize: 47856
[startup+1200.02 s]
Raw data (loadavg): 1.08 1.03 0.93 2/55 27261
Raw data (stat): 27200 (minisat+) R 27199 20838 20837 0 -1 0 13595 0 0 0 119965 53 0 0 25 0 1 0 480355548 49004544 11427 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11964 11427 603 41 0 11923 0
vsize: 47856
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.08 1.03 0.93 1/55 27261
Raw data (stat): 27200 (minisat+) Z 27199 20838 20837 0 -1 12 13596 0 0 0 119965 55 0 0 25 0 1 0 480355548 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.66
CPU system time (s): 0.555915
CPU usage (%): 100.014
Max. virtual memory (Kb): 47856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####