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 6348

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        890428 kB
Buffers:         36392 kB
Cached:          87912 kB
SwapCached:          0 kB
Active:          55616 kB
Inactive:        71544 kB
HighTotal:      131008 kB
HighFree:        39284 kB
LowTotal:       903652 kB
LowFree:        851144 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11564 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:45:14 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4770 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4626 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[4624]---> BDD-cost:   17
c ---[4622]---> BDD-cost:   17
c ---[4620]---> BDD-cost:   17
c ---[4618]---> BDD-cost:   17
c ---[4616]---> BDD-cost:   17
c ---[4614]---> BDD-cost:   17
c ---[4612]---> BDD-cost:   17
c ---[4610]---> BDD-cost:   17
c ---[4608]---> BDD-cost:   17
c ---[4606]---> BDD-cost:   17
c ---[4604]---> BDD-cost:   17
c ---[4602]---> BDD-cost:   17
c ---[4600]---> BDD-cost:   17
c ---[4598]---> BDD-cost:   17
c ---[4596]---> BDD-cost:   17
c ---[4594]---> BDD-cost:   17
c ---[4592]---> BDD-cost:   17
c ---[4590]---> BDD-cost:   17
c ---[4588]---> BDD-cost:   17
c ---[4586]---> BDD-cost:   17
c ---[4584]---> BDD-cost:   17
c ---[4582]---> BDD-cost:   17
c ---[4580]---> BDD-cost:   17
c ---[4578]---> BDD-cost:   17
c ---[4576]---> BDD-cost:   17
c ---[4574]---> BDD-cost:   17
c ---[4572]---> BDD-cost:   17
c ---[4570]---> BDD-cost:   17
c ---[4568]---> BDD-cost:   17
c ---[4566]---> BDD-cost:   17
c ---[4265]---> BDD-cost:    7
c ---[4264]---> BDD-cost:    7
c ---[4263]---> BDD-cost:    7
c ---[4262]---> BDD-cost:    7
c ---[4261]---> BDD-cost:    7
c ---[4260]---> BDD-cost:    7
c ---[4259]---> BDD-cost:    7
c ---[4258]---> BDD-cost:    7
c ---[4257]---> BDD-cost:    7
c ---[4256]---> BDD-cost:    7
c ---[4255]---> BDD-cost:    7
c ---[4254]---> BDD-cost:    7
c ---[4253]---> BDD-cost:    7
c ---[4252]---> BDD-cost:    7
c ---[4251]---> BDD-cost:    7
c ---[4250]---> BDD-cost:    7
c ---[4249]---> BDD-cost:    7
c ---[4248]---> BDD-cost:    7
c ---[4247]---> BDD-cost:    7
c ---[4246]---> BDD-cost:    7
c ---[4245]---> BDD-cost:    7
c ---[4244]---> BDD-cost:    7
c ---[4243]---> BDD-cost:    7
c ---[4242]---> BDD-cost:    7
c ---[4241]---> BDD-cost:    7
c ---[4240]---> BDD-cost:    7
c ---[4239]---> BDD-cost:    7
c ---[4238]---> BDD-cost:    7
c ---[4237]---> BDD-cost:    7
c ---[4236]---> BDD-cost:    7
c ---[4235]---> BDD-cost:    7
c ---[4234]---> BDD-cost:    7
c ---[4233]---> BDD-cost:    7
c ---[4232]---> BDD-cost:    7
c ---[4231]---> BDD-cost:    7
c ---[4230]---> BDD-cost:    7
c ---[4229]---> BDD-cost:    7
c ---[4228]---> BDD-cost:    7
c ---[4227]---> BDD-cost:    7
c ---[4226]---> BDD-cost:    7
c ---[4225]---> BDD-cost:    7
c ---[4224]---> BDD-cost:    7
c ---[4223]---> BDD-cost:    7
c ---[4222]---> BDD-cost:    7
c ---[4221]---> BDD-cost:    7
c ---[4220]---> BDD-cost:    7
c ---[4219]---> BDD-cost:    7
c ---[4218]---> BDD-cost:    7
c ---[4217]---> BDD-cost:    7
c ---[4216]---> BDD-cost:    7
c ---[4215]---> BDD-cost:    7
c ---[4214]---> BDD-cost:    7
c ---[4213]---> BDD-cost:    7
c ---[4212]---> BDD-cost:    7
c ---[4211]---> BDD-cost:    7
c ---[4210]---> BDD-cost:    7
c ---[4209]---> BDD-cost:    7
c ---[4208]---> BDD-cost:    7
c ---[4207]---> BDD-cost:    7
c ---[4206]---> BDD-cost:    7
c ---[4204]---> BDD-cost:    9
c ---[4202]---> BDD-cost:    9
c ---[4200]---> BDD-cost:    9
c ---[4198]---> BDD-cost:    9
c ---[4196]---> BDD-cost:    9
c ---[4194]---> BDD-cost:    9
c ---[4192]---> BDD-cost:    9
c ---[4190]---> BDD-cost:    9
c ---[4188]---> BDD-cost:    9
c ---[4186]---> BDD-cost:    9
c ---[4184]---> BDD-cost:    9
c ---[4182]---> BDD-cost:    9
c ---[4180]---> BDD-cost:    9
c ---[4178]---> BDD-cost:    9
c ---[4176]---> BDD-cost:    9
c ---[4174]---> BDD-cost:    9
c ---[4172]---> BDD-cost:    9
c ---[4170]---> BDD-cost:    9
c ---[4168]---> BDD-cost:    9
c ---[4166]---> BDD-cost:    9
c ---[4164]---> BDD-cost:    9
c ---[4162]---> BDD-cost:    9
c ---[4160]---> BDD-cost:    9
c ---[4158]---> BDD-cost:    9
c ---[4156]---> BDD-cost:    9
c ---[4154]---> BDD-cost:    9
c ---[4152]---> BDD-cost:    9
c ---[4150]---> BDD-cost:    9
c ---[4148]---> BDD-cost:    9
c ---[4146]---> BDD-cost:    9
c ---[4144]---> BDD-cost:    9
c ---[4142]---> BDD-cost:    9
c ---[4140]---> BDD-cost:    9
c ---[4138]---> BDD-cost:    9
c ---[4136]---> BDD-cost:    9
c ---[4134]---> BDD-cost:    9
c ---[4132]---> BDD-cost:    9
c ---[4130]---> BDD-cost:    9
c ---[4128]---> BDD-cost:    9
c ---[4126]---> BDD-cost:    9
c ---[4124]---> BDD-cost:    9
c ---[4122]---> BDD-cost:    9
c ---[4120]---> BDD-cost:    9
c ---[4118]---> BDD-cost:    9
c ---[4116]---> BDD-cost:    9
c ---[4114]---> BDD-cost:    9
c ---[4112]---> BDD-cost:    9
c ---[4110]---> BDD-cost:    9
c ---[4108]---> BDD-cost:    9
c ---[4106]---> BDD-cost:    9
c ---[4104]---> BDD-cost:    9
c ---[4102]---> BDD-cost:    9
c ---[4100]---> BDD-cost:    9
c ---[4098]---> BDD-cost:    9
c ---[4096]---> BDD-cost:    9
c ---[4094]---> BDD-cost:    9
c ---[4092]---> BDD-cost:    9
c ---[4090]---> BDD-cost:    9
c ---[4088]---> BDD-cost:    9
c ---[4086]---> BDD-cost:    9
c ---[4079]---> BDD-cost:   64
c ---[4078]---> BDD-cost:   64
c ---[4077]---> BDD-cost:   64
c ---[4076]---> BDD-cost:   64
c ---[4075]---> BDD-cost:   64
c ---[4074]---> BDD-cost:   64
c ---[4067]---> BDD-cost:   67
c ---[4066]---> BDD-cost:   67
c ---[4065]---> BDD-cost:   67
c ---[4064]---> BDD-cost:   67
c ---[4063]---> BDD-cost:   67
c ---[4062]---> BDD-cost:   67
c ---[4055]---> BDD-cost:   67
c ---[4054]---> BDD-cost:   67
c ---[4053]---> BDD-cost:   67
c ---[4052]---> BDD-cost:   67
c ---[4051]---> BDD-cost:   67
c ---[4050]---> BDD-cost:   67
c ---[4043]---> BDD-cost:   67
c ---[4042]---> BDD-cost:   67
c ---[4041]---> BDD-cost:   67
c ---[4040]---> BDD-cost:   67
c ---[4039]---> BDD-cost:   67
c ---[4038]---> BDD-cost:   67
c ---[4031]---> BDD-cost:   67
c ---[4030]---> BDD-cost:   67
c ---[4029]---> BDD-cost:   67
c ---[4028]---> BDD-cost:   67
c ---[4027]---> BDD-cost:   67
c ---[4026]---> BDD-cost:   67
c ---[4019]---> BDD-cost:   67
c ---[4018]---> BDD-cost:   67
c ---[4017]---> BDD-cost:   67
c ---[4016]---> BDD-cost:   67
c ---[4015]---> BDD-cost:   67
c ---[4014]---> BDD-cost:   67
c ---[4007]---> BDD-cost:   67
c ---[4006]---> BDD-cost:   67
c ---[4005]---> BDD-cost:   67
c ---[4004]---> BDD-cost:   67
c ---[4003]---> BDD-cost:   67
c ---[4002]---> BDD-cost:   67
c ---[2050]---> BDD-cost:    7
c ---[2048]---> BDD-cost:    7
c ---[2046]---> BDD-cost:    7
c ---[2044]---> BDD-cost:    7
c ---[2042]---> BDD-cost:    7
c ---[2040]---> BDD-cost:    7
c ---[2038]---> BDD-cost:    7
c ---[2036]---> BDD-cost:    7
c ---[2034]---> BDD-cost:    7
c ---[2032]---> BDD-cost:    7
c ---[2030]---> BDD-cost:    7
c ---[2028]---> BDD-cost:    7
c ---[2026]---> BDD-cost:    7
c ---[2024]---> BDD-cost:    7
c ---[2022]---> BDD-cost:    7
c ---[2020]---> BDD-cost:    7
c ---[2018]---> BDD-cost:    7
c ---[2016]---> BDD-cost:    7
c ---[2014]---> BDD-cost:    7
c ---[2012]---> BDD-cost:    7
c ---[2010]---> BDD-cost:    7
c ---[2008]---> BDD-cost:    7
c ---[2006]---> BDD-cost:    7
c ---[2004]---> BDD-cost:    7
c ---[2002]---> BDD-cost:    7
c ---[2000]---> BDD-cost:    7
c ---[1998]---> BDD-cost:    7
c ---[1996]---> BDD-cost:    7
c ---[1994]---> BDD-cost:    7
c ---[1992]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    7
c ---[1988]---> BDD-cost:    7
c ---[1986]---> BDD-cost:    7
c ---[1984]---> BDD-cost:    7
c ---[1982]---> BDD-cost:    7
c ---[1980]---> BDD-cost:    7
c ---[1978]---> BDD-cost:    7
c ---[1976]---> BDD-cost:    7
c ---[1974]---> BDD-cost:    7
c ---[1972]---> BDD-cost:    7
c ---[1970]---> BDD-cost:    7
c ---[1968]---> BDD-cost:    7
c ---[1966]---> BDD-cost:    7
c ---[1964]---> BDD-cost:    7
c ---[1962]---> BDD-cost:    7
c ---[1960]---> BDD-cost:    7
c ---[1958]---> BDD-cost:    7
c ---[1956]---> BDD-cost:    7
c ---[1954]---> BDD-cost:    7
c ---[1952]---> BDD-cost:    7
c ---[1950]---> BDD-cost:    7
c ---[1948]---> BDD-cost:    7
c ---[1946]---> BDD-cost:    7
c ---[1944]---> BDD-cost:    7
c ---[1942]---> BDD-cost:    7
c ---[1940]---> BDD-cost:    7
c ---[1938]---> BDD-cost:    7
c ---[1936]---> BDD-cost:    7
c ---[1934]---> BDD-cost:    7
c ---[1932]---> BDD-cost:    7
c ---[1931]---> BDD-cost:    7
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:    7
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:    7
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1923]---> BDD-cost:    7
c ---[1922]---> BDD-cost:    7
c ---[1921]---> BDD-cost:    7
c ---[1920]---> BDD-cost:    7
c ---[1919]---> BDD-cost:    9
c ---[1918]---> BDD-cost:    2
c ---[1917]---> BDD-cost:    9
c ---[1916]---> BDD-cost:    2
c ---[1915]---> BDD-cost:    9
c ---[1914]---> BDD-cost:    2
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    2
c ---[1911]---> BDD-cost:    8
c ---[1910]---> BDD-cost:    2
c ---[1909]---> BDD-cost:    8
c ---[1908]---> BDD-cost:    2
c ---[1907]---> BDD-cost:    8
c ---[1906]---> BDD-cost:    2
c ---[1905]---> BDD-cost:    8
c ---[1904]---> BDD-cost:    2
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:    2
c ---[1901]---> BDD-cost:    7
c ---[1900]---> BDD-cost:    2
c ---[1899]---> BDD-cost:    7
c ---[1898]---> BDD-cost:    2
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:    2
c ---[1895]---> BDD-cost:    6
c ---[1894]---> BDD-cost:    2
c ---[1893]---> BDD-cost:    6
c ---[1892]---> BDD-cost:    2
c ---[1891]---> BDD-cost:    6
c ---[1890]---> BDD-cost:    2
c ---[1889]---> BDD-cost:    6
c ---[1888]---> BDD-cost:    2
c ---[1887]---> BDD-cost:    5
c ---[1886]---> BDD-cost:    2
c ---[1885]---> BDD-cost:    5
c ---[1884]---> BDD-cost:    2
c ---[1883]---> BDD-cost:    5
c ---[1882]---> BDD-cost:    2
c ---[1881]---> BDD-cost:    5
c ---[1880]---> BDD-cost:    2
c ---[1879]---> BDD-cost:    4
c ---[1878]---> BDD-cost:    2
c ---[1877]---> BDD-cost:    4
c ---[1876]---> BDD-cost:    2
c ---[1875]---> BDD-cost:    4
c ---[1874]---> BDD-cost:    2
c ---[1873]---> BDD-cost:    4
c ---[1872]---> BDD-cost:    2
c ---[1871]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    2
c ---[1869]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    2
c ---[1867]---> BDD-cost:    3
c ---[1866]---> BDD-cost:    2
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    2
c ---[1855]---> BDD-cost:    6
c ---[1854]---> BDD-cost:    2
c ---[1853]---> BDD-cost:    2
c ---[1852]---> BDD-cost:    2
c ---[1851]---> BDD-cost:    2
c ---[1850]---> BDD-cost:    2
c ---[1849]---> BDD-cost:    2
c ---[1848]---> BDD-cost:    2
c ---[1847]---> BDD-cost:    5
c ---[1846]---> BDD-cost:    2
c ---[1845]---> BDD-cost:    2
c ---[1844]---> BDD-cost:    2
c ---[1843]---> BDD-cost:    2
c ---[1842]---> BDD-cost:    2
c ---[1841]---> BDD-cost:    2
c ---[1840]---> BDD-cost:    2
c ---[1839]---> BDD-cost:    4
c ---[1838]---> BDD-cost:    2
c ---[1837]---> BDD-cost:    2
c ---[1836]---> BDD-cost:    2
c ---[1835]---> BDD-cost:    2
c ---[1834]---> BDD-cost:    2
c ---[1833]---> BDD-cost:    2
c ---[1832]---> BDD-cost:    2
c ---[1831]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    2
c ---[1829]---> BDD-cost:    2
c ---[1828]---> BDD-cost:    2
c ---[1827]---> BDD-cost:    2
c ---[1826]---> BDD-cost:    2
c ---[1825]---> BDD-cost:    2
c ---[1824]---> BDD-cost:    2
c ---[1823]---> BDD-cost:    2
c ---[1822]---> BDD-cost:    2
c ---[1821]---> BDD-cost:    2
c ---[1820]---> BDD-cost:    2
c ---[1819]---> BDD-cost:    2
c ---[1818]---> BDD-cost:    2
c ---[1817]---> BDD-cost:    2
c ---[1816]---> BDD-cost:    2
c ---[1815]---> BDD-cost:    4
c ---[1814]---> BDD-cost:    2
c ---[1813]---> BDD-cost:    2
c ---[1812]---> BDD-cost:    2
c ---[1811]---> BDD-cost:    2
c ---[1810]---> BDD-cost:    2
c ---[1809]---> BDD-cost:    2
c ---[1808]---> BDD-cost:    2
c ---[1807]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    2
c ---[1805]---> BDD-cost:    2
c ---[1804]---> BDD-cost:    2
c ---[1803]---> BDD-cost:    2
c ---[1802]---> BDD-cost:    2
c ---[1801]---> BDD-cost:    2
c ---[1800]---> BDD-cost:    2
c ---[1791]---> BDD-cost:    2
c ---[1790]---> BDD-cost:    2
c ---[1789]---> BDD-cost:    2
c ---[1788]---> BDD-cost:    2
c ---[1787]---> BDD-cost:    2
c ---[1786]---> BDD-cost:    2
c ---[1785]---> BDD-cost:    2
c ---[1784]---> BDD-cost:    2
c ---[1783]---> BDD-cost:    2
c ---[1782]---> BDD-cost:    2
c ---[1781]---> BDD-cost:    2
c ---[1780]---> BDD-cost:    2
c ---[1779]---> BDD-cost:    2
c ---[1778]---> BDD-cost:    2
c ---[1777]---> BDD-cost:    2
c ---[1776]---> BDD-cost:    2
c ---[1775]---> BDD-cost:    2
c ---[1774]---> BDD-cost:    2
c ---[1773]---> BDD-cost:    2
c ---[1772]---> BDD-cost:    2
c ---[1771]---> BDD-cost:    2
c ---[1770]---> BDD-cost:    2
c ---[1769]---> BDD-cost:    2
c ---[1768]---> BDD-cost:    2
c ---[1767]---> BDD-cost:    2
c ---[1766]---> BDD-cost:    2
c ---[1765]---> BDD-cost:    2
c ---[1764]---> BDD-cost:    2
c ---[1763]---> BDD-cost:    2
c ---[1762]---> BDD-cost:    2
c ---[1761]---> BDD-cost:    2
c ---[1760]---> BDD-cost:    2
c ---[1759]---> BDD-cost:    2
c ---[1758]---> BDD-cost:    2
c ---[1757]---> BDD-cost:    2
c ---[1756]---> BDD-cost:    2
c ---[1755]---> BDD-cost:    2
c ---[1754]---> BDD-cost:    2
c ---[1753]---> BDD-cost:    2
c ---[1752]---> BDD-cost:    2
c ---[1751]---> BDD-cost:    2
c ---[1750]---> BDD-cost:    2
c ---[1749]---> BDD-cost:    2
c ---[1748]---> BDD-cost:    2
c ---[1747]---> BDD-cost:    2
c ---[1746]---> BDD-cost:    2
c ---[1745]---> BDD-cost:    2
c ---[1744]---> BDD-cost:    2
c ---[1743]---> BDD-cost:    2
c ---[1742]---> BDD-cost:    2
c ---[1741]---> BDD-cost:    2
c ---[1740]---> BDD-cost:    2
c ---[1739]---> BDD-cost:    2
c ---[1738]---> BDD-cost:    2
c ---[1737]---> BDD-cost:    2
c ---[1736]---> BDD-cost:    2
c ---[1727]---> BDD-cost:    2
c ---[1726]---> BDD-cost:    2
c ---[1725]---> BDD-cost:    2
c ---[1724]---> BDD-cost:    2
c ---[1723]---> BDD-cost:    2
c ---[1722]---> BDD-cost:    2
c ---[1721]---> BDD-cost:    2
c ---[1720]---> BDD-cost:    2
c ---[1719]---> BDD-cost:    2
c ---[1718]---> BDD-cost:    2
c ---[1717]---> BDD-cost:    2
c ---[1716]---> BDD-cost:    2
c ---[1715]---> BDD-cost:    2
c ---[1714]---> BDD-cost:    2
c ---[1713]---> BDD-cost:    2
c ---[1712]---> BDD-cost:    2
c ---[1711]---> BDD-cost:    2
c ---[1710]---> BDD-cost:    2
c ---[1709]---> BDD-cost:    2
c ---[1708]---> BDD-cost:    2
c ---[1707]---> BDD-cost:    2
c ---[1706]---> BDD-cost:    2
c ---[1705]---> BDD-cost:    2
c ---[1704]---> BDD-cost:    2
c ---[1703]---> BDD-cost:    2
c ---[1702]---> BDD-cost:    2
c ---[1701]---> BDD-cost:    2
c ---[1700]---> BDD-cost:    2
c ---[1699]---> BDD-cost:    2
c ---[1698]---> BDD-cost:    2
c ---[1697]---> BDD-cost:    2
c ---[1696]---> BDD-cost:    2
c ---[1695]---> BDD-cost:    2
c ---[1694]---> BDD-cost:    2
c ---[1693]---> BDD-cost:    2
c ---[1692]---> BDD-cost:    2
c ---[1691]---> BDD-cost:    2
c ---[1690]---> BDD-cost:    2
c ---[1689]---> BDD-cost:    2
c ---[1688]---> BDD-cost:    2
c ---[1687]---> BDD-cost:    2
c ---[1686]---> BDD-cost:    2
c ---[1685]---> BDD-cost:    2
c ---[1684]---> BDD-cost:    2
c ---[1683]---> BDD-cost:    2
c ---[1682]---> BDD-cost:    2
c ---[1681]---> BDD-cost:    2
c ---[1680]---> BDD-cost:    2
c ---[1679]---> BDD-cost:    2
c ---[1678]---> BDD-cost:    2
c ---[1677]---> BDD-cost:    2
c ---[1676]---> BDD-cost:    2
c ---[1675]---> BDD-cost:    2
c ---[1674]---> BDD-cost:    2
c ---[1673]---> BDD-cost:    2
c ---[1672]---> BDD-cost:    2
c ---[1663]---> BDD-cost:    2
c ---[1662]---> BDD-cost:    2
c ---[1661]---> BDD-cost:    2
c ---[1660]---> BDD-cost:    2
c ---[1659]---> BDD-cost:    2
c ---[1658]---> BDD-cost:    2
c ---[1657]---> BDD-cost:    2
c ---[1656]---> BDD-cost:    2
c ---[1655]---> BDD-cost:    2
c ---[1654]---> BDD-cost:    2
c ---[1653]---> BDD-cost:    2
c ---[1652]---> BDD-cost:    2
c ---[1651]---> BDD-cost:    2
c ---[1650]---> BDD-cost:    2
c ---[1649]---> BDD-cost:    2
c ---[1648]---> BDD-cost:    2
c ---[1647]---> BDD-cost:    2
c ---[1646]---> BDD-cost:    2
c ---[1645]---> BDD-cost:    2
c ---[1644]---> BDD-cost:    2
c ---[1643]---> BDD-cost:    2
c ---[1642]---> BDD-cost:    2
c ---[1641]---> BDD-cost:    2
c ---[1640]---> BDD-cost:    2
c ---[1639]---> BDD-cost:    2
c ---[1638]---> BDD-cost:    2
c ---[1637]---> BDD-cost:    2
c ---[1636]---> BDD-cost:    2
c ---[1635]---> BDD-cost:    2
c ---[1634]---> BDD-cost:    2
c ---[1633]---> BDD-cost:    2
c ---[1632]---> BDD-cost:    2
c ---[1631]---> BDD-cost:    2
c ---[1630]---> BDD-cost:    2
c ---[1629]---> BDD-cost:    2
c ---[1628]---> BDD-cost:    2
c ---[1627]---> BDD-cost:    2
c ---[1626]---> BDD-cost:    2
c ---[1625]---> BDD-cost:    2
c ---[1624]---> BDD-cost:    2
c ---[1623]---> BDD-cost:    2
c ---[1622]---> BDD-cost:    2
c ---[1621]---> BDD-cost:    2
c ---[1620]---> BDD-cost:    2
c ---[1619]---> BDD-cost:    2
c ---[1618]---> BDD-cost:    2
c ---[1617]---> BDD-cost:    2
c ---[1616]---> BDD-cost:    2
c ---[1615]---> BDD-cost:    2
c ---[1614]---> BDD-cost:    2
c ---[1613]---> BDD-cost:    2
c ---[1612]---> BDD-cost:    2
c ---[1611]---> BDD-cost:    2
c ---[1610]---> BDD-cost:    2
c ---[1609]---> BDD-cost:    2
c ---[1608]---> BDD-cost:    2
c ---[1599]---> BDD-cost:    9
c ---[1598]---> BDD-cost:    2
c ---[1597]---> BDD-cost:    9
c ---[1596]---> BDD-cost:    2
c ---[1595]---> BDD-cost:    9
c ---[1594]---> BDD-cost:    2
c ---[1593]---> BDD-cost:    9
c ---[1592]---> BDD-cost:    2
c ---[1591]---> BDD-cost:    8
c ---[1590]---> BDD-cost:    2
c ---[1589]---> BDD-cost:    8
c ---[1588]---> BDD-cost:    2
c ---[1587]---> BDD-cost:    8
c ---[1586]---> BDD-cost:    2
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    2
c ---[1583]---> BDD-cost:    7
c ---[1582]---> BDD-cost:    2
c ---[1581]---> BDD-cost:    7
c ---[1580]---> BDD-cost:    2
c ---[1579]---> BDD-cost:    7
c ---[1578]---> BDD-cost:    2
c ---[1577]---> BDD-cost:    7
c ---[1576]---> BDD-cost:    2
c ---[1575]---> BDD-cost:    6
c ---[1574]---> BDD-cost:    2
c ---[1573]---> BDD-cost:    6
c ---[1572]---> BDD-cost:    2
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    2
c ---[1569]---> BDD-cost:    6
c ---[1568]---> BDD-cost:    2
c ---[1567]---> BDD-cost:    5
c ---[1566]---> BDD-cost:    2
c ---[1565]---> BDD-cost:    5
c ---[1564]---> BDD-cost:    2
c ---[1563]---> BDD-cost:    5
c ---[1562]---> BDD-cost:    2
c ---[1561]---> BDD-cost:    5
c ---[1560]---> BDD-cost:    2
c ---[1559]---> BDD-cost:    4
c ---[1558]---> BDD-cost:    2
c ---[1557]---> BDD-cost:    4
c ---[1556]---> BDD-cost:    2
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    2
c ---[1553]---> BDD-cost:    4
c ---[1552]---> BDD-cost:    2
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    2
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    2
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    2
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    2
c ---[1535]---> BDD-cost:    6
c ---[1534]---> BDD-cost:    2
c ---[1533]---> BDD-cost:    2
c ---[1532]---> BDD-cost:    2
c ---[1531]---> BDD-cost:    2
c ---[1530]---> BDD-cost:    2
c ---[1529]---> BDD-cost:    2
c ---[1528]---> BDD-cost:    2
c ---[1527]---> BDD-cost:    5
c ---[1526]---> BDD-cost:    2
c ---[1525]---> BDD-cost:    2
c ---[1524]---> BDD-cost:    2
c ---[1523]---> BDD-cost:    2
c ---[1522]---> BDD-cost:    2
c ---[1521]---> BDD-cost:    2
c ---[1520]---> BDD-cost:    2
c ---[1519]---> BDD-cost:    4
c ---[1518]---> BDD-cost:    2
c ---[1517]---> BDD-cost:    2
c ---[1516]---> BDD-cost:    2
c ---[1515]---> BDD-cost:    2
c ---[1514]---> BDD-cost:    2
c ---[1513]---> BDD-cost:    2
c ---[1512]---> BDD-cost:    2
c ---[1511]---> BDD-cost:    3
c ---[1510]---> BDD-cost:    2
c ---[1509]---> BDD-cost:    2
c ---[1508]---> BDD-cost:    2
c ---[1507]---> BDD-cost:    2
c ---[1506]---> BDD-cost:    2
c ---[1505]---> BDD-cost:    2
c ---[1504]---> BDD-cost:    2
c ---[1503]---> BDD-cost:    2
c ---[1502]---> BDD-cost:    2
c ---[1501]---> BDD-cost:    2
c ---[1500]---> BDD-cost:    2
c ---[1499]---> BDD-cost:    2
c ---[1498]---> BDD-cost:    2
c ---[1497]---> BDD-cost:    2
c ---[1496]---> BDD-cost:    2
c ---[1495]---> BDD-cost:    4
c ---[1494]---> BDD-cost:    2
c ---[1493]---> BDD-cost:    2
c ---[1492]---> BDD-cost:    2
c ---[1491]---> BDD-cost:    2
c ---[1490]---> BDD-cost:    2
c ---[1489]---> BDD-cost:    2
c ---[1488]---> BDD-cost:    2
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    2
c ---[1485]---> BDD-cost:    2
c ---[1484]---> BDD-cost:    2
c ---[1483]---> BDD-cost:    2
c ---[1482]---> BDD-cost:    2
c ---[1481]---> BDD-cost:    2
c ---[1480]---> BDD-cost:    2
c ---[1471]---> BDD-cost:    2
c ---[1470]---> BDD-cost:    2
c ---[1469]---> BDD-cost:    2
c ---[1468]---> BDD-cost:    2
c ---[1467]---> BDD-cost:    2
c ---[1466]---> BDD-cost:    2
c ---[1465]---> BDD-cost:    2
c ---[1464]---> BDD-cost:    2
c ---[1463]---> BDD-cost:    2
c ---[1462]---> BDD-cost:    2
c ---[1461]---> BDD-cost:    2
c ---[1460]---> BDD-cost:    2
c ---[1459]---> BDD-cost:    2
c ---[1458]---> BDD-cost:    2
c ---[1457]---> BDD-cost:    2
c ---[1456]---> BDD-cost:    2
c ---[1455]---> BDD-cost:    2
c ---[1454]---> BDD-cost:    2
c ---[1453]---> BDD-cost:    2
c ---[1452]---> BDD-cost:    2
c ---[1451]---> BDD-cost:    2
c ---[1450]---> BDD-cost:    2
c ---[1449]---> BDD-cost:    2
c ---[1448]---> BDD-cost:    2
c ---[1447]---> BDD-cost:    2
c ---[1446]---> BDD-cost:    2
c ---[1445]---> BDD-cost:    2
c ---[1444]---> BDD-cost:    2
c ---[1443]---> BDD-cost:    2
c ---[1442]---> BDD-cost:    2
c ---[1441]---> BDD-cost:    2
c ---[1440]---> BDD-cost:    2
c ---[1439]---> BDD-cost:    2
c ---[1438]---> BDD-cost:    2
c ---[1437]---> BDD-cost:    2
c ---[1436]---> BDD-cost:    2
c ---[1435]---> BDD-cost:    2
c ---[1434]---> BDD-cost:    2
c ---[1433]---> BDD-cost:    2
c ---[1432]---> BDD-cost:    2
c ---[1431]---> BDD-cost:    2
c ---[1430]---> BDD-cost:    2
c ---[1429]---> BDD-cost:    2
c ---[1428]---> BDD-cost:    2
c ---[1427]---> BDD-cost:    2
c ---[1426]---> BDD-cost:    2
c ---[1425]---> BDD-cost:    2
c ---[1424]---> BDD-cost:    2
c ---[1423]---> BDD-cost:    2
c ---[1422]---> BDD-cost:    2
c ---[1421]---> BDD-cost:    2
c ---[1420]---> BDD-cost:    2
c ---[1419]---> BDD-cost:    2
c ---[1418]---> BDD-cost:    2
c ---[1417]---> BDD-cost:    2
c ---[1416]---> BDD-cost:    2
c ---[1407]---> BDD-cost:    2
c ---[1406]---> BDD-cost:    2
c ---[1405]---> BDD-cost:    2
c ---[1404]---> BDD-cost:    2
c ---[1403]---> BDD-cost:    2
c ---[1402]---> BDD-cost:    2
c ---[1401]---> BDD-cost:    2
c ---[1400]---> BDD-cost:    2
c ---[1399]---> BDD-cost:    2
c ---[1398]---> BDD-cost:    2
c ---[1397]---> BDD-cost:    2
c ---[1396]---> BDD-cost:    2
c ---[1395]---> BDD-cost:    2
c ---[1394]---> BDD-cost:    2
c ---[1393]---> BDD-cost:    2
c ---[1392]---> BDD-cost:    2
c ---[1391]---> BDD-cost:    2
c ---[1390]---> BDD-cost:    2
c ---[1389]---> BDD-cost:    2
c ---[1388]---> BDD-cost:    2
c ---[1387]---> BDD-cost:    2
c ---[1386]---> BDD-cost:    2
c ---[1385]---> BDD-cost:    2
c ---[1384]---> BDD-cost:    2
c ---[1383]---> BDD-cost:    2
c ---[1382]---> BDD-cost:    2
c ---[1381]---> BDD-cost:    2
c ---[1380]---> BDD-cost:    2
c ---[1379]---> BDD-cost:    2
c ---[1378]---> BDD-cost:    2
c ---[1377]---> BDD-cost:    2
c ---[1376]---> BDD-cost:    2
c ---[1375]---> BDD-cost:    2
c ---[1374]---> BDD-cost:    2
c ---[1373]---> BDD-cost:    2
c ---[1372]---> BDD-cost:    2
c ---[1371]---> BDD-cost:    2
c ---[1370]---> BDD-cost:    2
c ---[1369]---> BDD-cost:    2
c ---[1368]---> BDD-cost:    2
c ---[1367]---> BDD-cost:    2
c ---[1366]---> BDD-cost:    2
c ---[1365]---> BDD-cost:    2
c ---[1364]---> BDD-cost:    2
c ---[1363]---> BDD-cost:    2
c ---[1362]---> BDD-cost:    2
c ---[1361]---> BDD-cost:    2
c ---[1360]---> BDD-cost:    2
c ---[1359]---> BDD-cost:    2
c ---[1358]---> BDD-cost:    2
c ---[1357]---> BDD-cost:    2
c ---[1356]---> BDD-cost:    2
c ---[1355]---> BDD-cost:    2
c ---[1354]---> BDD-cost:    2
c ---[1353]---> BDD-cost:    2
c ---[1352]---> BDD-cost:    2
c ---[1343]---> BDD-cost:    2
c ---[1342]---> BDD-cost:    2
c ---[1341]---> BDD-cost:    2
c ---[1340]---> BDD-cost:    2
c ---[1339]---> BDD-cost:    2
c ---[1338]---> BDD-cost:    2
c ---[1337]---> BDD-cost:    2
c ---[1336]---> BDD-cost:    2
c ---[1335]---> BDD-cost:    2
c ---[1334]---> BDD-cost:    2
c ---[1333]---> BDD-cost:    2
c ---[1332]---> BDD-cost:    2
c ---[1331]---> BDD-cost:    2
c ---[1330]---> BDD-cost:    2
c ---[1329]---> BDD-cost:    2
c ---[1328]---> BDD-cost:    2
c ---[1327]---> BDD-cost:    2
c ---[1326]---> BDD-cost:    2
c ---[1325]---> BDD-cost:    2
c ---[1324]---> BDD-cost:    2
c ---[1323]---> BDD-cost:    2
c ---[1322]---> BDD-cost:    2
c ---[1321]---> BDD-cost:    2
c ---[1320]---> BDD-cost:    2
c ---[1319]---> BDD-cost:    2
c ---[1318]---> BDD-cost:    2
c ---[1317]---> BDD-cost:    2
c ---[1316]---> BDD-cost:    2
c ---[1315]---> BDD-cost:    2
c ---[1314]---> BDD-cost:    2
c ---[1313]---> BDD-cost:    2
c ---[1312]---> BDD-cost:    2
c ---[1311]---> BDD-cost:    2
c ---[1310]---> BDD-cost:    2
c ---[1309]---> BDD-cost:    2
c ---[1308]---> BDD-cost:    2
c ---[1307]---> BDD-cost:    2
c ---[1306]---> BDD-cost:    2
c ---[1305]---> BDD-cost:    2
c ---[1304]---> BDD-cost:    2
c ---[1303]---> BDD-cost:    2
c ---[1302]---> BDD-cost:    2
c ---[1301]---> BDD-cost:    2
c ---[1300]---> BDD-cost:    2
c ---[1299]---> BDD-cost:    2
c ---[1298]---> BDD-cost:    2
c ---[1297]---> BDD-cost:    2
c ---[1296]---> BDD-cost:    2
c ---[1295]---> BDD-cost:    2
c ---[1294]---> BDD-cost:    2
c ---[1293]---> BDD-cost:    2
c ---[1292]---> BDD-cost:    2
c ---[1291]---> BDD-cost:    2
c ---[1290]---> BDD-cost:    2
c ---[1289]---> BDD-cost:    2
c ---[1288]---> BDD-cost:    2
c ---[1279]---> BDD-cost:    9
c ---[1278]---> BDD-cost:    2
c ---[1277]---> BDD-cost:    9
c ---[1276]---> BDD-cost:    2
c ---[1275]---> BDD-cost:    9
c ---[1274]---> BDD-cost:    2
c ---[1273]---> BDD-cost:    9
c ---[1272]---> BDD-cost:    2
c ---[1271]---> BDD-cost:    8
c ---[1270]---> BDD-cost:    2
c ---[1269]---> BDD-cost:    8
c ---[1268]---> BDD-cost:    2
c ---[1267]---> BDD-cost:    8
c ---[1266]---> BDD-cost:    2
c ---[1265]---> BDD-cost:    8
c ---[1264]---> BDD-cost:    2
c ---[1263]---> BDD-cost:    7
c ---[1262]---> BDD-cost:    2
c ---[1261]---> BDD-cost:    7
c ---[1260]---> BDD-cost:    2
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    2
c ---[1257]---> BDD-cost:    7
c ---[1256]---> BDD-cost:    2
c ---[1255]---> BDD-cost:    6
c ---[1254]---> BDD-cost:    2
c ---[1253]---> BDD-cost:    6
c ---[1252]---> BDD-cost:    2
c ---[1251]---> BDD-cost:    6
c ---[1250]---> BDD-cost:    2
c ---[1249]---> BDD-cost:    6
c ---[1248]---> BDD-cost:    2
c ---[1247]---> BDD-cost:    5
c ---[1246]---> BDD-cost:    2
c ---[1245]---> BDD-cost:    5
c ---[1244]---> BDD-cost:    2
c ---[1243]---> BDD-cost:    5
c ---[1242]---> BDD-cost:    2
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    2
c ---[1239]---> BDD-cost:    4
c ---[1238]---> BDD-cost:    2
c ---[1237]---> BDD-cost:    4
c ---[1236]---> BDD-cost:    2
c ---[1235]---> BDD-cost:    4
c ---[1234]---> BDD-cost:    2
c ---[1233]---> BDD-cost:    4
c ---[1232]---> BDD-cost:    2
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    2
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    2
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    2
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    2
c ---[1215]---> BDD-cost:    6
c ---[1214]---> BDD-cost:    2
c ---[1213]---> BDD-cost:    2
c ---[1212]---> BDD-cost:    2
c ---[1211]---> BDD-cost:    2
c ---[1210]---> BDD-cost:    2
c ---[1209]---> BDD-cost:    2
c ---[1208]---> BDD-cost:    2
c ---[1207]---> BDD-cost:    5
c ---[1206]---> BDD-cost:    2
c ---[1205]---> BDD-cost:    2
c ---[1204]---> BDD-cost:    2
c ---[1203]---> BDD-cost:    2
c ---[1202]---> BDD-cost:    2
c ---[1201]---> BDD-cost:    2
c ---[1200]---> BDD-cost:    2
c ---[1199]---> BDD-cost:    4
c ---[1198]---> BDD-cost:    2
c ---[1197]---> BDD-cost:    2
c ---[1196]---> BDD-cost:    2
c ---[1195]---> BDD-cost:    2
c ---[1194]---> BDD-cost:    2
c ---[1193]---> BDD-cost:    2
c ---[1192]---> BDD-cost:    2
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    2
c ---[1189]---> BDD-cost:    2
c ---[1188]---> BDD-cost:    2
c ---[1187]---> BDD-cost:    2
c ---[1186]---> BDD-cost:    2
c ---[1185]---> BDD-cost:    2
c ---[1184]---> BDD-cost:    2
c ---[1183]---> BDD-cost:    2
c ---[1182]---> BDD-cost:    2
c ---[1181]---> BDD-cost:    2
c ---[1180]---> BDD-cost:    2
c ---[1179]---> BDD-cost:    2
c ---[1178]---> BDD-cost:    2
c ---[1177]---> BDD-cost:    2
c ---[1176]---> BDD-cost:    2
c ---[1175]---> BDD-cost:    4
c ---[1174]---> BDD-cost:    2
c ---[1173]---> BDD-cost:    2
c ---[1172]---> BDD-cost:    2
c ---[1171]---> BDD-cost:    2
c ---[1170]---> BDD-cost:    2
c ---[1169]---> BDD-cost:    2
c ---[1168]---> BDD-cost:    2
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    2
c ---[1165]---> BDD-cost:    2
c ---[1164]---> BDD-cost:    2
c ---[1163]---> BDD-cost:    2
c ---[1162]---> BDD-cost:    2
c ---[1161]---> BDD-cost:    2
c ---[1160]---> BDD-cost:    2
c ---[1151]---> BDD-cost:    2
c ---[1150]---> BDD-cost:    2
c ---[1149]---> BDD-cost:    2
c ---[1148]---> BDD-cost:    2
c ---[1147]---> BDD-cost:    2
c ---[1146]---> BDD-cost:    2
c ---[1145]---> BDD-cost:    2
c ---[1144]---> BDD-cost:    2
c ---[1143]---> BDD-cost:    2
c ---[1142]---> BDD-cost:    2
c ---[1141]---> BDD-cost:    2
c ---[1140]---> BDD-cost:    2
c ---[1139]---> BDD-cost:    2
c ---[1138]---> BDD-cost:    2
c ---[1137]---> BDD-cost:    2
c ---[1136]---> BDD-cost:    2
c ---[1135]---> BDD-cost:    2
c ---[1134]---> BDD-cost:    2
c ---[1133]---> BDD-cost:    2
c ---[1132]---> BDD-cost:    2
c ---[1131]---> BDD-cost:    2
c ---[1130]---> BDD-cost:    2
c ---[1129]---> BDD-cost:    2
c ---[1128]---> BDD-cost:    2
c ---[1127]---> BDD-cost:    2
c ---[1126]---> BDD-cost:    2
c ---[1125]---> BDD-cost:    2
c ---[1124]---> BDD-cost:    2
c ---[1123]---> BDD-cost:    2
c ---[1122]---> BDD-cost:    2
c ---[1121]---> BDD-cost:    2
c ---[1120]---> BDD-cost:    2
c ---[1119]---> BDD-cost:    2
c ---[1118]---> BDD-cost:    2
c ---[1117]---> BDD-cost:    2
c ---[1116]---> BDD-cost:    2
c ---[1115]---> BDD-cost:    2
c ---[1114]---> BDD-cost:    2
c ---[1113]---> BDD-cost:    2
c ---[1112]---> BDD-cost:    2
c ---[1111]---> BDD-cost:    2
c ---[1110]---> BDD-cost:    2
c ---[1109]---> BDD-cost:    2
c ---[1108]---> BDD-cost:    2
c ---[1107]---> BDD-cost:    2
c ---[1106]---> BDD-cost:    2
c ---[1105]---> BDD-cost:    2
c ---[1104]---> BDD-cost:    2
c ---[1103]---> BDD-cost:    2
c ---[1102]---> BDD-cost:    2
c ---[1101]---> BDD-cost:    2
c ---[1100]---> BDD-cost:    2
c ---[1099]---> BDD-cost:    2
c ---[1098]---> BDD-cost:    2
c ---[1097]---> BDD-cost:    2
c ---[1096]---> BDD-cost:    2
c ---[1087]---> BDD-cost:    2
c ---[1086]---> BDD-cost:    2
c ---[1085]---> BDD-cost:    2
c ---[1084]---> BDD-cost:    2
c ---[1083]---> BDD-cost:    2
c ---[1082]---> BDD-cost:    2
c ---[1081]---> BDD-cost:    2
c ---[1080]---> BDD-cost:    2
c ---[1079]---> BDD-cost:    2
c ---[1078]---> BDD-cost:    2
c ---[1077]---> BDD-cost:    2
c ---[1076]---> BDD-cost:    2
c ---[1075]---> BDD-cost:    2
c ---[1074]---> BDD-cost:    2
c ---[1073]---> BDD-cost:    2
c ---[1072]---> BDD-cost:    2
c ---[1071]---> BDD-cost:    2
c ---[1070]---> BDD-cost:    2
c ---[1069]---> BDD-cost:    2
c ---[1068]---> BDD-cost:    2
c ---[1067]---> BDD-cost:    2
c ---[1066]---> BDD-cost:    2
c ---[1065]---> BDD-cost:    2
c ---[1064]---> BDD-cost:    2
c ---[1063]---> BDD-cost:    2
c ---[1062]---> BDD-cost:    2
c ---[1061]---> BDD-cost:    2
c ---[1060]---> BDD-cost:    2
c ---[1059]---> BDD-cost:    2
c ---[1058]---> BDD-cost:    2
c ---[1057]---> BDD-cost:    2
c ---[1056]---> BDD-cost:    2
c ---[1055]---> BDD-cost:    2
c ---[1054]---> BDD-cost:    2
c ---[1053]---> BDD-cost:    2
c ---[1052]---> BDD-cost:    2
c ---[1051]---> BDD-cost:    2
c ---[1050]---> BDD-cost:    2
c ---[1049]---> BDD-cost:    2
c ---[1048]---> BDD-cost:    2
c ---[1047]---> BDD-cost:    2
c ---[1046]---> BDD-cost:    2
c ---[1045]---> BDD-cost:    2
c ---[1044]---> BDD-cost:    2
c ---[1043]---> BDD-cost:    2
c ---[1042]---> BDD-cost:    2
c ---[1041]---> BDD-cost:    2
c ---[1040]---> BDD-cost:    2
c ---[1039]---> BDD-cost:    2
c ---[1038]---> BDD-cost:    2
c ---[1037]---> BDD-cost:    2
c ---[1036]---> BDD-cost:    2
c ---[1035]---> BDD-cost:    2
c ---[1034]---> BDD-cost:    2
c ---[1033]---> BDD-cost:    2
c ---[1032]---> BDD-cost:    2
c ---[1023]---> BDD-cost:    2
c ---[1022]---> BDD-cost:    2
c ---[1021]---> BDD-cost:    2
c ---[1020]---> BDD-cost:    2
c ---[1019]---> BDD-cost:    2
c ---[1018]---> BDD-cost:    2
c ---[1017]---> BDD-cost:    2
c ---[1016]---> BDD-cost:    2
c ---[1015]---> BDD-cost:    2
c ---[1014]---> BDD-cost:    2
c ---[1013]---> BDD-cost:    2
c ---[1012]---> BDD-cost:    2
c ---[1011]---> BDD-cost:    2
c ---[1010]---> BDD-cost:    2
c ---[1009]---> BDD-cost:    2
c ---[1008]---> BDD-cost:    2
c ---[1007]---> BDD-cost:    2
c ---[1006]---> BDD-cost:    2
c ---[1005]---> BDD-cost:    2
c ---[1004]---> BDD-cost:    2
c ---[1003]---> BDD-cost:    2
c ---[1002]---> BDD-cost:    2
c ---[1001]---> BDD-cost:    2
c ---[1000]---> BDD-cost:    2
c ---[ 999]---> BDD-cost:    2
c ---[ 998]---> BDD-cost:    2
c ---[ 997]---> BDD-cost:    2
c ---[ 996]---> BDD-cost:    2
c ---[ 995]---> BDD-cost:    2
c ---[ 994]---> BDD-cost:    2
c ---[ 993]---> BDD-cost:    2
c ---[ 992]---> BDD-cost:    2
c ---[ 991]---> BDD-cost:    2
c ---[ 990]---> BDD-cost:    2
c ---[ 989]---> BDD-cost:    2
c ---[ 988]---> BDD-cost:    2
c ---[ 987]---> BDD-cost:    2
c ---[ 986]---> BDD-cost:    2
c ---[ 985]---> BDD-cost:    2
c ---[ 984]---> BDD-cost:    2
c ---[ 983]---> BDD-cost:    2
c ---[ 982]---> BDD-cost:    2
c ---[ 981]---> BDD-cost:    2
c ---[ 980]---> BDD-cost:    2
c ---[ 979]---> BDD-cost:    2
c ---[ 978]---> BDD-cost:    2
c ---[ 977]---> BDD-cost:    2
c ---[ 976]---> BDD-cost:    2
c ---[ 975]---> BDD-cost:    2
c ---[ 974]---> BDD-cost:    2
c ---[ 973]---> BDD-cost:    2
c ---[ 972]---> BDD-cost:    2
c ---[ 971]---> BDD-cost:    2
c ---[ 970]---> BDD-cost:    2
c ---[ 969]---> BDD-cost:    2
c ---[ 968]---> BDD-cost:    2
c ---[ 959]---> BDD-cost:    9
c ---[ 958]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    9
c ---[ 956]---> BDD-cost:    2
c ---[ 955]---> BDD-cost:    9
c ---[ 954]---> BDD-cost:    2
c ---[ 953]---> BDD-cost:    9
c ---[ 952]---> BDD-cost:    2
c ---[ 951]---> BDD-cost:    8
c ---[ 950]---> BDD-cost:    2
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    2
c ---[ 947]---> BDD-cost:    8
c ---[ 946]---> BDD-cost:    2
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    2
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    2
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    2
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    2
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    2
c ---[ 935]---> BDD-cost:    6
c ---[ 934]---> BDD-cost:    2
c ---[ 933]---> BDD-cost:    6
c ---[ 932]---> BDD-cost:    2
c ---[ 931]---> BDD-cost:    6
c ---[ 930]---> BDD-cost:    2
c ---[ 929]---> BDD-cost:    6
c ---[ 928]---> BDD-cost:    2
c ---[ 927]---> BDD-cost:    5
c ---[ 926]---> BDD-cost:    2
c ---[ 925]---> BDD-cost:    5
c ---[ 924]---> BDD-cost:    2
c ---[ 923]---> BDD-cost:    5
c ---[ 922]---> BDD-cost:    2
c ---[ 921]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:    2
c ---[ 919]---> BDD-cost:    4
c ---[ 918]---> BDD-cost:    2
c ---[ 917]---> BDD-cost:    4
c ---[ 916]---> BDD-cost:    2
c ---[ 915]---> BDD-cost:    4
c ---[ 914]---> BDD-cost:    2
c ---[ 913]---> BDD-cost:    4
c ---[ 912]---> BDD-cost:    2
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    2
c ---[ 909]---> BDD-cost:    3
c ---[ 908]---> BDD-cost:    2
c ---[ 907]---> BDD-cost:    3
c ---[ 906]---> BDD-cost:    2
c ---[ 905]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    2
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    2
c ---[ 893]---> BDD-cost:    2
c ---[ 892]---> BDD-cost:    2
c ---[ 891]---> BDD-cost:    2
c ---[ 890]---> BDD-cost:    2
c ---[ 889]---> BDD-cost:    2
c ---[ 888]---> BDD-cost:    2
c ---[ 887]---> BDD-cost:    5
c ---[ 886]---> BDD-cost:    2
c ---[ 885]---> BDD-cost:    2
c ---[ 884]---> BDD-cost:    2
c ---[ 883]---> BDD-cost:    2
c ---[ 882]---> BDD-cost:    2
c ---[ 881]---> BDD-cost:    2
c ---[ 880]---> BDD-cost:    2
c ---[ 879]---> BDD-cost:    4
c ---[ 878]---> BDD-cost:    2
c ---[ 877]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    2
c ---[ 875]---> BDD-cost:    2
c ---[ 874]---> BDD-cost:    2
c ---[ 873]---> BDD-cost:    2
c ---[ 872]---> BDD-cost:    2
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    2
c ---[ 869]---> BDD-cost:    2
c ---[ 868]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 866]---> BDD-cost:    2
c ---[ 865]---> BDD-cost:    2
c ---[ 864]---> BDD-cost:    2
c ---[ 863]---> BDD-cost:    2
c ---[ 862]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 859]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    2
c ---[ 857]---> BDD-cost:    2
c ---[ 856]---> BDD-cost:    2
c ---[ 855]---> BDD-cost:    4
c ---[ 854]---> BDD-cost:    2
c ---[ 853]---> BDD-cost:    2
c ---[ 852]---> BDD-cost:    2
c ---[ 851]---> BDD-cost:    2
c ---[ 850]---> BDD-cost:    2
c ---[ 849]---> BDD-cost:    2
c ---[ 848]---> BDD-cost:    2
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 844]---> BDD-cost:    2
c ---[ 843]---> BDD-cost:    2
c ---[ 842]---> BDD-cost:    2
c ---[ 841]---> BDD-cost:    2
c ---[ 840]---> BDD-cost:    2
c ---[ 831]---> BDD-cost:    2
c ---[ 830]---> BDD-cost:    2
c ---[ 829]---> BDD-cost:    2
c ---[ 828]---> BDD-cost:    2
c ---[ 827]---> BDD-cost:    2
c ---[ 826]---> BDD-cost:    2
c ---[ 825]---> BDD-cost:    2
c ---[ 824]---> BDD-cost:    2
c ---[ 823]---> BDD-cost:    2
c ---[ 822]---> BDD-cost:    2
c ---[ 821]---> BDD-cost:    2
c ---[ 820]---> BDD-cost:    2
c ---[ 819]---> BDD-cost:    2
c ---[ 818]---> BDD-cost:    2
c ---[ 817]---> BDD-cost:    2
c ---[ 816]---> BDD-cost:    2
c ---[ 815]---> BDD-cost:    2
c ---[ 814]---> BDD-cost:    2
c ---[ 813]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 811]---> BDD-cost:    2
c ---[ 810]---> BDD-cost:    2
c ---[ 809]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    2
c ---[ 807]---> BDD-cost:    2
c ---[ 806]---> BDD-cost:    2
c ---[ 805]---> BDD-cost:    2
c ---[ 804]---> BDD-cost:    2
c ---[ 803]---> BDD-cost:    2
c ---[ 802]---> BDD-cost:    2
c ---[ 801]---> BDD-cost:    2
c ---[ 800]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 798]---> BDD-cost:    2
c ---[ 797]---> BDD-cost:    2
c ---[ 796]---> BDD-cost:    2
c ---[ 795]---> BDD-cost:    2
c ---[ 794]---> BDD-cost:    2
c ---[ 793]---> BDD-cost:    2
c ---[ 792]---> BDD-cost:    2
c ---[ 791]---> BDD-cost:    2
c ---[ 790]---> BDD-cost:    2
c ---[ 789]---> BDD-cost:    2
c ---[ 788]---> BDD-cost:    2
c ---[ 787]---> BDD-cost:    2
c ---[ 786]---> BDD-cost:    2
c ---[ 785]---> BDD-cost:    2
c ---[ 784]---> BDD-cost:    2
c ---[ 783]---> BDD-cost:    2
c ---[ 782]---> BDD-cost:    2
c ---[ 781]---> BDD-cost:    2
c ---[ 780]---> BDD-cost:    2
c ---[ 779]---> BDD-cost:    2
c ---[ 778]---> BDD-cost:    2
c ---[ 777]---> BDD-cost:    2
c ---[ 776]---> BDD-cost:    2
c ---[ 767]---> BDD-cost:    2
c ---[ 766]---> BDD-cost:    2
c ---[ 765]---> BDD-cost:    2
c ---[ 764]---> BDD-cost:    2
c ---[ 763]---> BDD-cost:    2
c ---[ 762]---> BDD-cost:    2
c ---[ 761]---> BDD-cost:    2
c ---[ 760]---> BDD-cost:    2
c ---[ 759]---> BDD-cost:    2
c ---[ 758]---> BDD-cost:    2
c ---[ 757]---> BDD-cost:    2
c ---[ 756]---> BDD-cost:    2
c ---[ 755]---> BDD-cost:    2
c ---[ 754]---> BDD-cost:    2
c ---[ 753]---> BDD-cost:    2
c ---[ 752]---> BDD-cost:    2
c ---[ 751]---> BDD-cost:    2
c ---[ 750]---> BDD-cost:    2
c ---[ 749]---> BDD-cost:    2
c ---[ 748]---> BDD-cost:    2
c ---[ 747]---> BDD-cost:    2
c ---[ 746]---> BDD-cost:    2
c ---[ 745]---> BDD-cost:    2
c ---[ 744]---> BDD-cost:    2
c ---[ 743]---> BDD-cost:    2
c ---[ 742]---> BDD-cost:    2
c ---[ 741]---> BDD-cost:    2
c ---[ 740]---> BDD-cost:    2
c ---[ 739]---> BDD-cost:    2
c ---[ 738]---> BDD-cost:    2
c ---[ 737]---> BDD-cost:    2
c ---[ 736]---> BDD-cost:    2
c ---[ 735]---> BDD-cost:    2
c ---[ 734]---> BDD-cost:    2
c ---[ 733]---> BDD-cost:    2
c ---[ 732]---> BDD-cost:    2
c ---[ 731]---> BDD-cost:    2
c ---[ 730]---> BDD-cost:    2
c ---[ 729]---> BDD-cost:    2
c ---[ 728]---> BDD-cost:    2
c ---[ 727]---> BDD-cost:    2
c ---[ 726]---> BDD-cost:    2
c ---[ 725]---> BDD-cost:    2
c ---[ 724]---> BDD-cost:    2
c ---[ 723]---> BDD-cost:    2
c ---[ 722]---> BDD-cost:    2
c ---[ 721]---> BDD-cost:    2
c ---[ 720]---> BDD-cost:    2
c ---[ 719]---> BDD-cost:    2
c ---[ 718]---> BDD-cost:    2
c ---[ 717]---> BDD-cost:    2
c ---[ 716]---> BDD-cost:    2
c ---[ 715]---> BDD-cost:    2
c ---[ 714]---> BDD-cost:    2
c ---[ 713]---> BDD-cost:    2
c ---[ 712]---> BDD-cost:    2
c ---[ 703]---> BDD-cost:    2
c ---[ 702]---> BDD-cost:    2
c ---[ 701]---> BDD-cost:    2
c ---[ 700]---> BDD-cost:    2
c ---[ 699]---> BDD-cost:    2
c ---[ 698]---> BDD-cost:    2
c ---[ 697]---> BDD-cost:    2
c ---[ 696]---> BDD-cost:    2
c ---[ 695]---> BDD-cost:    2
c ---[ 694]---> BDD-cost:    2
c ---[ 693]---> BDD-cost:    2
c ---[ 692]---> BDD-cost:    2
c ---[ 691]---> BDD-cost:    2
c ---[ 690]---> BDD-cost:    2
c ---[ 689]---> BDD-cost:    2
c ---[ 688]---> BDD-cost:    2
c ---[ 687]---> BDD-cost:    2
c ---[ 686]---> BDD-cost:    2
c ---[ 685]---> BDD-cost:    2
c ---[ 684]---> BDD-cost:    2
c ---[ 683]---> BDD-cost:    2
c ---[ 682]---> BDD-cost:    2
c ---[ 681]---> BDD-cost:    2
c ---[ 680]---> BDD-cost:    2
c ---[ 679]---> BDD-cost:    2
c ---[ 678]---> BDD-cost:    2
c ---[ 677]---> BDD-cost:    2
c ---[ 676]---> BDD-cost:    2
c ---[ 675]---> BDD-cost:    2
c ---[ 674]---> BDD-cost:    2
c ---[ 673]---> BDD-cost:    2
c ---[ 672]---> BDD-cost:    2
c ---[ 671]---> BDD-cost:    2
c ---[ 670]---> BDD-cost:    2
c ---[ 669]---> BDD-cost:    2
c ---[ 668]---> BDD-cost:    2
c ---[ 667]---> BDD-cost:    2
c ---[ 666]---> BDD-cost:    2
c ---[ 665]---> BDD-cost:    2
c ---[ 664]---> BDD-cost:    2
c ---[ 663]---> BDD-cost:    2
c ---[ 662]---> BDD-cost:    2
c ---[ 661]---> BDD-cost:    2
c ---[ 660]---> BDD-cost:    2
c ---[ 659]---> BDD-cost:    2
c ---[ 658]---> BDD-cost:    2
c ---[ 657]---> BDD-cost:    2
c ---[ 656]---> BDD-cost:    2
c ---[ 655]---> BDD-cost:    2
c ---[ 654]---> BDD-cost:    2
c ---[ 653]---> BDD-cost:    2
c ---[ 652]---> BDD-cost:    2
c ---[ 651]---> BDD-cost:    2
c ---[ 650]---> BDD-cost:    2
c ---[ 649]---> BDD-cost:    2
c ---[ 648]---> BDD-cost:    2
c ---[ 639]---> BDD-cost:    9
c ---[ 638]---> BDD-cost:    2
c ---[ 637]---> BDD-cost:    9
c ---[ 636]---> BDD-cost:    2
c ---[ 635]---> BDD-cost:    9
c ---[ 634]---> BDD-cost:    2
c ---[ 633]---> BDD-cost:    9
c ---[ 632]---> BDD-cost:    2
c ---[ 631]---> BDD-cost:    8
c ---[ 630]---> BDD-cost:    2
c ---[ 629]---> BDD-cost:    8
c ---[ 628]---> BDD-cost:    2
c ---[ 627]---> BDD-cost:    8
c ---[ 626]---> BDD-cost:    2
c ---[ 625]---> BDD-cost:    8
c ---[ 624]---> BDD-cost:    2
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    2
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    2
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    2
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    2
c ---[ 615]---> BDD-cost:    6
c ---[ 614]---> BDD-cost:    2
c ---[ 613]---> BDD-cost:    6
c ---[ 612]---> BDD-cost:    2
c ---[ 611]---> BDD-cost:    6
c ---[ 610]---> BDD-cost:    2
c ---[ 609]---> BDD-cost:    6
c ---[ 608]---> BDD-cost:    2
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:    2
c ---[ 605]---> BDD-cost:    5
c ---[ 604]---> BDD-cost:    2
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    2
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost:    2
c ---[ 599]---> BDD-cost:    4
c ---[ 598]---> BDD-cost:    2
c ---[ 597]---> BDD-cost:    4
c ---[ 596]---> BDD-cost:    2
c ---[ 595]---> BDD-cost:    4
c ---[ 594]---> BDD-cost:    2
c ---[ 593]---> BDD-cost:    4
c ---[ 592]---> BDD-cost:    2
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    2
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    2
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    2
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    2
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    2
c ---[ 573]---> BDD-cost:    2
c ---[ 572]---> BDD-cost:    2
c ---[ 571]---> BDD-cost:    2
c ---[ 570]---> BDD-cost:    2
c ---[ 569]---> BDD-cost:    2
c ---[ 568]---> BDD-cost:    2
c ---[ 567]---> BDD-cost:    5
c ---[ 566]---> BDD-cost:    2
c ---[ 565]---> BDD-cost:    2
c ---[ 564]---> BDD-cost:    2
c ---[ 563]---> BDD-cost:    2
c ---[ 562]---> BDD-cost:    2
c ---[ 561]---> BDD-cost:    2
c ---[ 560]---> BDD-cost:    2
c ---[ 559]---> BDD-cost:    4
c ---[ 558]---> BDD-cost:    2
c ---[ 557]---> BDD-cost:    2
c ---[ 556]---> BDD-cost:    2
c ---[ 555]---> BDD-cost:    2
c ---[ 554]---> BDD-cost:    2
c ---[ 553]---> BDD-cost:    2
c ---[ 552]---> BDD-cost:    2
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    2
c ---[ 549]---> BDD-cost:    2
c ---[ 548]---> BDD-cost:    2
c ---[ 547]---> BDD-cost:    2
c ---[ 546]---> BDD-cost:    2
c ---[ 545]---> BDD-cost:    2
c ---[ 544]---> BDD-cost:    2
c ---[ 543]---> BDD-cost:    2
c ---[ 542]---> BDD-cost:    2
c ---[ 541]---> BDD-cost:    2
c ---[ 540]---> BDD-cost:    2
c ---[ 539]---> BDD-cost:    2
c ---[ 538]---> BDD-cost:    2
c ---[ 537]---> BDD-cost:    2
c ---[ 536]---> BDD-cost:    2
c ---[ 535]---> BDD-cost:    4
c ---[ 534]---> BDD-cost:    2
c ---[ 533]---> BDD-cost:    2
c ---[ 532]---> BDD-cost:    2
c ---[ 531]---> BDD-cost:    2
c ---[ 530]---> BDD-cost:    2
c ---[ 529]---> BDD-cost:    2
c ---[ 528]---> BDD-cost:    2
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    2
c ---[ 525]---> BDD-cost:    2
c ---[ 524]---> BDD-cost:    2
c ---[ 523]---> BDD-cost:    2
c ---[ 522]---> BDD-cost:    2
c ---[ 521]---> BDD-cost:    2
c ---[ 520]---> BDD-cost:    2
c ---[ 511]---> BDD-cost:    2
c ---[ 510]---> BDD-cost:    2
c ---[ 509]---> BDD-cost:    2
c ---[ 508]---> BDD-cost:    2
c ---[ 507]---> BDD-cost:    2
c ---[ 506]---> BDD-cost:    2
c ---[ 505]---> BDD-cost:    2
c ---[ 504]---> BDD-cost:    2
c ---[ 503]---> BDD-cost:    2
c ---[ 502]---> BDD-cost:    2
c ---[ 501]---> BDD-cost:    2
c ---[ 500]---> BDD-cost:    2
c ---[ 499]---> BDD-cost:    2
c ---[ 498]---> BDD-cost:    2
c ---[ 497]---> BDD-cost:    2
c ---[ 496]---> BDD-cost:    2
c ---[ 495]---> BDD-cost:    2
c ---[ 494]---> BDD-cost:    2
c ---[ 493]---> BDD-cost:    2
c ---[ 492]---> BDD-cost:    2
c ---[ 491]---> BDD-cost:    2
c ---[ 490]---> BDD-cost:    2
c ---[ 489]---> BDD-cost:    2
c ---[ 488]---> BDD-cost:    2
c ---[ 487]---> BDD-cost:    2
c ---[ 486]---> BDD-cost:    2
c ---[ 485]---> BDD-cost:    2
c ---[ 484]---> BDD-cost:    2
c ---[ 483]---> BDD-cost:    2
c ---[ 482]---> BDD-cost:    2
c ---[ 481]---> BDD-cost:    2
c ---[ 480]---> BDD-cost:    2
c ---[ 479]---> BDD-cost:    2
c ---[ 478]---> BDD-cost:    2
c ---[ 477]---> BDD-cost:    2
c ---[ 476]---> BDD-cost:    2
c ---[ 475]---> BDD-cost:    2
c ---[ 474]---> BDD-cost:    2
c ---[ 473]---> BDD-cost:    2
c ---[ 472]---> BDD-cost:    2
c ---[ 471]---> BDD-cost:    2
c ---[ 470]---> BDD-cost:    2
c ---[ 469]---> BDD-cost:    2
c ---[ 468]---> BDD-cost:    2
c ---[ 467]---> BDD-cost:    2
c ---[ 466]---> BDD-cost:    2
c ---[ 465]---> BDD-cost:    2
c ---[ 464]---> BDD-cost:    2
c ---[ 463]---> BDD-cost:    2
c ---[ 462]---> BDD-cost:    2
c ---[ 461]---> BDD-cost:    2
c ---[ 460]---> BDD-cost:    2
c ---[ 459]---> BDD-cost:    2
c ---[ 458]---> BDD-cost:    2
c ---[ 457]---> BDD-cost:    2
c ---[ 456]---> BDD-cost:    2
c ---[ 447]---> BDD-cost:    2
c ---[ 446]---> BDD-cost:    2
c ---[ 445]---> BDD-cost:    2
c ---[ 444]---> BDD-cost:    2
c ---[ 443]---> BDD-cost:    2
c ---[ 442]---> BDD-cost:    2
c ---[ 441]---> BDD-cost:    2
c ---[ 440]---> BDD-cost:    2
c ---[ 439]---> BDD-cost:    2
c ---[ 438]---> BDD-cost:    2
c ---[ 437]---> BDD-cost:    2
c ---[ 436]---> BDD-cost:    2
c ---[ 435]---> BDD-cost:    2
c ---[ 434]---> BDD-cost:    2
c ---[ 433]---> BDD-cost:    2
c ---[ 432]---> BDD-cost:    2
c ---[ 431]---> BDD-cost:    2
c ---[ 430]---> BDD-cost:    2
c ---[ 429]---> BDD-cost:    2
c ---[ 428]---> BDD-cost:    2
c ---[ 427]---> BDD-cost:    2
c ---[ 426]---> BDD-cost:    2
c ---[ 425]---> BDD-cost:    2
c ---[ 424]---> BDD-cost:    2
c ---[ 423]---> BDD-cost:    2
c ---[ 422]---> BDD-cost:    2
c ---[ 421]---> BDD-cost:    2
c ---[ 420]---> BDD-cost:    2
c ---[ 419]---> BDD-cost:    2
c ---[ 418]---> BDD-cost:    2
c ---[ 417]---> BDD-cost:    2
c ---[ 416]---> BDD-cost:    2
c ---[ 415]---> BDD-cost:    2
c ---[ 414]---> BDD-cost:    2
c ---[ 413]---> BDD-cost:    2
c ---[ 412]---> BDD-cost:    2
c ---[ 411]---> BDD-cost:    2
c ---[ 410]---> BDD-cost:    2
c ---[ 409]---> BDD-cost:    2
c ---[ 408]---> BDD-cost:    2
c ---[ 407]---> BDD-cost:    2
c ---[ 406]---> BDD-cost:    2
c ---[ 405]---> BDD-cost:    2
c ---[ 404]---> BDD-cost:    2
c ---[ 403]---> BDD-cost:    2
c ---[ 402]---> BDD-cost:    2
c ---[ 401]---> BDD-cost:    2
c ---[ 400]---> BDD-cost:    2
c ---[ 399]---> BDD-cost:    2
c ---[ 398]---> BDD-cost:    2
c ---[ 397]---> BDD-cost:    2
c ---[ 396]---> BDD-cost:    2
c ---[ 395]---> BDD-cost:    2
c ---[ 394]---> BDD-cost:    2
c ---[ 393]---> BDD-cost:    2
c ---[ 392]---> BDD-cost:    2
c ---[ 383]---> BDD-cost:    2
c ---[ 382]---> BDD-cost:    2
c ---[ 381]---> BDD-cost:    2
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:    2
c ---[ 378]---> BDD-cost:    2
c ---[ 377]---> BDD-cost:    2
c ---[ 376]---> BDD-cost:    2
c ---[ 375]---> BDD-cost:    2
c ---[ 374]---> BDD-cost:    2
c ---[ 373]---> BDD-cost:    2
c ---[ 372]---> BDD-cost:    2
c ---[ 371]---> BDD-cost:    2
c ---[ 370]---> BDD-cost:    2
c ---[ 369]---> BDD-cost:    2
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:    2
c ---[ 366]---> BDD-cost:    2
c ---[ 365]---> BDD-cost:    2
c ---[ 364]---> BDD-cost:    2
c ---[ 363]---> BDD-cost:    2
c ---[ 362]---> BDD-cost:    2
c ---[ 361]---> BDD-cost:    2
c ---[ 360]---> BDD-cost:    2
c ---[ 359]---> BDD-cost:    2
c ---[ 358]---> BDD-cost:    2
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:    2
c ---[ 355]---> BDD-cost:    2
c ---[ 354]---> BDD-cost:    2
c ---[ 353]---> BDD-cost:    2
c ---[ 352]---> BDD-cost:    2
c ---[ 351]---> BDD-cost:    2
c ---[ 350]---> BDD-cost:    2
c ---[ 349]---> BDD-cost:    2
c ---[ 348]---> BDD-cost:    2
c ---[ 347]---> BDD-cost:    2
c ---[ 346]---> BDD-cost:    2
c ---[ 345]---> BDD-cost:    2
c ---[ 344]---> BDD-cost:    2
c ---[ 343]---> BDD-cost:    2
c ---[ 342]---> BDD-cost:    2
c ---[ 341]---> BDD-cost:    2
c ---[ 340]---> BDD-cost:    2
c ---[ 339]---> BDD-cost:    2
c ---[ 338]---> BDD-cost:    2
c ---[ 337]---> BDD-cost:    2
c ---[ 336]---> BDD-cost:    2
c ---[ 335]---> BDD-cost:    2
c ---[ 334]---> BDD-cost:    2
c ---[ 333]---> BDD-cost:    2
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    2
c ---[ 330]---> BDD-cost:    2
c ---[ 329]---> BDD-cost:    2
c ---[ 328]---> BDD-cost:    2
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    2
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    2
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    2
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    2
c ---[ 311]---> BDD-cost:    8
c ---[ 310]---> BDD-cost:    2
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    2
c ---[ 307]---> BDD-cost:    8
c ---[ 306]---> BDD-cost:    2
c ---[ 305]---> BDD-cost:    8
c ---[ 304]---> BDD-cost:    2
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    2
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    2
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    2
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    2
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    2
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    2
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    2
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    2
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:    2
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:    2
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    2
c ---[ 281]---> BDD-cost:    5
c ---[ 280]---> BDD-cost:    2
c ---[ 279]---> BDD-cost:    4
c ---[ 278]---> BDD-cost:    2
c ---[ 277]---> BDD-cost:    4
c ---[ 276]---> BDD-cost:    2
c ---[ 275]---> BDD-cost:    4
c ---[ 274]---> BDD-cost:    2
c ---[ 273]---> BDD-cost:    4
c ---[ 272]---> BDD-cost:    2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    2
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    2
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    2
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    2
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    2
c ---[ 253]---> BDD-cost:    2
c ---[ 252]---> BDD-cost:    2
c ---[ 251]---> BDD-cost:    2
c ---[ 250]---> BDD-cost:    2
c ---[ 249]---> BDD-cost:    2
c ---[ 248]---> BDD-cost:    2
c ---[ 247]---> BDD-cost:    5
c ---[ 246]---> BDD-cost:    2
c ---[ 245]---> BDD-cost:    2
c ---[ 244]---> BDD-cost:    2
c ---[ 243]---> BDD-cost:    2
c ---[ 242]---> BDD-cost:    2
c ---[ 241]---> BDD-cost:    2
c ---[ 240]---> BDD-cost:    2
c ---[ 239]---> BDD-cost:    4
c ---[ 238]---> BDD-cost:    2
c ---[ 237]---> BDD-cost:    2
c ---[ 236]---> BDD-cost:    2
c ---[ 235]---> BDD-cost:    2
c ---[ 234]---> BDD-cost:    2
c ---[ 233]---> BDD-cost:    2
c ---[ 232]---> BDD-cost:    2
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    2
c ---[ 229]---> BDD-cost:    2
c ---[ 228]---> BDD-cost:    2
c ---[ 227]---> BDD-cost:    2
c ---[ 226]---> BDD-cost:    2
c ---[ 225]---> BDD-cost:    2
c ---[ 224]---> BDD-cost:    2
c ---[ 223]---> BDD-cost:    2
c ---[ 222]---> BDD-cost:    2
c ---[ 221]---> BDD-cost:    2
c ---[ 220]---> BDD-cost:    2
c ---[ 219]---> BDD-cost:    2
c ---[ 218]---> BDD-cost:    2
c ---[ 217]---> BDD-cost:    2
c ---[ 216]---> BDD-cost:    2
c ---[ 215]---> BDD-cost:    4
c ---[ 214]---> BDD-cost:    2
c ---[ 213]---> BDD-cost:    2
c ---[ 212]---> BDD-cost:    2
c ---[ 211]---> BDD-cost:    2
c ---[ 210]---> BDD-cost:    2
c ---[ 209]---> BDD-cost:    2
c ---[ 208]---> BDD-cost:    2
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    2
c ---[ 205]---> BDD-cost:    2
c ---[ 204]---> BDD-cost:    2
c ---[ 203]---> BDD-cost:    2
c ---[ 202]---> BDD-cost:    2
c ---[ 201]---> BDD-cost:    2
c ---[ 200]---> BDD-cost:    2
c ---[ 191]---> BDD-cost:    2
c ---[ 190]---> BDD-cost:    2
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 181]---> BDD-cost:    2
c ---[ 180]---> BDD-cost:    2
c ---[ 179]---> BDD-cost:    2
c ---[ 178]---> BDD-cost:    2
c ---[ 177]---> BDD-cost:    2
c ---[ 176]---> BDD-cost:    2
c ---[ 175]---> BDD-cost:    2
c ---[ 174]---> BDD-cost:    2
c ---[ 173]---> BDD-cost:    2
c ---[ 172]---> BDD-cost:    2
c ---[ 171]---> BDD-cost:    2
c ---[ 170]---> BDD-cost:    2
c ---[ 169]---> BDD-cost:    2
c ---[ 168]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 166]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 164]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 162]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    2
c ---[ 159]---> BDD-cost:    2
c ---[ 158]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    2
c ---[ 156]---> BDD-cost:    2
c ---[ 155]---> BDD-cost:    2
c ---[ 154]---> BDD-cost:    2
c ---[ 153]---> BDD-cost:    2
c ---[ 152]---> BDD-cost:    2
c ---[ 151]---> BDD-cost:    2
c ---[ 150]---> BDD-cost:    2
c ---[ 149]---> BDD-cost:    2
c ---[ 148]---> BDD-cost:    2
c ---[ 147]---> BDD-cost:    2
c ---[ 146]---> BDD-cost:    2
c ---[ 145]---> BDD-cost:    2
c ---[ 144]---> BDD-cost:    2
c ---[ 143]---> BDD-cost:    2
c ---[ 142]---> BDD-cost:    2
c ---[ 141]---> BDD-cost:    2
c ---[ 140]---> BDD-cost:    2
c ---[ 139]---> BDD-cost:    2
c ---[ 138]---> BDD-cost:    2
c ---[ 137]---> BDD-cost:    2
c ---[ 136]---> BDD-cost:    2
c ---[ 127]---> BDD-cost:    2
c ---[ 126]---> BDD-cost:    2
c ---[ 125]---> BDD-cost:    2
c ---[ 124]---> BDD-cost:    2
c ---[ 123]---> BDD-cost:    2
c ---[ 122]---> BDD-cost:    2
c ---[ 121]---> BDD-cost:    2
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 118]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 116]---> BDD-cost:    2
c ---[ 115]---> BDD-cost:    2
c ---[ 114]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 111]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 109]---> BDD-cost:    2
c ---[ 108]---> BDD-cost:    2
c ---[ 107]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 104]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[ 102]---> BDD-cost:    2
c ---[ 101]---> BDD-cost:    2
c ---[ 100]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  94]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  88]---> BDD-cost:    2
c ---[  87]---> BDD-cost:    2
c ---[  86]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  83]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  81]---> BDD-cost:    2
c ---[  80]---> BDD-cost:    2
c ---[  79]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  76]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  74]---> BDD-cost:    2
c ---[  73]---> BDD-cost:    2
c ---[  72]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  62]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  60]---> BDD-cost:    2
c ---[  59]---> BDD-cost:    2
c ---[  58]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  55]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  53]---> BDD-cost:    2
c ---[  52]---> BDD-cost:    2
c ---[  51]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  48]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  46]---> BDD-cost:    2
c ---[  45]---> BDD-cost:    2
c ---[  44]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  41]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  39]---> BDD-cost:    2
c ---[  38]---> BDD-cost:    2
c ---[  37]---> BDD-cost:    2
c ---[  36]---> BDD-cost:    2
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:    2
c ---[  33]---> BDD-cost:    2
c ---[  32]---> BDD-cost:    2
c ---[  31]---> BDD-cost:    2
c ---[  30]---> BDD-cost:    2
c ---[  29]---> BDD-cost:    2
c ---[  28]---> BDD-cost:    2
c ---[  27]---> BDD-cost:    2
c ---[  26]---> BDD-cost:    2
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost:    2
c ---[  23]---> BDD-cost:    2
c ---[  22]---> BDD-cost:    2
c ---[  21]---> BDD-cost:    2
c ---[  20]---> BDD-cost:    2
c ---[  19]---> BDD-cost:    2
c ---[  18]---> BDD-cost:    2
c ---[  17]---> BDD-cost:    2
c ---[  16]---> BDD-cost:    2
c ---[  15]---> BDD-cost:    2
c ---[  14]---> BDD-cost:    2
c ---[  13]---> BDD-cost:    2
c ---[  12]---> BDD-cost:    2
c ---[  11]---> BDD-cost:    2
c ---[  10]---> BDD-cost:    2
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27714    80370 |    9238       0        0     nan |  0.000 % |
c |       101 |   27714    80370 |   10161     101     1108    11.0 | 27.023 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       113 |   44918   120698 |   14972     113     1273    11.3 | 27.023 % |
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       127 |   44978   120846 |   14992     127     1979    15.6 | 27.023 % |
c |       227 |   44585   119956 |   16491     216     2966    13.7 | 15.975 % |
c |       378 |   44225   119138 |   18140     358     4796    13.4 | 16.783 % |
c |       603 |   44052   118743 |   19954     581    12516    21.5 | 17.172 % |
c |       942 |   43527   117532 |   21949     911    21336    23.4 | 18.393 % |
c |      1449 |   43396   117230 |   24144    1415    49025    34.6 | 18.689 % |
c |      2208 |   41061   111830 |   26559    2124    69384    32.7 | 24.390 % |
c ==============================================================================
c [1mFound solution: 78[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3006 |   40820   111283 |   13606    2912    91195    31.3 | 24.390 % |
c |      3106 |   40795   111208 |   14966    3004    95488    31.8 | 25.097 % |
c |      3259 |   40790   111193 |   16463    3155    97888    31.0 | 25.105 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3405 |   40711   111004 |   13570    3294   101714    30.9 | 25.105 % |
c |      3506 |   40643   110842 |   14927    3394   106021    31.2 | 25.468 % |
c |      3657 |   40643   110842 |   16419    3545   109776    31.0 | 25.468 % |
c |      3882 |   40435   110357 |   18061    3756   115834    30.8 | 25.965 % |
c ==============================================================================
c [1mFound solution: 74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3898 |   40474   110456 |   13491    3771   116308    30.8 | 25.965 % |
c |      3998 |   40474   110456 |   14840    3871   119483    30.9 | 25.954 % |
c |      4148 |   40474   110456 |   16324    4021   125318    31.2 | 25.954 % |
c |      4373 |   40440   110364 |   17956    4239   130491    30.8 | 26.016 % |
c |      4711 |   40430   110334 |   19752    4573   142539    31.2 | 26.032 % |
c |      5217 |   40362   110166 |   21727    5073   163110    32.2 | 26.195 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5869 |   40379   110209 |   13459    5725   195381    34.1 | 26.195 % |
c |      5973 |   40374   110194 |   14804    5828   198842    34.1 | 26.200 % |
c |      6124 |   40369   110179 |   16285    5977   203094    34.0 | 26.208 % |
c |      6351 |   40369   110179 |   17913    6204   211052    34.0 | 26.208 % |
c |      6689 |   40369   110179 |   19705    6542   225359    34.4 | 26.208 % |
c |      7196 |   40359   110149 |   21675    7046   248740    35.3 | 26.223 % |
c |      7957 |   40354   110134 |   23843    7806   278137    35.6 | 26.231 % |
c |      9098 |   39642   108475 |   26227    8908   300628    33.7 | 27.991 % |
c |     10807 |   39515   108182 |   28850   10608   402556    37.9 | 28.309 % |
c |     13369 |   39456   108039 |   31735   13162   525778    39.9 | 28.425 % |
c |     17215 |   39413   107910 |   34909   16978   704918    41.5 | 28.479 % |
c |     22982 |   39338   107696 |   38400   22720   962366    42.4 | 28.604 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25542 |   39341   107700 |   13113   25263  1082544    42.9 | 28.604 % |
c |     25642 |   39341   107700 |   14424   12732   470529    37.0 | 28.663 % |
c |     25794 |   39280   107559 |   15866   12882   474554    36.8 | 28.818 % |
c |     26019 |   39280   107559 |   17453   13107   487263    37.2 | 28.818 % |
c |     26356 |   39280   107559 |   19198   13444   504770    37.5 | 28.818 % |
c |     26862 |   39280   107559 |   21118   13950   524685    37.6 | 28.818 % |
c |     27621 |   39270   107529 |   23230   14706   565172    38.4 | 28.834 % |
c |     28761 |   39245   107454 |   25553   15838   626110    39.5 | 28.872 % |
c |     30469 |   39240   107439 |   28108   17545   697241    39.7 | 28.880 % |
c |     33032 |   39179   107295 |   30919   20099   796116    39.6 | 28.996 % |
c |     36877 |   39155   107229 |   34011   23940   999524    41.8 | 29.035 % |
c |     42643 |   39116   107118 |   37412   29694  1331219    44.8 | 29.097 % |
c |     51292 |   38967   106763 |   41154   38326  1705365    44.5 | 29.438 % |
c |     64266 |   38758   106274 |   45269   19032   752196    39.5 | 29.933 % |
c |     83727 |   38557   105754 |   49796   38463  1736817    45.2 | 30.359 % |
c |    112919 |   38406   105352 |   54776   30234  1164548    38.5 | 30.638 % |
c |    156708 |   38194   104801 |   60253   31281  1073127    34.3 | 31.049 % |
c |    222393 |   37783   103780 |   66279   52209  2528830    48.4 | 31.877 % |
c |    320919 |   37399   102830 |   72907   48047  2118950    44.1 | 32.675 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.93 0.90 2/54 13434
Raw data (stat): 13434 (runsolver) R 13433 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423467821 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 1641 0 0 0 995 3 0 0 25 0 1 0 423467821 8630272 1619 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2107 1619 603 41 0 2066 0
vsize: 8428
[startup+20.0006 s]
Raw data (loadavg): 0.85 0.93 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 1835 0 0 0 1993 4 0 0 25 0 1 0 423467821 9428992 1813 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1813 603 41 0 2261 0
vsize: 9208
[startup+30.0018 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2052 0 0 0 2992 5 0 0 25 0 1 0 423467821 10371072 2030 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2532 2030 603 41 0 2491 0
vsize: 10128
[startup+40.002 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2233 0 0 0 3990 6 0 0 25 0 1 0 423467821 11034624 2211 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2694 2211 603 41 0 2653 0
vsize: 10776
[startup+50.0022 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2434 0 0 0 4990 6 0 0 25 0 1 0 423467821 12025856 2412 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2936 2412 603 41 0 2895 0
vsize: 11744
[startup+60.003 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2617 0 0 0 5989 7 0 0 25 0 1 0 423467821 12693504 2595 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3099 2595 603 41 0 3058 0
vsize: 12396
[startup+70.0039 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2787 0 0 0 6988 8 0 0 25 0 1 0 423467821 13361152 2765 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3262 2765 603 41 0 3221 0
vsize: 13048
[startup+80.0047 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2787 0 0 0 7988 8 0 0 25 0 1 0 423467821 13361152 2765 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3262 2765 603 41 0 3221 0
vsize: 13048
[startup+90.0046 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2787 0 0 0 8988 8 0 0 25 0 1 0 423467821 13361152 2765 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3262 2765 603 41 0 3221 0
vsize: 13048
[startup+100.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2787 0 0 0 9989 8 0 0 25 0 1 0 423467821 13361152 2765 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3262 2765 603 41 0 3221 0
vsize: 13048
[startup+110.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 2853 0 0 0 10989 8 0 0 25 0 1 0 423467821 13627392 2831 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3327 2831 603 41 0 3286 0
vsize: 13308
[startup+120.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3044 0 0 0 11988 9 0 0 25 0 1 0 423467821 14422016 3022 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3521 3022 603 41 0 3480 0
vsize: 14084
[startup+130.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3403 0 0 0 12988 10 0 0 25 0 1 0 423467821 16031744 3381 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3914 3381 603 41 0 3873 0
vsize: 15656
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3927 0 0 0 13986 11 0 0 25 0 1 0 423467821 18046976 3905 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3905 603 41 0 4365 0
vsize: 17624
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3936 0 0 0 14987 11 0 0 25 0 1 0 423467821 18178048 3914 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3914 603 41 0 4397 0
vsize: 17752
[startup+160.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3936 0 0 0 15987 11 0 0 25 0 1 0 423467821 18178048 3914 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3914 603 41 0 4397 0
vsize: 17752
[startup+170.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3936 0 0 0 16987 11 0 0 25 0 1 0 423467821 18178048 3914 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3914 603 41 0 4397 0
vsize: 17752
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3936 0 0 0 17987 11 0 0 25 0 1 0 423467821 18178048 3914 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3914 603 41 0 4397 0
vsize: 17752
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3936 0 0 0 18987 11 0 0 25 0 1 0 423467821 18178048 3914 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3914 603 41 0 4397 0
vsize: 17752
[startup+200.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 3936 0 0 0 19987 11 0 0 25 0 1 0 423467821 18178048 3914 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3914 603 41 0 4397 0
vsize: 17752
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4055 0 0 0 20987 11 0 0 25 0 1 0 423467821 18583552 4033 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4537 4033 603 41 0 4496 0
vsize: 18148
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4347 0 0 0 21986 13 0 0 25 0 1 0 423467821 19779584 4325 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4829 4325 603 41 0 4788 0
vsize: 19316
[startup+230.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 22986 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223592 1075352675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 23986 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 24987 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 25987 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 26987 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+280.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 27987 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+290.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 28988 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+300.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 29988 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4566 0 0 0 30988 13 0 0 25 0 1 0 423467821 20713472 4544 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4544 603 41 0 5016 0
vsize: 20228
[startup+320.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4577 0 0 0 31989 13 0 0 25 0 1 0 423467821 20713472 4555 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4555 603 41 0 5016 0
vsize: 20228
[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4585 0 0 0 32989 13 0 0 25 0 1 0 423467821 20713472 4563 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5057 4563 603 41 0 5016 0
vsize: 20228
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4740 0 0 0 33989 14 0 0 25 0 1 0 423467821 21368832 4718 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5217 4718 603 41 0 5176 0
vsize: 20868
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4747 0 0 0 34989 14 0 0 25 0 1 0 423467821 21368832 4725 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5217 4725 603 41 0 5176 0
vsize: 20868
[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4752 0 0 0 35989 14 0 0 25 0 1 0 423467821 21524480 4730 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4730 603 41 0 5214 0
vsize: 21020
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4752 0 0 0 36989 14 0 0 25 0 1 0 423467821 21524480 4730 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4730 603 41 0 5214 0
vsize: 21020
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4753 0 0 0 37989 14 0 0 25 0 1 0 423467821 21524480 4731 4294967295 134512640 134672761 3221224576 3221223776 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4731 603 41 0 5214 0
vsize: 21020
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4753 0 0 0 38990 14 0 0 25 0 1 0 423467821 21524480 4731 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4731 603 41 0 5214 0
vsize: 21020
[startup+400.025 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4753 0 0 0 39990 14 0 0 25 0 1 0 423467821 21524480 4731 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4731 603 41 0 5214 0
vsize: 21020
[startup+410.026 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4753 0 0 0 40990 14 0 0 25 0 1 0 423467821 21524480 4731 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4731 603 41 0 5214 0
vsize: 21020
[startup+420.026 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4758 0 0 0 41990 14 0 0 25 0 1 0 423467821 21524480 4736 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4736 603 41 0 5214 0
vsize: 21020
[startup+430.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4758 0 0 0 42990 14 0 0 25 0 1 0 423467821 21524480 4736 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4736 603 41 0 5214 0
vsize: 21020
[startup+440.028 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4758 0 0 0 43991 14 0 0 25 0 1 0 423467821 21524480 4736 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5255 4736 603 41 0 5214 0
vsize: 21020
[startup+450.028 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 4951 0 0 0 44990 15 0 0 25 0 1 0 423467821 22323200 4929 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5450 4929 603 41 0 5409 0
vsize: 21800
[startup+460.029 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5103 0 0 0 45989 16 0 0 25 0 1 0 423467821 22863872 5081 4294967295 134512640 134672761 3221224576 3221223712 134560645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5582 5081 603 41 0 5541 0
vsize: 22328
[startup+470.029 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5241 0 0 0 46989 16 0 0 25 0 1 0 423467821 23396352 5219 4294967295 134512640 134672761 3221224576 3221223744 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5712 5219 603 41 0 5671 0
vsize: 22848
[startup+480.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5376 0 0 0 47988 17 0 0 25 0 1 0 423467821 24055808 5354 4294967295 134512640 134672761 3221224576 3221223712 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5354 603 41 0 5832 0
vsize: 23492
[startup+490.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5376 0 0 0 48988 17 0 0 25 0 1 0 423467821 24055808 5354 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5354 603 41 0 5832 0
vsize: 23492
[startup+500.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5376 0 0 0 49989 17 0 0 25 0 1 0 423467821 24055808 5354 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5354 603 41 0 5832 0
vsize: 23492
[startup+510.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5376 0 0 0 50989 17 0 0 25 0 1 0 423467821 24055808 5354 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5354 603 41 0 5832 0
vsize: 23492
[startup+520.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5380 0 0 0 51989 17 0 0 25 0 1 0 423467821 24055808 5358 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5358 603 41 0 5832 0
vsize: 23492
[startup+530.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5380 0 0 0 52989 17 0 0 25 0 1 0 423467821 24055808 5358 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5358 603 41 0 5832 0
vsize: 23492
[startup+540.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5382 0 0 0 53989 17 0 0 25 0 1 0 423467821 24055808 5360 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5360 603 41 0 5832 0
vsize: 23492
[startup+550.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5388 0 0 0 54989 17 0 0 25 0 1 0 423467821 24055808 5366 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5366 603 41 0 5832 0
vsize: 23492
[startup+560.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5391 0 0 0 55990 17 0 0 25 0 1 0 423467821 24055808 5369 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5369 603 41 0 5832 0
vsize: 23492
[startup+570.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5391 0 0 0 56990 17 0 0 25 0 1 0 423467821 24055808 5369 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5369 603 41 0 5832 0
vsize: 23492
[startup+580.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5397 0 0 0 57990 17 0 0 25 0 1 0 423467821 24055808 5375 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5375 603 41 0 5832 0
vsize: 23492
[startup+590.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5399 0 0 0 58990 17 0 0 25 0 1 0 423467821 24055808 5377 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5873 5377 603 41 0 5832 0
vsize: 23492
[startup+600.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5407 0 0 0 59990 17 0 0 25 0 1 0 423467821 24199168 5385 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5908 5385 603 41 0 5867 0
vsize: 23632
[startup+610.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5412 0 0 0 60990 17 0 0 25 0 1 0 423467821 24199168 5390 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5908 5390 603 41 0 5867 0
vsize: 23632
[startup+620.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5473 0 0 0 61990 17 0 0 25 0 1 0 423467821 24469504 5451 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5451 603 41 0 5933 0
vsize: 23896
[startup+630.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5642 0 0 0 62990 18 0 0 25 0 1 0 423467821 25137152 5620 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5620 603 41 0 6096 0
vsize: 24548
[startup+640.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5780 0 0 0 63990 18 0 0 25 0 1 0 423467821 25931776 5758 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6331 5758 603 41 0 6290 0
vsize: 25324
[startup+650.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 5904 0 0 0 64989 19 0 0 25 0 1 0 423467821 26468352 5882 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6462 5882 603 41 0 6421 0
vsize: 25848
[startup+660.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6025 0 0 0 65989 19 0 0 25 0 1 0 423467821 26865664 6003 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6559 6003 603 41 0 6518 0
vsize: 26236
[startup+670.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 66989 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223760 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+680.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 67989 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+690.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 68990 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+700.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 69990 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223776 134557892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+710.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 70990 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223680 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+720.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 71990 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+730.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 72990 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+740.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 73990 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+750.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 74991 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+760.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 75991 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+770.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 76991 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+780.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 77991 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+790.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6097 0 0 0 78991 19 0 0 25 0 1 0 423467821 27262976 6075 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6075 603 41 0 6615 0
vsize: 26624
[startup+800.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6105 0 0 0 79991 19 0 0 25 0 1 0 423467821 27262976 6083 4294967295 134512640 134672761 3221224576 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6656 6083 603 41 0 6615 0
vsize: 26624
[startup+810.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6134 0 0 0 80992 19 0 0 25 0 1 0 423467821 27426816 6112 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6696 6112 603 41 0 6655 0
vsize: 26784
[startup+820.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6152 0 0 0 81992 19 0 0 25 0 1 0 423467821 27426816 6130 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6696 6130 603 41 0 6655 0
vsize: 26784
[startup+830.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6165 0 0 0 82992 19 0 0 25 0 1 0 423467821 27574272 6143 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6143 603 41 0 6691 0
vsize: 26928
[startup+840.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6172 0 0 0 83992 19 0 0 25 0 1 0 423467821 27574272 6150 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6150 603 41 0 6691 0
vsize: 26928
[startup+850.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6191 0 0 0 84992 19 0 0 25 0 1 0 423467821 27721728 6169 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6768 6169 603 41 0 6727 0
vsize: 27072
[startup+860.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6218 0 0 0 85993 19 0 0 25 0 1 0 423467821 27865088 6196 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6803 6196 603 41 0 6762 0
vsize: 27212
[startup+870.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6242 0 0 0 86993 19 0 0 25 0 1 0 423467821 27865088 6220 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6803 6220 603 41 0 6762 0
vsize: 27212
[startup+880.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 87993 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+890.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 88993 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+900.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 89993 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+910.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 90993 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+920.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 91993 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223660 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+930.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 92993 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+940.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 93994 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+950.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6305 0 0 0 94994 20 0 0 25 0 1 0 423467821 28127232 6283 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6867 6283 603 41 0 6826 0
vsize: 27468
[startup+960.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6320 0 0 0 95994 20 0 0 25 0 1 0 423467821 28274688 6298 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6298 603 41 0 6862 0
vsize: 27612
[startup+970.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6320 0 0 0 96994 20 0 0 25 0 1 0 423467821 28274688 6298 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6298 603 41 0 6862 0
vsize: 27612
[startup+980.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6320 0 0 0 97994 20 0 0 25 0 1 0 423467821 28274688 6298 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6298 603 41 0 6862 0
vsize: 27612
[startup+990.044 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6325 0 0 0 98995 20 0 0 25 0 1 0 423467821 28274688 6303 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6303 603 41 0 6862 0
vsize: 27612
[startup+1000.04 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6332 0 0 0 99994 20 0 0 25 0 1 0 423467821 28274688 6310 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6310 603 41 0 6862 0
vsize: 27612
[startup+1010.05 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6333 0 0 0 100994 20 0 0 25 0 1 0 423467821 28274688 6311 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6311 603 41 0 6862 0
vsize: 27612
[startup+1020.05 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6345 0 0 0 101994 20 0 0 25 0 1 0 423467821 28418048 6323 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6938 6323 603 41 0 6897 0
vsize: 27752
[startup+1030.04 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6350 0 0 0 102995 20 0 0 25 0 1 0 423467821 28418048 6328 4294967295 134512640 134672761 3221224576 3221223760 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6938 6328 603 41 0 6897 0
vsize: 27752
[startup+1040.05 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6354 0 0 0 103995 20 0 0 25 0 1 0 423467821 28418048 6332 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6938 6332 603 41 0 6897 0
vsize: 27752
[startup+1050.05 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6354 0 0 0 104995 20 0 0 25 0 1 0 423467821 28418048 6332 4294967295 134512640 134672761 3221224576 3221223712 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6938 6332 603 41 0 6897 0
vsize: 27752
[startup+1060.05 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6360 0 0 0 105995 20 0 0 25 0 1 0 423467821 28418048 6338 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6938 6338 603 41 0 6897 0
vsize: 27752
[startup+1070.05 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6366 0 0 0 106995 20 0 0 25 0 1 0 423467821 28418048 6344 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6938 6344 603 41 0 6897 0
vsize: 27752
[startup+1080.05 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6385 0 0 0 107995 20 0 0 25 0 1 0 423467821 28565504 6363 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6974 6363 603 41 0 6933 0
vsize: 27896
[startup+1090.05 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6385 0 0 0 108996 20 0 0 25 0 1 0 423467821 28565504 6363 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6974 6363 603 41 0 6933 0
vsize: 27896
[startup+1100.05 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6386 0 0 0 109996 20 0 0 25 0 1 0 423467821 28565504 6364 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6974 6364 603 41 0 6933 0
vsize: 27896
[startup+1110.05 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6403 0 0 0 110996 20 0 0 25 0 1 0 423467821 28565504 6381 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6974 6381 603 41 0 6933 0
vsize: 27896
[startup+1120.05 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6479 0 0 0 111995 21 0 0 25 0 1 0 423467821 28971008 6457 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7073 6457 603 41 0 7032 0
vsize: 28292
[startup+1130.05 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6584 0 0 0 112995 21 0 0 25 0 1 0 423467821 29372416 6562 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7171 6562 603 41 0 7130 0
vsize: 28684
[startup+1140.05 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6615 0 0 0 113995 22 0 0 25 0 1 0 423467821 29507584 6593 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7204 6593 603 41 0 7163 0
vsize: 28816
[startup+1150.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6615 0 0 0 114995 22 0 0 25 0 1 0 423467821 29507584 6593 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7204 6593 603 41 0 7163 0
vsize: 28816
[startup+1160.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6615 0 0 0 115995 22 0 0 25 0 1 0 423467821 29507584 6593 4294967295 134512640 134672761 3221224576 3221223680 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7204 6593 603 41 0 7163 0
vsize: 28816
[startup+1170.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6625 0 0 0 116996 22 0 0 25 0 1 0 423467821 29507584 6603 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7204 6603 603 41 0 7163 0
vsize: 28816
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6633 0 0 0 117995 22 0 0 25 0 1 0 423467821 29507584 6611 4294967295 134512640 134672761 3221224576 3221223744 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7204 6611 603 41 0 7163 0
vsize: 28816
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6640 0 0 0 118996 22 0 0 25 0 1 0 423467821 29642752 6618 4294967295 134512640 134672761 3221224576 3221223744 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6618 603 41 0 7196 0
vsize: 28948
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13434
Raw data (stat): 13434 (minisat+) R 13433 5897 5896 0 -1 0 6650 0 0 0 119996 22 0 0 25 0 1 0 423467821 29642752 6628 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6628 603 41 0 7196 0
vsize: 28948
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 13434
Raw data (stat): 13434 (minisat+) Z 13433 5897 5896 0 -1 12 6653 0 0 0 119996 23 0 0 25 0 1 0 423467821 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.2
CPU user time (s): 1199.96
CPU system time (s): 0.236963
CPU usage (%): 100.011
Max. virtual memory (Kb): 28948
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####