PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-13 21:15:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2354 boxname=wulflinc28 idbench=262 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3ce91e964f348d481da3f7741c5768eb  /oldhome/oroussel/tmp/wulflinc28/normalized-data6_3.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc28/normalized-data6_3.opb
IDLAUNCH: 2354
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        910852 kB
Buffers:         34248 kB
Cached:          53740 kB
SwapCached:          4 kB
Active:          49104 kB
Inactive:        41696 kB
HighTotal:      131008 kB
HighFree:        73724 kB
LowTotal:       903652 kB
LowFree:        837128 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27480 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:35:34 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 2354 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4626 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[4624]---> BDD-cost:   17
c ---[4622]---> BDD-cost:   17
c ---[4620]---> BDD-cost:   17
c ---[4618]---> BDD-cost:   17
c ---[4616]---> BDD-cost:   17
c ---[4614]---> BDD-cost:   17
c ---[4612]---> BDD-cost:   17
c ---[4610]---> BDD-cost:   17
c ---[4608]---> BDD-cost:   17
c ---[4606]---> BDD-cost:   17
c ---[4604]---> BDD-cost:   17
c ---[4602]---> BDD-cost:   17
c ---[4600]---> BDD-cost:   17
c ---[4598]---> BDD-cost:   17
c ---[4596]---> BDD-cost:   17
c ---[4594]---> BDD-cost:   17
c ---[4592]---> BDD-cost:   17
c ---[4590]---> BDD-cost:   17
c ---[4588]---> BDD-cost:   17
c ---[4586]---> BDD-cost:   17
c ---[4584]---> BDD-cost:   17
c ---[4582]---> BDD-cost:   17
c ---[4580]---> BDD-cost:   17
c ---[4578]---> BDD-cost:   17
c ---[4576]---> BDD-cost:   17
c ---[4574]---> BDD-cost:   17
c ---[4572]---> BDD-cost:   17
c ---[4570]---> BDD-cost:   17
c ---[4568]---> BDD-cost:   17
c ---[4566]---> BDD-cost:   17
c ---[4265]---> BDD-cost:    7
c ---[4264]---> BDD-cost:    7
c ---[4263]---> BDD-cost:    7
c ---[4262]---> BDD-cost:    7
c ---[4261]---> BDD-cost:    7
c ---[4260]---> BDD-cost:    7
c ---[4259]---> BDD-cost:    7
c ---[4258]---> BDD-cost:    7
c ---[4257]---> BDD-cost:    7
c ---[4256]---> BDD-cost:    7
c ---[4255]---> BDD-cost:    7
c ---[4254]---> BDD-cost:    7
c ---[4253]---> BDD-cost:    7
c ---[4252]---> BDD-cost:    7
c ---[4251]---> BDD-cost:    7
c ---[4250]---> BDD-cost:    7
c ---[4249]---> BDD-cost:    7
c ---[4248]---> BDD-cost:    7
c ---[4247]---> BDD-cost:    7
c ---[4246]---> BDD-cost:    7
c ---[4245]---> BDD-cost:    7
c ---[4244]---> BDD-cost:    7
c ---[4243]---> BDD-cost:    7
c ---[4242]---> BDD-cost:    7
c ---[4241]---> BDD-cost:    7
c ---[4240]---> BDD-cost:    7
c ---[4239]---> BDD-cost:    7
c ---[4238]---> BDD-cost:    7
c ---[4237]---> BDD-cost:    7
c ---[4236]---> BDD-cost:    7
c ---[4235]---> BDD-cost:    7
c ---[4234]---> BDD-cost:    7
c ---[4233]---> BDD-cost:    7
c ---[4232]---> BDD-cost:    7
c ---[4231]---> BDD-cost:    7
c ---[4230]---> BDD-cost:    7
c ---[4229]---> BDD-cost:    7
c ---[4228]---> BDD-cost:    7
c ---[4227]---> BDD-cost:    7
c ---[4226]---> BDD-cost:    7
c ---[4225]---> BDD-cost:    7
c ---[4224]---> BDD-cost:    7
c ---[4223]---> BDD-cost:    7
c ---[4222]---> BDD-cost:    7
c ---[4221]---> BDD-cost:    7
c ---[4220]---> BDD-cost:    7
c ---[4219]---> BDD-cost:    7
c ---[4218]---> BDD-cost:    7
c ---[4217]---> BDD-cost:    7
c ---[4216]---> BDD-cost:    7
c ---[4215]---> BDD-cost:    7
c ---[4214]---> BDD-cost:    7
c ---[4213]---> BDD-cost:    7
c ---[4212]---> BDD-cost:    7
c ---[4211]---> BDD-cost:    7
c ---[4210]---> BDD-cost:    7
c ---[4209]---> BDD-cost:    7
c ---[4208]---> BDD-cost:    7
c ---[4207]---> BDD-cost:    7
c ---[4206]---> BDD-cost:    7
c ---[4204]---> BDD-cost:    9
c ---[4202]---> BDD-cost:    9
c ---[4200]---> BDD-cost:    9
c ---[4198]---> BDD-cost:    9
c ---[4196]---> BDD-cost:    9
c ---[4194]---> BDD-cost:    9
c ---[4192]---> BDD-cost:    9
c ---[4190]---> BDD-cost:    9
c ---[4188]---> BDD-cost:    9
c ---[4186]---> BDD-cost:    9
c ---[4184]---> BDD-cost:    9
c ---[4182]---> BDD-cost:    9
c ---[4180]---> BDD-cost:    9
c ---[4178]---> BDD-cost:    9
c ---[4176]---> BDD-cost:    9
c ---[4174]---> BDD-cost:    9
c ---[4172]---> BDD-cost:    9
c ---[4170]---> BDD-cost:    9
c ---[4168]---> BDD-cost:    9
c ---[4166]---> BDD-cost:    9
c ---[4164]---> BDD-cost:    9
c ---[4162]---> BDD-cost:    9
c ---[4160]---> BDD-cost:    9
c ---[4158]---> BDD-cost:    9
c ---[4156]---> BDD-cost:    9
c ---[4154]---> BDD-cost:    9
c ---[4152]---> BDD-cost:    9
c ---[4150]---> BDD-cost:    9
c ---[4148]---> BDD-cost:    9
c ---[4146]---> BDD-cost:    9
c ---[4144]---> BDD-cost:    9
c ---[4142]---> BDD-cost:    9
c ---[4140]---> BDD-cost:    9
c ---[4138]---> BDD-cost:    9
c ---[4136]---> BDD-cost:    9
c ---[4134]---> BDD-cost:    9
c ---[4132]---> BDD-cost:    9
c ---[4130]---> BDD-cost:    9
c ---[4128]---> BDD-cost:    9
c ---[4126]---> BDD-cost:    9
c ---[4124]---> BDD-cost:    9
c ---[4122]---> BDD-cost:    9
c ---[4120]---> BDD-cost:    9
c ---[4118]---> BDD-cost:    9
c ---[4116]---> BDD-cost:    9
c ---[4114]---> BDD-cost:    9
c ---[4112]---> BDD-cost:    9
c ---[4110]---> BDD-cost:    9
c ---[4108]---> BDD-cost:    9
c ---[4106]---> BDD-cost:    9
c ---[4104]---> BDD-cost:    9
c ---[4102]---> BDD-cost:    9
c ---[4100]---> BDD-cost:    9
c ---[4098]---> BDD-cost:    9
c ---[4096]---> BDD-cost:    9
c ---[4094]---> BDD-cost:    9
c ---[4092]---> BDD-cost:    9
c ---[4090]---> BDD-cost:    9
c ---[4088]---> BDD-cost:    9
c ---[4086]---> BDD-cost:    9
c ---[4079]---> BDD-cost:   64
c ---[4078]---> BDD-cost:   64
c ---[4077]---> BDD-cost:   64
c ---[4076]---> BDD-cost:   64
c ---[4075]---> BDD-cost:   64
c ---[4074]---> BDD-cost:   64
c ---[4067]---> BDD-cost:   67
c ---[4066]---> BDD-cost:   67
c ---[4065]---> BDD-cost:   67
c ---[4064]---> BDD-cost:   67
c ---[4063]---> BDD-cost:   67
c ---[4062]---> BDD-cost:   67
c ---[4055]---> BDD-cost:   67
c ---[4054]---> BDD-cost:   67
c ---[4053]---> BDD-cost:   67
c ---[4052]---> BDD-cost:   67
c ---[4051]---> BDD-cost:   67
c ---[4050]---> BDD-cost:   67
c ---[4043]---> BDD-cost:   67
c ---[4042]---> BDD-cost:   67
c ---[4041]---> BDD-cost:   67
c ---[4040]---> BDD-cost:   67
c ---[4039]---> BDD-cost:   67
c ---[4038]---> BDD-cost:   67
c ---[4031]---> BDD-cost:   67
c ---[4030]---> BDD-cost:   67
c ---[4029]---> BDD-cost:   67
c ---[4028]---> BDD-cost:   67
c ---[4027]---> BDD-cost:   67
c ---[4026]---> BDD-cost:   67
c ---[4019]---> BDD-cost:   67
c ---[4018]---> BDD-cost:   67
c ---[4017]---> BDD-cost:   67
c ---[4016]---> BDD-cost:   67
c ---[4015]---> BDD-cost:   67
c ---[4014]---> BDD-cost:   67
c ---[4007]---> BDD-cost:   67
c ---[4006]---> BDD-cost:   67
c ---[4005]---> BDD-cost:   67
c ---[4004]---> BDD-cost:   67
c ---[4003]---> BDD-cost:   67
c ---[4002]---> BDD-cost:   67
c ---[2050]---> BDD-cost:    7
c ---[2048]---> BDD-cost:    7
c ---[2046]---> BDD-cost:    7
c ---[2044]---> BDD-cost:    7
c ---[2042]---> BDD-cost:    7
c ---[2040]---> BDD-cost:    7
c ---[2038]---> BDD-cost:    7
c ---[2036]---> BDD-cost:    7
c ---[2034]---> BDD-cost:    7
c ---[2032]---> BDD-cost:    7
c ---[2030]---> BDD-cost:    7
c ---[2028]---> BDD-cost:    7
c ---[2026]---> BDD-cost:    7
c ---[2024]---> BDD-cost:    7
c ---[2022]---> BDD-cost:    7
c ---[2020]---> BDD-cost:    7
c ---[2018]---> BDD-cost:    7
c ---[2016]---> BDD-cost:    7
c ---[2014]---> BDD-cost:    7
c ---[2012]---> BDD-cost:    7
c ---[2010]---> BDD-cost:    7
c ---[2008]---> BDD-cost:    7
c ---[2006]---> BDD-cost:    7
c ---[2004]---> BDD-cost:    7
c ---[2002]---> BDD-cost:    7
c ---[2000]---> BDD-cost:    7
c ---[1998]---> BDD-cost:    7
c ---[1996]---> BDD-cost:    7
c ---[1994]---> BDD-cost:    7
c ---[1992]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    7
c ---[1988]---> BDD-cost:    7
c ---[1986]---> BDD-cost:    7
c ---[1984]---> BDD-cost:    7
c ---[1982]---> BDD-cost:    7
c ---[1980]---> BDD-cost:    7
c ---[1978]---> BDD-cost:    7
c ---[1976]---> BDD-cost:    7
c ---[1974]---> BDD-cost:    7
c ---[1972]---> BDD-cost:    7
c ---[1970]---> BDD-cost:    7
c ---[1968]---> BDD-cost:    7
c ---[1966]---> BDD-cost:    7
c ---[1964]---> BDD-cost:    7
c ---[1962]---> BDD-cost:    7
c ---[1960]---> BDD-cost:    7
c ---[1958]---> BDD-cost:    7
c ---[1956]---> BDD-cost:    7
c ---[1954]---> BDD-cost:    7
c ---[1952]---> BDD-cost:    7
c ---[1950]---> BDD-cost:    7
c ---[1948]---> BDD-cost:    7
c ---[1946]---> BDD-cost:    7
c ---[1944]---> BDD-cost:    7
c ---[1942]---> BDD-cost:    7
c ---[1940]---> BDD-cost:    7
c ---[1938]---> BDD-cost:    7
c ---[1936]---> BDD-cost:    7
c ---[1934]---> BDD-cost:    7
c ---[1932]---> BDD-cost:    7
c ---[1931]---> BDD-cost:    7
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:    7
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:    7
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1923]---> BDD-cost:    7
c ---[1922]---> BDD-cost:    7
c ---[1921]---> BDD-cost:    7
c ---[1920]---> BDD-cost:    7
c ---[1919]---> BDD-cost:    9
c ---[1918]---> BDD-cost:    2
c ---[1917]---> BDD-cost:    9
c ---[1916]---> BDD-cost:    2
c ---[1915]---> BDD-cost:    9
c ---[1914]---> BDD-cost:    2
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    2
c ---[1911]---> BDD-cost:    8
c ---[1910]---> BDD-cost:    2
c ---[1909]---> BDD-cost:    8
c ---[1908]---> BDD-cost:    2
c ---[1907]---> BDD-cost:    8
c ---[1906]---> BDD-cost:    2
c ---[1905]---> BDD-cost:    8
c ---[1904]---> BDD-cost:    2
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:    2
c ---[1901]---> BDD-cost:    7
c ---[1900]---> BDD-cost:    2
c ---[1899]---> BDD-cost:    7
c ---[1898]---> BDD-cost:    2
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:    2
c ---[1895]---> BDD-cost:    6
c ---[1894]---> BDD-cost:    2
c ---[1893]---> BDD-cost:    6
c ---[1892]---> BDD-cost:    2
c ---[1891]---> BDD-cost:    6
c ---[1890]---> BDD-cost:    2
c ---[1889]---> BDD-cost:    6
c ---[1888]---> BDD-cost:    2
c ---[1887]---> BDD-cost:    5
c ---[1886]---> BDD-cost:    2
c ---[1885]---> BDD-cost:    5
c ---[1884]---> BDD-cost:    2
c ---[1883]---> BDD-cost:    5
c ---[1882]---> BDD-cost:    2
c ---[1881]---> BDD-cost:    5
c ---[1880]---> BDD-cost:    2
c ---[1879]---> BDD-cost:    4
c ---[1878]---> BDD-cost:    2
c ---[1877]---> BDD-cost:    4
c ---[1876]---> BDD-cost:    2
c ---[1875]---> BDD-cost:    4
c ---[1874]---> BDD-cost:    2
c ---[1873]---> BDD-cost:    4
c ---[1872]---> BDD-cost:    2
c ---[1871]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    2
c ---[1869]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    2
c ---[1867]---> BDD-cost:    3
c ---[1866]---> BDD-cost:    2
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    2
c ---[1855]---> BDD-cost:    6
c ---[1854]---> BDD-cost:    2
c ---[1853]---> BDD-cost:    2
c ---[1852]---> BDD-cost:    2
c ---[1851]---> BDD-cost:    2
c ---[1850]---> BDD-cost:    2
c ---[1849]---> BDD-cost:    2
c ---[1848]---> BDD-cost:    2
c ---[1847]---> BDD-cost:    5
c ---[1846]---> BDD-cost:    2
c ---[1845]---> BDD-cost:    2
c ---[1844]---> BDD-cost:    2
c ---[1843]---> BDD-cost:    2
c ---[1842]---> BDD-cost:    2
c ---[1841]---> BDD-cost:    2
c ---[1840]---> BDD-cost:    2
c ---[1839]---> BDD-cost:    4
c ---[1838]---> BDD-cost:    2
c ---[1837]---> BDD-cost:    2
c ---[1836]---> BDD-cost:    2
c ---[1835]---> BDD-cost:    2
c ---[1834]---> BDD-cost:    2
c ---[1833]---> BDD-cost:    2
c ---[1832]---> BDD-cost:    2
c ---[1831]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    2
c ---[1829]---> BDD-cost:    2
c ---[1828]---> BDD-cost:    2
c ---[1827]---> BDD-cost:    2
c ---[1826]---> BDD-cost:    2
c ---[1825]---> BDD-cost:    2
c ---[1824]---> BDD-cost:    2
c ---[1823]---> BDD-cost:    2
c ---[1822]---> BDD-cost:    2
c ---[1821]---> BDD-cost:    2
c ---[1820]---> BDD-cost:    2
c ---[1819]---> BDD-cost:    2
c ---[1818]---> BDD-cost:    2
c ---[1817]---> BDD-cost:    2
c ---[1816]---> BDD-cost:    2
c ---[1815]---> BDD-cost:    4
c ---[1814]---> BDD-cost:    2
c ---[1813]---> BDD-cost:    2
c ---[1812]---> BDD-cost:    2
c ---[1811]---> BDD-cost:    2
c ---[1810]---> BDD-cost:    2
c ---[1809]---> BDD-cost:    2
c ---[1808]---> BDD-cost:    2
c ---[1807]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    2
c ---[1805]---> BDD-cost:    2
c ---[1804]---> BDD-cost:    2
c ---[1803]---> BDD-cost:    2
c ---[1802]---> BDD-cost:    2
c ---[1801]---> BDD-cost:    2
c ---[1800]---> BDD-cost:    2
c ---[1791]---> BDD-cost:    2
c ---[1790]---> BDD-cost:    2
c ---[1789]---> BDD-cost:    2
c ---[1788]---> BDD-cost:    2
c ---[1787]---> BDD-cost:    2
c ---[1786]---> BDD-cost:    2
c ---[1785]---> BDD-cost:    2
c ---[1784]---> BDD-cost:    2
c ---[1783]---> BDD-cost:    2
c ---[1782]---> BDD-cost:    2
c ---[1781]---> BDD-cost:    2
c ---[1780]---> BDD-cost:    2
c ---[1779]---> BDD-cost:    2
c ---[1778]---> BDD-cost:    2
c ---[1777]---> BDD-cost:    2
c ---[1776]---> BDD-cost:    2
c ---[1775]---> BDD-cost:    2
c ---[1774]---> BDD-cost:    2
c ---[1773]---> BDD-cost:    2
c ---[1772]---> BDD-cost:    2
c ---[1771]---> BDD-cost:    2
c ---[1770]---> BDD-cost:    2
c ---[1769]---> BDD-cost:    2
c ---[1768]---> BDD-cost:    2
c ---[1767]---> BDD-cost:    2
c ---[1766]---> BDD-cost:    2
c ---[1765]---> BDD-cost:    2
c ---[1764]---> BDD-cost:    2
c ---[1763]---> BDD-cost:    2
c ---[1762]---> BDD-cost:    2
c ---[1761]---> BDD-cost:    2
c ---[1760]---> BDD-cost:    2
c ---[1759]---> BDD-cost:    2
c ---[1758]---> BDD-cost:    2
c ---[1757]---> BDD-cost:    2
c ---[1756]---> BDD-cost:    2
c ---[1755]---> BDD-cost:    2
c ---[1754]---> BDD-cost:    2
c ---[1753]---> BDD-cost:    2
c ---[1752]---> BDD-cost:    2
c ---[1751]---> BDD-cost:    2
c ---[1750]---> BDD-cost:    2
c ---[1749]---> BDD-cost:    2
c ---[1748]---> BDD-cost:    2
c ---[1747]---> BDD-cost:    2
c ---[1746]---> BDD-cost:    2
c ---[1745]---> BDD-cost:    2
c ---[1744]---> BDD-cost:    2
c ---[1743]---> BDD-cost:    2
c ---[1742]---> BDD-cost:    2
c ---[1741]---> BDD-cost:    2
c ---[1740]---> BDD-cost:    2
c ---[1739]---> BDD-cost:    2
c ---[1738]---> BDD-cost:    2
c ---[1737]---> BDD-cost:    2
c ---[1736]---> BDD-cost:    2
c ---[1727]---> BDD-cost:    2
c ---[1726]---> BDD-cost:    2
c ---[1725]---> BDD-cost:    2
c ---[1724]---> BDD-cost:    2
c ---[1723]---> BDD-cost:    2
c ---[1722]---> BDD-cost:    2
c ---[1721]---> BDD-cost:    2
c ---[1720]---> BDD-cost:    2
c ---[1719]---> BDD-cost:    2
c ---[1718]---> BDD-cost:    2
c ---[1717]---> BDD-cost:    2
c ---[1716]---> BDD-cost:    2
c ---[1715]---> BDD-cost:    2
c ---[1714]---> BDD-cost:    2
c ---[1713]---> BDD-cost:    2
c ---[1712]---> BDD-cost:    2
c ---[1711]---> BDD-cost:    2
c ---[1710]---> BDD-cost:    2
c ---[1709]---> BDD-cost:    2
c ---[1708]---> BDD-cost:    2
c ---[1707]---> BDD-cost:    2
c ---[1706]---> BDD-cost:    2
c ---[1705]---> BDD-cost:    2
c ---[1704]---> BDD-cost:    2
c ---[1703]---> BDD-cost:    2
c ---[1702]---> BDD-cost:    2
c ---[1701]---> BDD-cost:    2
c ---[1700]---> BDD-cost:    2
c ---[1699]---> BDD-cost:    2
c ---[1698]---> BDD-cost:    2
c ---[1697]---> BDD-cost:    2
c ---[1696]---> BDD-cost:    2
c ---[1695]---> BDD-cost:    2
c ---[1694]---> BDD-cost:    2
c ---[1693]---> BDD-cost:    2
c ---[1692]---> BDD-cost:    2
c ---[1691]---> BDD-cost:    2
c ---[1690]---> BDD-cost:    2
c ---[1689]---> BDD-cost:    2
c ---[1688]---> BDD-cost:    2
c ---[1687]---> BDD-cost:    2
c ---[1686]---> BDD-cost:    2
c ---[1685]---> BDD-cost:    2
c ---[1684]---> BDD-cost:    2
c ---[1683]---> BDD-cost:    2
c ---[1682]---> BDD-cost:    2
c ---[1681]---> BDD-cost:    2
c ---[1680]---> BDD-cost:    2
c ---[1679]---> BDD-cost:    2
c ---[1678]---> BDD-cost:    2
c ---[1677]---> BDD-cost:    2
c ---[1676]---> BDD-cost:    2
c ---[1675]---> BDD-cost:    2
c ---[1674]---> BDD-cost:    2
c ---[1673]---> BDD-cost:    2
c ---[1672]---> BDD-cost:    2
c ---[1663]---> BDD-cost:    2
c ---[1662]---> BDD-cost:    2
c ---[1661]---> BDD-cost:    2
c ---[1660]---> BDD-cost:    2
c ---[1659]---> BDD-cost:    2
c ---[1658]---> BDD-cost:    2
c ---[1657]---> BDD-cost:    2
c ---[1656]---> BDD-cost:    2
c ---[1655]---> BDD-cost:    2
c ---[1654]---> BDD-cost:    2
c ---[1653]---> BDD-cost:    2
c ---[1652]---> BDD-cost:    2
c ---[1651]---> BDD-cost:    2
c ---[1650]---> BDD-cost:    2
c ---[1649]---> BDD-cost:    2
c ---[1648]---> BDD-cost:    2
c ---[1647]---> BDD-cost:    2
c ---[1646]---> BDD-cost:    2
c ---[1645]---> BDD-cost:    2
c ---[1644]---> BDD-cost:    2
c ---[1643]---> BDD-cost:    2
c ---[1642]---> BDD-cost:    2
c ---[1641]---> BDD-cost:    2
c ---[1640]---> BDD-cost:    2
c ---[1639]---> BDD-cost:    2
c ---[1638]---> BDD-cost:    2
c ---[1637]---> BDD-cost:    2
c ---[1636]---> BDD-cost:    2
c ---[1635]---> BDD-cost:    2
c ---[1634]---> BDD-cost:    2
c ---[1633]---> BDD-cost:    2
c ---[1632]---> BDD-cost:    2
c ---[1631]---> BDD-cost:    2
c ---[1630]---> BDD-cost:    2
c ---[1629]---> BDD-cost:    2
c ---[1628]---> BDD-cost:    2
c ---[1627]---> BDD-cost:    2
c ---[1626]---> BDD-cost:    2
c ---[1625]---> BDD-cost:    2
c ---[1624]---> BDD-cost:    2
c ---[1623]---> BDD-cost:    2
c ---[1622]---> BDD-cost:    2
c ---[1621]---> BDD-cost:    2
c ---[1620]---> BDD-cost:    2
c ---[1619]---> BDD-cost:    2
c ---[1618]---> BDD-cost:    2
c ---[1617]---> BDD-cost:    2
c ---[1616]---> BDD-cost:    2
c ---[1615]---> BDD-cost:    2
c ---[1614]---> BDD-cost:    2
c ---[1613]---> BDD-cost:    2
c ---[1612]---> BDD-cost:    2
c ---[1611]---> BDD-cost:    2
c ---[1610]---> BDD-cost:    2
c ---[1609]---> BDD-cost:    2
c ---[1608]---> BDD-cost:    2
c ---[1599]---> BDD-cost:    9
c ---[1598]---> BDD-cost:    2
c ---[1597]---> BDD-cost:    9
c ---[1596]---> BDD-cost:    2
c ---[1595]---> BDD-cost:    9
c ---[1594]---> BDD-cost:    2
c ---[1593]---> BDD-cost:    9
c ---[1592]---> BDD-cost:    2
c ---[1591]---> BDD-cost:    8
c ---[1590]---> BDD-cost:    2
c ---[1589]---> BDD-cost:    8
c ---[1588]---> BDD-cost:    2
c ---[1587]---> BDD-cost:    8
c ---[1586]---> BDD-cost:    2
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    2
c ---[1583]---> BDD-cost:    7
c ---[1582]---> BDD-cost:    2
c ---[1581]---> BDD-cost:    7
c ---[1580]---> BDD-cost:    2
c ---[1579]---> BDD-cost:    7
c ---[1578]---> BDD-cost:    2
c ---[1577]---> BDD-cost:    7
c ---[1576]---> BDD-cost:    2
c ---[1575]---> BDD-cost:    6
c ---[1574]---> BDD-cost:    2
c ---[1573]---> BDD-cost:    6
c ---[1572]---> BDD-cost:    2
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    2
c ---[1569]---> BDD-cost:    6
c ---[1568]---> BDD-cost:    2
c ---[1567]---> BDD-cost:    5
c ---[1566]---> BDD-cost:    2
c ---[1565]---> BDD-cost:    5
c ---[1564]---> BDD-cost:    2
c ---[1563]---> BDD-cost:    5
c ---[1562]---> BDD-cost:    2
c ---[1561]---> BDD-cost:    5
c ---[1560]---> BDD-cost:    2
c ---[1559]---> BDD-cost:    4
c ---[1558]---> BDD-cost:    2
c ---[1557]---> BDD-cost:    4
c ---[1556]---> BDD-cost:    2
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    2
c ---[1553]---> BDD-cost:    4
c ---[1552]---> BDD-cost:    2
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    2
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    2
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    2
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    2
c ---[1535]---> BDD-cost:    6
c ---[1534]---> BDD-cost:    2
c ---[1533]---> BDD-cost:    2
c ---[1532]---> BDD-cost:    2
c ---[1531]---> BDD-cost:    2
c ---[1530]---> BDD-cost:    2
c ---[1529]---> BDD-cost:    2
c ---[1528]---> BDD-cost:    2
c ---[1527]---> BDD-cost:    5
c ---[1526]---> BDD-cost:    2
c ---[1525]---> BDD-cost:    2
c ---[1524]---> BDD-cost:    2
c ---[1523]---> BDD-cost:    2
c ---[1522]---> BDD-cost:    2
c ---[1521]---> BDD-cost:    2
c ---[1520]---> BDD-cost:    2
c ---[1519]---> BDD-cost:    4
c ---[1518]---> BDD-cost:    2
c ---[1517]---> BDD-cost:    2
c ---[1516]---> BDD-cost:    2
c ---[1515]---> BDD-cost:    2
c ---[1514]---> BDD-cost:    2
c ---[1513]---> BDD-cost:    2
c ---[1512]---> BDD-cost:    2
c ---[1511]---> BDD-cost:    3
c ---[1510]---> BDD-cost:    2
c ---[1509]---> BDD-cost:    2
c ---[1508]---> BDD-cost:    2
c ---[1507]---> BDD-cost:    2
c ---[1506]---> BDD-cost:    2
c ---[1505]---> BDD-cost:    2
c ---[1504]---> BDD-cost:    2
c ---[1503]---> BDD-cost:    2
c ---[1502]---> BDD-cost:    2
c ---[1501]---> BDD-cost:    2
c ---[1500]---> BDD-cost:    2
c ---[1499]---> BDD-cost:    2
c ---[1498]---> BDD-cost:    2
c ---[1497]---> BDD-cost:    2
c ---[1496]---> BDD-cost:    2
c ---[1495]---> BDD-cost:    4
c ---[1494]---> BDD-cost:    2
c ---[1493]---> BDD-cost:    2
c ---[1492]---> BDD-cost:    2
c ---[1491]---> BDD-cost:    2
c ---[1490]---> BDD-cost:    2
c ---[1489]---> BDD-cost:    2
c ---[1488]---> BDD-cost:    2
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    2
c ---[1485]---> BDD-cost:    2
c ---[1484]---> BDD-cost:    2
c ---[1483]---> BDD-cost:    2
c ---[1482]---> BDD-cost:    2
c ---[1481]---> BDD-cost:    2
c ---[1480]---> BDD-cost:    2
c ---[1471]---> BDD-cost:    2
c ---[1470]---> BDD-cost:    2
c ---[1469]---> BDD-cost:    2
c ---[1468]---> BDD-cost:    2
c ---[1467]---> BDD-cost:    2
c ---[1466]---> BDD-cost:    2
c ---[1465]---> BDD-cost:    2
c ---[1464]---> BDD-cost:    2
c ---[1463]---> BDD-cost:    2
c ---[1462]---> BDD-cost:    2
c ---[1461]---> BDD-cost:    2
c ---[1460]---> BDD-cost:    2
c ---[1459]---> BDD-cost:    2
c ---[1458]---> BDD-cost:    2
c ---[1457]---> BDD-cost:    2
c ---[1456]---> BDD-cost:    2
c ---[1455]---> BDD-cost:    2
c ---[1454]---> BDD-cost:    2
c ---[1453]---> BDD-cost:    2
c ---[1452]---> BDD-cost:    2
c ---[1451]---> BDD-cost:    2
c ---[1450]---> BDD-cost:    2
c ---[1449]---> BDD-cost:    2
c ---[1448]---> BDD-cost:    2
c ---[1447]---> BDD-cost:    2
c ---[1446]---> BDD-cost:    2
c ---[1445]---> BDD-cost:    2
c ---[1444]---> BDD-cost:    2
c ---[1443]---> BDD-cost:    2
c ---[1442]---> BDD-cost:    2
c ---[1441]---> BDD-cost:    2
c ---[1440]---> BDD-cost:    2
c ---[1439]---> BDD-cost:    2
c ---[1438]---> BDD-cost:    2
c ---[1437]---> BDD-cost:    2
c ---[1436]---> BDD-cost:    2
c ---[1435]---> BDD-cost:    2
c ---[1434]---> BDD-cost:    2
c ---[1433]---> BDD-cost:    2
c ---[1432]---> BDD-cost:    2
c ---[1431]---> BDD-cost:    2
c ---[1430]---> BDD-cost:    2
c ---[1429]---> BDD-cost:    2
c ---[1428]---> BDD-cost:    2
c ---[1427]---> BDD-cost:    2
c ---[1426]---> BDD-cost:    2
c ---[1425]---> BDD-cost:    2
c ---[1424]---> BDD-cost:    2
c ---[1423]---> BDD-cost:    2
c ---[1422]---> BDD-cost:    2
c ---[1421]---> BDD-cost:    2
c ---[1420]---> BDD-cost:    2
c ---[1419]---> BDD-cost:    2
c ---[1418]---> BDD-cost:    2
c ---[1417]---> BDD-cost:    2
c ---[1416]---> BDD-cost:    2
c ---[1407]---> BDD-cost:    2
c ---[1406]---> BDD-cost:    2
c ---[1405]---> BDD-cost:    2
c ---[1404]---> BDD-cost:    2
c ---[1403]---> BDD-cost:    2
c ---[1402]---> BDD-cost:    2
c ---[1401]---> BDD-cost:    2
c ---[1400]---> BDD-cost:    2
c ---[1399]---> BDD-cost:    2
c ---[1398]---> BDD-cost:    2
c ---[1397]---> BDD-cost:    2
c ---[1396]---> BDD-cost:    2
c ---[1395]---> BDD-cost:    2
c ---[1394]---> BDD-cost:    2
c ---[1393]---> BDD-cost:    2
c ---[1392]---> BDD-cost:    2
c ---[1391]---> BDD-cost:    2
c ---[1390]---> BDD-cost:    2
c ---[1389]---> BDD-cost:    2
c ---[1388]---> BDD-cost:    2
c ---[1387]---> BDD-cost:    2
c ---[1386]---> BDD-cost:    2
c ---[1385]---> BDD-cost:    2
c ---[1384]---> BDD-cost:    2
c ---[1383]---> BDD-cost:    2
c ---[1382]---> BDD-cost:    2
c ---[1381]---> BDD-cost:    2
c ---[1380]---> BDD-cost:    2
c ---[1379]---> BDD-cost:    2
c ---[1378]---> BDD-cost:    2
c ---[1377]---> BDD-cost:    2
c ---[1376]---> BDD-cost:    2
c ---[1375]---> BDD-cost:    2
c ---[1374]---> BDD-cost:    2
c ---[1373]---> BDD-cost:    2
c ---[1372]---> BDD-cost:    2
c ---[1371]---> BDD-cost:    2
c ---[1370]---> BDD-cost:    2
c ---[1369]---> BDD-cost:    2
c ---[1368]---> BDD-cost:    2
c ---[1367]---> BDD-cost:    2
c ---[1366]---> BDD-cost:    2
c ---[1365]---> BDD-cost:    2
c ---[1364]---> BDD-cost:    2
c ---[1363]---> BDD-cost:    2
c ---[1362]---> BDD-cost:    2
c ---[1361]---> BDD-cost:    2
c ---[1360]---> BDD-cost:    2
c ---[1359]---> BDD-cost:    2
c ---[1358]---> BDD-cost:    2
c ---[1357]---> BDD-cost:    2
c ---[1356]---> BDD-cost:    2
c ---[1355]---> BDD-cost:    2
c ---[1354]---> BDD-cost:    2
c ---[1353]---> BDD-cost:    2
c ---[1352]---> BDD-cost:    2
c ---[1343]---> BDD-cost:    2
c ---[1342]---> BDD-cost:    2
c ---[1341]---> BDD-cost:    2
c ---[1340]---> BDD-cost:    2
c ---[1339]---> BDD-cost:    2
c ---[1338]---> BDD-cost:    2
c ---[1337]---> BDD-cost:    2
c ---[1336]---> BDD-cost:    2
c ---[1335]---> BDD-cost:    2
c ---[1334]---> BDD-cost:    2
c ---[1333]---> BDD-cost:    2
c ---[1332]---> BDD-cost:    2
c ---[1331]---> BDD-cost:    2
c ---[1330]---> BDD-cost:    2
c ---[1329]---> BDD-cost:    2
c ---[1328]---> BDD-cost:    2
c ---[1327]---> BDD-cost:    2
c ---[1326]---> BDD-cost:    2
c ---[1325]---> BDD-cost:    2
c ---[1324]---> BDD-cost:    2
c ---[1323]---> BDD-cost:    2
c ---[1322]---> BDD-cost:    2
c ---[1321]---> BDD-cost:    2
c ---[1320]---> BDD-cost:    2
c ---[1319]---> BDD-cost:    2
c ---[1318]---> BDD-cost:    2
c ---[1317]---> BDD-cost:    2
c ---[1316]---> BDD-cost:    2
c ---[1315]---> BDD-cost:    2
c ---[1314]---> BDD-cost:    2
c ---[1313]---> BDD-cost:    2
c ---[1312]---> BDD-cost:    2
c ---[1311]---> BDD-cost:    2
c ---[1310]---> BDD-cost:    2
c ---[1309]---> BDD-cost:    2
c ---[1308]---> BDD-cost:    2
c ---[1307]---> BDD-cost:    2
c ---[1306]---> BDD-cost:    2
c ---[1305]---> BDD-cost:    2
c ---[1304]---> BDD-cost:    2
c ---[1303]---> BDD-cost:    2
c ---[1302]---> BDD-cost:    2
c ---[1301]---> BDD-cost:    2
c ---[1300]---> BDD-cost:    2
c ---[1299]---> BDD-cost:    2
c ---[1298]---> BDD-cost:    2
c ---[1297]---> BDD-cost:    2
c ---[1296]---> BDD-cost:    2
c ---[1295]---> BDD-cost:    2
c ---[1294]---> BDD-cost:    2
c ---[1293]---> BDD-cost:    2
c ---[1292]---> BDD-cost:    2
c ---[1291]---> BDD-cost:    2
c ---[1290]---> BDD-cost:    2
c ---[1289]---> BDD-cost:    2
c ---[1288]---> BDD-cost:    2
c ---[1279]---> BDD-cost:    9
c ---[1278]---> BDD-cost:    2
c ---[1277]---> BDD-cost:    9
c ---[1276]---> BDD-cost:    2
c ---[1275]---> BDD-cost:    9
c ---[1274]---> BDD-cost:    2
c ---[1273]---> BDD-cost:    9
c ---[1272]---> BDD-cost:    2
c ---[1271]---> BDD-cost:    8
c ---[1270]---> BDD-cost:    2
c ---[1269]---> BDD-cost:    8
c ---[1268]---> BDD-cost:    2
c ---[1267]---> BDD-cost:    8
c ---[1266]---> BDD-cost:    2
c ---[1265]---> BDD-cost:    8
c ---[1264]---> BDD-cost:    2
c ---[1263]---> BDD-cost:    7
c ---[1262]---> BDD-cost:    2
c ---[1261]---> BDD-cost:    7
c ---[1260]---> BDD-cost:    2
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    2
c ---[1257]---> BDD-cost:    7
c ---[1256]---> BDD-cost:    2
c ---[1255]---> BDD-cost:    6
c ---[1254]---> BDD-cost:    2
c ---[1253]---> BDD-cost:    6
c ---[1252]---> BDD-cost:    2
c ---[1251]---> BDD-cost:    6
c ---[1250]---> BDD-cost:    2
c ---[1249]---> BDD-cost:    6
c ---[1248]---> BDD-cost:    2
c ---[1247]---> BDD-cost:    5
c ---[1246]---> BDD-cost:    2
c ---[1245]---> BDD-cost:    5
c ---[1244]---> BDD-cost:    2
c ---[1243]---> BDD-cost:    5
c ---[1242]---> BDD-cost:    2
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    2
c ---[1239]---> BDD-cost:    4
c ---[1238]---> BDD-cost:    2
c ---[1237]---> BDD-cost:    4
c ---[1236]---> BDD-cost:    2
c ---[1235]---> BDD-cost:    4
c ---[1234]---> BDD-cost:    2
c ---[1233]---> BDD-cost:    4
c ---[1232]---> BDD-cost:    2
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    2
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    2
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    2
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    2
c ---[1215]---> BDD-cost:    6
c ---[1214]---> BDD-cost:    2
c ---[1213]---> BDD-cost:    2
c ---[1212]---> BDD-cost:    2
c ---[1211]---> BDD-cost:    2
c ---[1210]---> BDD-cost:    2
c ---[1209]---> BDD-cost:    2
c ---[1208]---> BDD-cost:    2
c ---[1207]---> BDD-cost:    5
c ---[1206]---> BDD-cost:    2
c ---[1205]---> BDD-cost:    2
c ---[1204]---> BDD-cost:    2
c ---[1203]---> BDD-cost:    2
c ---[1202]---> BDD-cost:    2
c ---[1201]---> BDD-cost:    2
c ---[1200]---> BDD-cost:    2
c ---[1199]---> BDD-cost:    4
c ---[1198]---> BDD-cost:    2
c ---[1197]---> BDD-cost:    2
c ---[1196]---> BDD-cost:    2
c ---[1195]---> BDD-cost:    2
c ---[1194]---> BDD-cost:    2
c ---[1193]---> BDD-cost:    2
c ---[1192]---> BDD-cost:    2
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    2
c ---[1189]---> BDD-cost:    2
c ---[1188]---> BDD-cost:    2
c ---[1187]---> BDD-cost:    2
c ---[1186]---> BDD-cost:    2
c ---[1185]---> BDD-cost:    2
c ---[1184]---> BDD-cost:    2
c ---[1183]---> BDD-cost:    2
c ---[1182]---> BDD-cost:    2
c ---[1181]---> BDD-cost:    2
c ---[1180]---> BDD-cost:    2
c ---[1179]---> BDD-cost:    2
c ---[1178]---> BDD-cost:    2
c ---[1177]---> BDD-cost:    2
c ---[1176]---> BDD-cost:    2
c ---[1175]---> BDD-cost:    4
c ---[1174]---> BDD-cost:    2
c ---[1173]---> BDD-cost:    2
c ---[1172]---> BDD-cost:    2
c ---[1171]---> BDD-cost:    2
c ---[1170]---> BDD-cost:    2
c ---[1169]---> BDD-cost:    2
c ---[1168]---> BDD-cost:    2
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    2
c ---[1165]---> BDD-cost:    2
c ---[1164]---> BDD-cost:    2
c ---[1163]---> BDD-cost:    2
c ---[1162]---> BDD-cost:    2
c ---[1161]---> BDD-cost:    2
c ---[1160]---> BDD-cost:    2
c ---[1151]---> BDD-cost:    2
c ---[1150]---> BDD-cost:    2
c ---[1149]---> BDD-cost:    2
c ---[1148]---> BDD-cost:    2
c ---[1147]---> BDD-cost:    2
c ---[1146]---> BDD-cost:    2
c ---[1145]---> BDD-cost:    2
c ---[1144]---> BDD-cost:    2
c ---[1143]---> BDD-cost:    2
c ---[1142]---> BDD-cost:    2
c ---[1141]---> BDD-cost:    2
c ---[1140]---> BDD-cost:    2
c ---[1139]---> BDD-cost:    2
c ---[1138]---> BDD-cost:    2
c ---[1137]---> BDD-cost:    2
c ---[1136]---> BDD-cost:    2
c ---[1135]---> BDD-cost:    2
c ---[1134]---> BDD-cost:    2
c ---[1133]---> BDD-cost:    2
c ---[1132]---> BDD-cost:    2
c ---[1131]---> BDD-cost:    2
c ---[1130]---> BDD-cost:    2
c ---[1129]---> BDD-cost:    2
c ---[1128]---> BDD-cost:    2
c ---[1127]---> BDD-cost:    2
c ---[1126]---> BDD-cost:    2
c ---[1125]---> BDD-cost:    2
c ---[1124]---> BDD-cost:    2
c ---[1123]---> BDD-cost:    2
c ---[1122]---> BDD-cost:    2
c ---[1121]---> BDD-cost:    2
c ---[1120]---> BDD-cost:    2
c ---[1119]---> BDD-cost:    2
c ---[1118]---> BDD-cost:    2
c ---[1117]---> BDD-cost:    2
c ---[1116]---> BDD-cost:    2
c ---[1115]---> BDD-cost:    2
c ---[1114]---> BDD-cost:    2
c ---[1113]---> BDD-cost:    2
c ---[1112]---> BDD-cost:    2
c ---[1111]---> BDD-cost:    2
c ---[1110]---> BDD-cost:    2
c ---[1109]---> BDD-cost:    2
c ---[1108]---> BDD-cost:    2
c ---[1107]---> BDD-cost:    2
c ---[1106]---> BDD-cost:    2
c ---[1105]---> BDD-cost:    2
c ---[1104]---> BDD-cost:    2
c ---[1103]---> BDD-cost:    2
c ---[1102]---> BDD-cost:    2
c ---[1101]---> BDD-cost:    2
c ---[1100]---> BDD-cost:    2
c ---[1099]---> BDD-cost:    2
c ---[1098]---> BDD-cost:    2
c ---[1097]---> BDD-cost:    2
c ---[1096]---> BDD-cost:    2
c ---[1087]---> BDD-cost:    2
c ---[1086]---> BDD-cost:    2
c ---[1085]---> BDD-cost:    2
c ---[1084]---> BDD-cost:    2
c ---[1083]---> BDD-cost:    2
c ---[1082]---> BDD-cost:    2
c ---[1081]---> BDD-cost:    2
c ---[1080]---> BDD-cost:    2
c ---[1079]---> BDD-cost:    2
c ---[1078]---> BDD-cost:    2
c ---[1077]---> BDD-cost:    2
c ---[1076]---> BDD-cost:    2
c ---[1075]---> BDD-cost:    2
c ---[1074]---> BDD-cost:    2
c ---[1073]---> BDD-cost:    2
c ---[1072]---> BDD-cost:    2
c ---[1071]---> BDD-cost:    2
c ---[1070]---> BDD-cost:    2
c ---[1069]---> BDD-cost:    2
c ---[1068]---> BDD-cost:    2
c ---[1067]---> BDD-cost:    2
c ---[1066]---> BDD-cost:    2
c ---[1065]---> BDD-cost:    2
c ---[1064]---> BDD-cost:    2
c ---[1063]---> BDD-cost:    2
c ---[1062]---> BDD-cost:    2
c ---[1061]---> BDD-cost:    2
c ---[1060]---> BDD-cost:    2
c ---[1059]---> BDD-cost:    2
c ---[1058]---> BDD-cost:    2
c ---[1057]---> BDD-cost:    2
c ---[1056]---> BDD-cost:    2
c ---[1055]---> BDD-cost:    2
c ---[1054]---> BDD-cost:    2
c ---[1053]---> BDD-cost:    2
c ---[1052]---> BDD-cost:    2
c ---[1051]---> BDD-cost:    2
c ---[1050]---> BDD-cost:    2
c ---[1049]---> BDD-cost:    2
c ---[1048]---> BDD-cost:    2
c ---[1047]---> BDD-cost:    2
c ---[1046]---> BDD-cost:    2
c ---[1045]---> BDD-cost:    2
c ---[1044]---> BDD-cost:    2
c ---[1043]---> BDD-cost:    2
c ---[1042]---> BDD-cost:    2
c ---[1041]---> BDD-cost:    2
c ---[1040]---> BDD-cost:    2
c ---[1039]---> BDD-cost:    2
c ---[1038]---> BDD-cost:    2
c ---[1037]---> BDD-cost:    2
c ---[1036]---> BDD-cost:    2
c ---[1035]---> BDD-cost:    2
c ---[1034]---> BDD-cost:    2
c ---[1033]---> BDD-cost:    2
c ---[1032]---> BDD-cost:    2
c ---[1023]---> BDD-cost:    2
c ---[1022]---> BDD-cost:    2
c ---[1021]---> BDD-cost:    2
c ---[1020]---> BDD-cost:    2
c ---[1019]---> BDD-cost:    2
c ---[1018]---> BDD-cost:    2
c ---[1017]---> BDD-cost:    2
c ---[1016]---> BDD-cost:    2
c ---[1015]---> BDD-cost:    2
c ---[1014]---> BDD-cost:    2
c ---[1013]---> BDD-cost:    2
c ---[1012]---> BDD-cost:    2
c ---[1011]---> BDD-cost:    2
c ---[1010]---> BDD-cost:    2
c ---[1009]---> BDD-cost:    2
c ---[1008]---> BDD-cost:    2
c ---[1007]---> BDD-cost:    2
c ---[1006]---> BDD-cost:    2
c ---[1005]---> BDD-cost:    2
c ---[1004]---> BDD-cost:    2
c ---[1003]---> BDD-cost:    2
c ---[1002]---> BDD-cost:    2
c ---[1001]---> BDD-cost:    2
c ---[1000]---> BDD-cost:    2
c ---[ 999]---> BDD-cost:    2
c ---[ 998]---> BDD-cost:    2
c ---[ 997]---> BDD-cost:    2
c ---[ 996]---> BDD-cost:    2
c ---[ 995]---> BDD-cost:    2
c ---[ 994]---> BDD-cost:    2
c ---[ 993]---> BDD-cost:    2
c ---[ 992]---> BDD-cost:    2
c ---[ 991]---> BDD-cost:    2
c ---[ 990]---> BDD-cost:    2
c ---[ 989]---> BDD-cost:    2
c ---[ 988]---> BDD-cost:    2
c ---[ 987]---> BDD-cost:    2
c ---[ 986]---> BDD-cost:    2
c ---[ 985]---> BDD-cost:    2
c ---[ 984]---> BDD-cost:    2
c ---[ 983]---> BDD-cost:    2
c ---[ 982]---> BDD-cost:    2
c ---[ 981]---> BDD-cost:    2
c ---[ 980]---> BDD-cost:    2
c ---[ 979]---> BDD-cost:    2
c ---[ 978]---> BDD-cost:    2
c ---[ 977]---> BDD-cost:    2
c ---[ 976]---> BDD-cost:    2
c ---[ 975]---> BDD-cost:    2
c ---[ 974]---> BDD-cost:    2
c ---[ 973]---> BDD-cost:    2
c ---[ 972]---> BDD-cost:    2
c ---[ 971]---> BDD-cost:    2
c ---[ 970]---> BDD-cost:    2
c ---[ 969]---> BDD-cost:    2
c ---[ 968]---> BDD-cost:    2
c ---[ 959]---> BDD-cost:    9
c ---[ 958]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    9
c ---[ 956]---> BDD-cost:    2
c ---[ 955]---> BDD-cost:    9
c ---[ 954]---> BDD-cost:    2
c ---[ 953]---> BDD-cost:    9
c ---[ 952]---> BDD-cost:    2
c ---[ 951]---> BDD-cost:    8
c ---[ 950]---> BDD-cost:    2
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    2
c ---[ 947]---> BDD-cost:    8
c ---[ 946]---> BDD-cost:    2
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    2
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    2
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    2
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    2
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    2
c ---[ 935]---> BDD-cost:    6
c ---[ 934]---> BDD-cost:    2
c ---[ 933]---> BDD-cost:    6
c ---[ 932]---> BDD-cost:    2
c ---[ 931]---> BDD-cost:    6
c ---[ 930]---> BDD-cost:    2
c ---[ 929]---> BDD-cost:    6
c ---[ 928]---> BDD-cost:    2
c ---[ 927]---> BDD-cost:    5
c ---[ 926]---> BDD-cost:    2
c ---[ 925]---> BDD-cost:    5
c ---[ 924]---> BDD-cost:    2
c ---[ 923]---> BDD-cost:    5
c ---[ 922]---> BDD-cost:    2
c ---[ 921]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:    2
c ---[ 919]---> BDD-cost:    4
c ---[ 918]---> BDD-cost:    2
c ---[ 917]---> BDD-cost:    4
c ---[ 916]---> BDD-cost:    2
c ---[ 915]---> BDD-cost:    4
c ---[ 914]---> BDD-cost:    2
c ---[ 913]---> BDD-cost:    4
c ---[ 912]---> BDD-cost:    2
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    2
c ---[ 909]---> BDD-cost:    3
c ---[ 908]---> BDD-cost:    2
c ---[ 907]---> BDD-cost:    3
c ---[ 906]---> BDD-cost:    2
c ---[ 905]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    2
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    2
c ---[ 893]---> BDD-cost:    2
c ---[ 892]---> BDD-cost:    2
c ---[ 891]---> BDD-cost:    2
c ---[ 890]---> BDD-cost:    2
c ---[ 889]---> BDD-cost:    2
c ---[ 888]---> BDD-cost:    2
c ---[ 887]---> BDD-cost:    5
c ---[ 886]---> BDD-cost:    2
c ---[ 885]---> BDD-cost:    2
c ---[ 884]---> BDD-cost:    2
c ---[ 883]---> BDD-cost:    2
c ---[ 882]---> BDD-cost:    2
c ---[ 881]---> BDD-cost:    2
c ---[ 880]---> BDD-cost:    2
c ---[ 879]---> BDD-cost:    4
c ---[ 878]---> BDD-cost:    2
c ---[ 877]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    2
c ---[ 875]---> BDD-cost:    2
c ---[ 874]---> BDD-cost:    2
c ---[ 873]---> BDD-cost:    2
c ---[ 872]---> BDD-cost:    2
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    2
c ---[ 869]---> BDD-cost:    2
c ---[ 868]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 866]---> BDD-cost:    2
c ---[ 865]---> BDD-cost:    2
c ---[ 864]---> BDD-cost:    2
c ---[ 863]---> BDD-cost:    2
c ---[ 862]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 859]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    2
c ---[ 857]---> BDD-cost:    2
c ---[ 856]---> BDD-cost:    2
c ---[ 855]---> BDD-cost:    4
c ---[ 854]---> BDD-cost:    2
c ---[ 853]---> BDD-cost:    2
c ---[ 852]---> BDD-cost:    2
c ---[ 851]---> BDD-cost:    2
c ---[ 850]---> BDD-cost:    2
c ---[ 849]---> BDD-cost:    2
c ---[ 848]---> BDD-cost:    2
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 844]---> BDD-cost:    2
c ---[ 843]---> BDD-cost:    2
c ---[ 842]---> BDD-cost:    2
c ---[ 841]---> BDD-cost:    2
c ---[ 840]---> BDD-cost:    2
c ---[ 831]---> BDD-cost:    2
c ---[ 830]---> BDD-cost:    2
c ---[ 829]---> BDD-cost:    2
c ---[ 828]---> BDD-cost:    2
c ---[ 827]---> BDD-cost:    2
c ---[ 826]---> BDD-cost:    2
c ---[ 825]---> BDD-cost:    2
c ---[ 824]---> BDD-cost:    2
c ---[ 823]---> BDD-cost:    2
c ---[ 822]---> BDD-cost:    2
c ---[ 821]---> BDD-cost:    2
c ---[ 820]---> BDD-cost:    2
c ---[ 819]---> BDD-cost:    2
c ---[ 818]---> BDD-cost:    2
c ---[ 817]---> BDD-cost:    2
c ---[ 816]---> BDD-cost:    2
c ---[ 815]---> BDD-cost:    2
c ---[ 814]---> BDD-cost:    2
c ---[ 813]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 811]---> BDD-cost:    2
c ---[ 810]---> BDD-cost:    2
c ---[ 809]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    2
c ---[ 807]---> BDD-cost:    2
c ---[ 806]---> BDD-cost:    2
c ---[ 805]---> BDD-cost:    2
c ---[ 804]---> BDD-cost:    2
c ---[ 803]---> BDD-cost:    2
c ---[ 802]---> BDD-cost:    2
c ---[ 801]---> BDD-cost:    2
c ---[ 800]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 798]---> BDD-cost:    2
c ---[ 797]---> BDD-cost:    2
c ---[ 796]---> BDD-cost:    2
c ---[ 795]---> BDD-cost:    2
c ---[ 794]---> BDD-cost:    2
c ---[ 793]---> BDD-cost:    2
c ---[ 792]---> BDD-cost:    2
c ---[ 791]---> BDD-cost:    2
c ---[ 790]---> BDD-cost:    2
c ---[ 789]---> BDD-cost:    2
c ---[ 788]---> BDD-cost:    2
c ---[ 787]---> BDD-cost:    2
c ---[ 786]---> BDD-cost:    2
c ---[ 785]---> BDD-cost:    2
c ---[ 784]---> BDD-cost:    2
c ---[ 783]---> BDD-cost:    2
c ---[ 782]---> BDD-cost:    2
c ---[ 781]---> BDD-cost:    2
c ---[ 780]---> BDD-cost:    2
c ---[ 779]---> BDD-cost:    2
c ---[ 778]---> BDD-cost:    2
c ---[ 777]---> BDD-cost:    2
c ---[ 776]---> BDD-cost:    2
c ---[ 767]---> BDD-cost:    2
c ---[ 766]---> BDD-cost:    2
c ---[ 765]---> BDD-cost:    2
c ---[ 764]---> BDD-cost:    2
c ---[ 763]---> BDD-cost:    2
c ---[ 762]---> BDD-cost:    2
c ---[ 761]---> BDD-cost:    2
c ---[ 760]---> BDD-cost:    2
c ---[ 759]---> BDD-cost:    2
c ---[ 758]---> BDD-cost:    2
c ---[ 757]---> BDD-cost:    2
c ---[ 756]---> BDD-cost:    2
c ---[ 755]---> BDD-cost:    2
c ---[ 754]---> BDD-cost:    2
c ---[ 753]---> BDD-cost:    2
c ---[ 752]---> BDD-cost:    2
c ---[ 751]---> BDD-cost:    2
c ---[ 750]---> BDD-cost:    2
c ---[ 749]---> BDD-cost:    2
c ---[ 748]---> BDD-cost:    2
c ---[ 747]---> BDD-cost:    2
c ---[ 746]---> BDD-cost:    2
c ---[ 745]---> BDD-cost:    2
c ---[ 744]---> BDD-cost:    2
c ---[ 743]---> BDD-cost:    2
c ---[ 742]---> BDD-cost:    2
c ---[ 741]---> BDD-cost:    2
c ---[ 740]---> BDD-cost:    2
c ---[ 739]---> BDD-cost:    2
c ---[ 738]---> BDD-cost:    2
c ---[ 737]---> BDD-cost:    2
c ---[ 736]---> BDD-cost:    2
c ---[ 735]---> BDD-cost:    2
c ---[ 734]---> BDD-cost:    2
c ---[ 733]---> BDD-cost:    2
c ---[ 732]---> BDD-cost:    2
c ---[ 731]---> BDD-cost:    2
c ---[ 730]---> BDD-cost:    2
c ---[ 729]---> BDD-cost:    2
c ---[ 728]---> BDD-cost:    2
c ---[ 727]---> BDD-cost:    2
c ---[ 726]---> BDD-cost:    2
c ---[ 725]---> BDD-cost:    2
c ---[ 724]---> BDD-cost:    2
c ---[ 723]---> BDD-cost:    2
c ---[ 722]---> BDD-cost:    2
c ---[ 721]---> BDD-cost:    2
c ---[ 720]---> BDD-cost:    2
c ---[ 719]---> BDD-cost:    2
c ---[ 718]---> BDD-cost:    2
c ---[ 717]---> BDD-cost:    2
c ---[ 716]---> BDD-cost:    2
c ---[ 715]---> BDD-cost:    2
c ---[ 714]---> BDD-cost:    2
c ---[ 713]---> BDD-cost:    2
c ---[ 712]---> BDD-cost:    2
c ---[ 703]---> BDD-cost:    2
c ---[ 702]---> BDD-cost:    2
c ---[ 701]---> BDD-cost:    2
c ---[ 700]---> BDD-cost:    2
c ---[ 699]---> BDD-cost:    2
c ---[ 698]---> BDD-cost:    2
c ---[ 697]---> BDD-cost:    2
c ---[ 696]---> BDD-cost:    2
c ---[ 695]---> BDD-cost:    2
c ---[ 694]---> BDD-cost:    2
c ---[ 693]---> BDD-cost:    2
c ---[ 692]---> BDD-cost:    2
c ---[ 691]---> BDD-cost:    2
c ---[ 690]---> BDD-cost:    2
c ---[ 689]---> BDD-cost:    2
c ---[ 688]---> BDD-cost:    2
c ---[ 687]---> BDD-cost:    2
c ---[ 686]---> BDD-cost:    2
c ---[ 685]---> BDD-cost:    2
c ---[ 684]---> BDD-cost:    2
c ---[ 683]---> BDD-cost:    2
c ---[ 682]---> BDD-cost:    2
c ---[ 681]---> BDD-cost:    2
c ---[ 680]---> BDD-cost:    2
c ---[ 679]---> BDD-cost:    2
c ---[ 678]---> BDD-cost:    2
c ---[ 677]---> BDD-cost:    2
c ---[ 676]---> BDD-cost:    2
c ---[ 675]---> BDD-cost:    2
c ---[ 674]---> BDD-cost:    2
c ---[ 673]---> BDD-cost:    2
c ---[ 672]---> BDD-cost:    2
c ---[ 671]---> BDD-cost:    2
c ---[ 670]---> BDD-cost:    2
c ---[ 669]---> BDD-cost:    2
c ---[ 668]---> BDD-cost:    2
c ---[ 667]---> BDD-cost:    2
c ---[ 666]---> BDD-cost:    2
c ---[ 665]---> BDD-cost:    2
c ---[ 664]---> BDD-cost:    2
c ---[ 663]---> BDD-cost:    2
c ---[ 662]---> BDD-cost:    2
c ---[ 661]---> BDD-cost:    2
c ---[ 660]---> BDD-cost:    2
c ---[ 659]---> BDD-cost:    2
c ---[ 658]---> BDD-cost:    2
c ---[ 657]---> BDD-cost:    2
c ---[ 656]---> BDD-cost:    2
c ---[ 655]---> BDD-cost:    2
c ---[ 654]---> BDD-cost:    2
c ---[ 653]---> BDD-cost:    2
c ---[ 652]---> BDD-cost:    2
c ---[ 651]---> BDD-cost:    2
c ---[ 650]---> BDD-cost:    2
c ---[ 649]---> BDD-cost:    2
c ---[ 648]---> BDD-cost:    2
c ---[ 639]---> BDD-cost:    9
c ---[ 638]---> BDD-cost:    2
c ---[ 637]---> BDD-cost:    9
c ---[ 636]---> BDD-cost:    2
c ---[ 635]---> BDD-cost:    9
c ---[ 634]---> BDD-cost:    2
c ---[ 633]---> BDD-cost:    9
c ---[ 632]---> BDD-cost:    2
c ---[ 631]---> BDD-cost:    8
c ---[ 630]---> BDD-cost:    2
c ---[ 629]---> BDD-cost:    8
c ---[ 628]---> BDD-cost:    2
c ---[ 627]---> BDD-cost:    8
c ---[ 626]---> BDD-cost:    2
c ---[ 625]---> BDD-cost:    8
c ---[ 624]---> BDD-cost:    2
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    2
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    2
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    2
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    2
c ---[ 615]---> BDD-cost:    6
c ---[ 614]---> BDD-cost:    2
c ---[ 613]---> BDD-cost:    6
c ---[ 612]---> BDD-cost:    2
c ---[ 611]---> BDD-cost:    6
c ---[ 610]---> BDD-cost:    2
c ---[ 609]---> BDD-cost:    6
c ---[ 608]---> BDD-cost:    2
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:    2
c ---[ 605]---> BDD-cost:    5
c ---[ 604]---> BDD-cost:    2
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    2
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost:    2
c ---[ 599]---> BDD-cost:    4
c ---[ 598]---> BDD-cost:    2
c ---[ 597]---> BDD-cost:    4
c ---[ 596]---> BDD-cost:    2
c ---[ 595]---> BDD-cost:    4
c ---[ 594]---> BDD-cost:    2
c ---[ 593]---> BDD-cost:    4
c ---[ 592]---> BDD-cost:    2
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    2
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    2
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    2
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    2
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    2
c ---[ 573]---> BDD-cost:    2
c ---[ 572]---> BDD-cost:    2
c ---[ 571]---> BDD-cost:    2
c ---[ 570]---> BDD-cost:    2
c ---[ 569]---> BDD-cost:    2
c ---[ 568]---> BDD-cost:    2
c ---[ 567]---> BDD-cost:    5
c ---[ 566]---> BDD-cost:    2
c ---[ 565]---> BDD-cost:    2
c ---[ 564]---> BDD-cost:    2
c ---[ 563]---> BDD-cost:    2
c ---[ 562]---> BDD-cost:    2
c ---[ 561]---> BDD-cost:    2
c ---[ 560]---> BDD-cost:    2
c ---[ 559]---> BDD-cost:    4
c ---[ 558]---> BDD-cost:    2
c ---[ 557]---> BDD-cost:    2
c ---[ 556]---> BDD-cost:    2
c ---[ 555]---> BDD-cost:    2
c ---[ 554]---> BDD-cost:    2
c ---[ 553]---> BDD-cost:    2
c ---[ 552]---> BDD-cost:    2
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    2
c ---[ 549]---> BDD-cost:    2
c ---[ 548]---> BDD-cost:    2
c ---[ 547]---> BDD-cost:    2
c ---[ 546]---> BDD-cost:    2
c ---[ 545]---> BDD-cost:    2
c ---[ 544]---> BDD-cost:    2
c ---[ 543]---> BDD-cost:    2
c ---[ 542]---> BDD-cost:    2
c ---[ 541]---> BDD-cost:    2
c ---[ 540]---> BDD-cost:    2
c ---[ 539]---> BDD-cost:    2
c ---[ 538]---> BDD-cost:    2
c ---[ 537]---> BDD-cost:    2
c ---[ 536]---> BDD-cost:    2
c ---[ 535]---> BDD-cost:    4
c ---[ 534]---> BDD-cost:    2
c ---[ 533]---> BDD-cost:    2
c ---[ 532]---> BDD-cost:    2
c ---[ 531]---> BDD-cost:    2
c ---[ 530]---> BDD-cost:    2
c ---[ 529]---> BDD-cost:    2
c ---[ 528]---> BDD-cost:    2
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    2
c ---[ 525]---> BDD-cost:    2
c ---[ 524]---> BDD-cost:    2
c ---[ 523]---> BDD-cost:    2
c ---[ 522]---> BDD-cost:    2
c ---[ 521]---> BDD-cost:    2
c ---[ 520]---> BDD-cost:    2
c ---[ 511]---> BDD-cost:    2
c ---[ 510]---> BDD-cost:    2
c ---[ 509]---> BDD-cost:    2
c ---[ 508]---> BDD-cost:    2
c ---[ 507]---> BDD-cost:    2
c ---[ 506]---> BDD-cost:    2
c ---[ 505]---> BDD-cost:    2
c ---[ 504]---> BDD-cost:    2
c ---[ 503]---> BDD-cost:    2
c ---[ 502]---> BDD-cost:    2
c ---[ 501]---> BDD-cost:    2
c ---[ 500]---> BDD-cost:    2
c ---[ 499]---> BDD-cost:    2
c ---[ 498]---> BDD-cost:    2
c ---[ 497]---> BDD-cost:    2
c ---[ 496]---> BDD-cost:    2
c ---[ 495]---> BDD-cost:    2
c ---[ 494]---> BDD-cost:    2
c ---[ 493]---> BDD-cost:    2
c ---[ 492]---> BDD-cost:    2
c ---[ 491]---> BDD-cost:    2
c ---[ 490]---> BDD-cost:    2
c ---[ 489]---> BDD-cost:    2
c ---[ 488]---> BDD-cost:    2
c ---[ 487]---> BDD-cost:    2
c ---[ 486]---> BDD-cost:    2
c ---[ 485]---> BDD-cost:    2
c ---[ 484]---> BDD-cost:    2
c ---[ 483]---> BDD-cost:    2
c ---[ 482]---> BDD-cost:    2
c ---[ 481]---> BDD-cost:    2
c ---[ 480]---> BDD-cost:    2
c ---[ 479]---> BDD-cost:    2
c ---[ 478]---> BDD-cost:    2
c ---[ 477]---> BDD-cost:    2
c ---[ 476]---> BDD-cost:    2
c ---[ 475]---> BDD-cost:    2
c ---[ 474]---> BDD-cost:    2
c ---[ 473]---> BDD-cost:    2
c ---[ 472]---> BDD-cost:    2
c ---[ 471]---> BDD-cost:    2
c ---[ 470]---> BDD-cost:    2
c ---[ 469]---> BDD-cost:    2
c ---[ 468]---> BDD-cost:    2
c ---[ 467]---> BDD-cost:    2
c ---[ 466]---> BDD-cost:    2
c ---[ 465]---> BDD-cost:    2
c ---[ 464]---> BDD-cost:    2
c ---[ 463]---> BDD-cost:    2
c ---[ 462]---> BDD-cost:    2
c ---[ 461]---> BDD-cost:    2
c ---[ 460]---> BDD-cost:    2
c ---[ 459]---> BDD-cost:    2
c ---[ 458]---> BDD-cost:    2
c ---[ 457]---> BDD-cost:    2
c ---[ 456]---> BDD-cost:    2
c ---[ 447]---> BDD-cost:    2
c ---[ 446]---> BDD-cost:    2
c ---[ 445]---> BDD-cost:    2
c ---[ 444]---> BDD-cost:    2
c ---[ 443]---> BDD-cost:    2
c ---[ 442]---> BDD-cost:    2
c ---[ 441]---> BDD-cost:    2
c ---[ 440]---> BDD-cost:    2
c ---[ 439]---> BDD-cost:    2
c ---[ 438]---> BDD-cost:    2
c ---[ 437]---> BDD-cost:    2
c ---[ 436]---> BDD-cost:    2
c ---[ 435]---> BDD-cost:    2
c ---[ 434]---> BDD-cost:    2
c ---[ 433]---> BDD-cost:    2
c ---[ 432]---> BDD-cost:    2
c ---[ 431]---> BDD-cost:    2
c ---[ 430]---> BDD-cost:    2
c ---[ 429]---> BDD-cost:    2
c ---[ 428]---> BDD-cost:    2
c ---[ 427]---> BDD-cost:    2
c ---[ 426]---> BDD-cost:    2
c ---[ 425]---> BDD-cost:    2
c ---[ 424]---> BDD-cost:    2
c ---[ 423]---> BDD-cost:    2
c ---[ 422]---> BDD-cost:    2
c ---[ 421]---> BDD-cost:    2
c ---[ 420]---> BDD-cost:    2
c ---[ 419]---> BDD-cost:    2
c ---[ 418]---> BDD-cost:    2
c ---[ 417]---> BDD-cost:    2
c ---[ 416]---> BDD-cost:    2
c ---[ 415]---> BDD-cost:    2
c ---[ 414]---> BDD-cost:    2
c ---[ 413]---> BDD-cost:    2
c ---[ 412]---> BDD-cost:    2
c ---[ 411]---> BDD-cost:    2
c ---[ 410]---> BDD-cost:    2
c ---[ 409]---> BDD-cost:    2
c ---[ 408]---> BDD-cost:    2
c ---[ 407]---> BDD-cost:    2
c ---[ 406]---> BDD-cost:    2
c ---[ 405]---> BDD-cost:    2
c ---[ 404]---> BDD-cost:    2
c ---[ 403]---> BDD-cost:    2
c ---[ 402]---> BDD-cost:    2
c ---[ 401]---> BDD-cost:    2
c ---[ 400]---> BDD-cost:    2
c ---[ 399]---> BDD-cost:    2
c ---[ 398]---> BDD-cost:    2
c ---[ 397]---> BDD-cost:    2
c ---[ 396]---> BDD-cost:    2
c ---[ 395]---> BDD-cost:    2
c ---[ 394]---> BDD-cost:    2
c ---[ 393]---> BDD-cost:    2
c ---[ 392]---> BDD-cost:    2
c ---[ 383]---> BDD-cost:    2
c ---[ 382]---> BDD-cost:    2
c ---[ 381]---> BDD-cost:    2
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:    2
c ---[ 378]---> BDD-cost:    2
c ---[ 377]---> BDD-cost:    2
c ---[ 376]---> BDD-cost:    2
c ---[ 375]---> BDD-cost:    2
c ---[ 374]---> BDD-cost:    2
c ---[ 373]---> BDD-cost:    2
c ---[ 372]---> BDD-cost:    2
c ---[ 371]---> BDD-cost:    2
c ---[ 370]---> BDD-cost:    2
c ---[ 369]---> BDD-cost:    2
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:    2
c ---[ 366]---> BDD-cost:    2
c ---[ 365]---> BDD-cost:    2
c ---[ 364]---> BDD-cost:    2
c ---[ 363]---> BDD-cost:    2
c ---[ 362]---> BDD-cost:    2
c ---[ 361]---> BDD-cost:    2
c ---[ 360]---> BDD-cost:    2
c ---[ 359]---> BDD-cost:    2
c ---[ 358]---> BDD-cost:    2
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:    2
c ---[ 355]---> BDD-cost:    2
c ---[ 354]---> BDD-cost:    2
c ---[ 353]---> BDD-cost:    2
c ---[ 352]---> BDD-cost:    2
c ---[ 351]---> BDD-cost:    2
c ---[ 350]---> BDD-cost:    2
c ---[ 349]---> BDD-cost:    2
c ---[ 348]---> BDD-cost:    2
c ---[ 347]---> BDD-cost:    2
c ---[ 346]---> BDD-cost:    2
c ---[ 345]---> BDD-cost:    2
c ---[ 344]---> BDD-cost:    2
c ---[ 343]---> BDD-cost:    2
c ---[ 342]---> BDD-cost:    2
c ---[ 341]---> BDD-cost:    2
c ---[ 340]---> BDD-cost:    2
c ---[ 339]---> BDD-cost:    2
c ---[ 338]---> BDD-cost:    2
c ---[ 337]---> BDD-cost:    2
c ---[ 336]---> BDD-cost:    2
c ---[ 335]---> BDD-cost:    2
c ---[ 334]---> BDD-cost:    2
c ---[ 333]---> BDD-cost:    2
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    2
c ---[ 330]---> BDD-cost:    2
c ---[ 329]---> BDD-cost:    2
c ---[ 328]---> BDD-cost:    2
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    2
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    2
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    2
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    2
c ---[ 311]---> BDD-cost:    8
c ---[ 310]---> BDD-cost:    2
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    2
c ---[ 307]---> BDD-cost:    8
c ---[ 306]---> BDD-cost:    2
c ---[ 305]---> BDD-cost:    8
c ---[ 304]---> BDD-cost:    2
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    2
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    2
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    2
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    2
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    2
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    2
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    2
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    2
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:    2
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:    2
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    2
c ---[ 281]---> BDD-cost:    5
c ---[ 280]---> BDD-cost:    2
c ---[ 279]---> BDD-cost:    4
c ---[ 278]---> BDD-cost:    2
c ---[ 277]---> BDD-cost:    4
c ---[ 276]---> BDD-cost:    2
c ---[ 275]---> BDD-cost:    4
c ---[ 274]---> BDD-cost:    2
c ---[ 273]---> BDD-cost:    4
c ---[ 272]---> BDD-cost:    2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    2
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    2
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    2
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    2
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    2
c ---[ 253]---> BDD-cost:    2
c ---[ 252]---> BDD-cost:    2
c ---[ 251]---> BDD-cost:    2
c ---[ 250]---> BDD-cost:    2
c ---[ 249]---> BDD-cost:    2
c ---[ 248]---> BDD-cost:    2
c ---[ 247]---> BDD-cost:    5
c ---[ 246]---> BDD-cost:    2
c ---[ 245]---> BDD-cost:    2
c ---[ 244]---> BDD-cost:    2
c ---[ 243]---> BDD-cost:    2
c ---[ 242]---> BDD-cost:    2
c ---[ 241]---> BDD-cost:    2
c ---[ 240]---> BDD-cost:    2
c ---[ 239]---> BDD-cost:    4
c ---[ 238]---> BDD-cost:    2
c ---[ 237]---> BDD-cost:    2
c ---[ 236]---> BDD-cost:    2
c ---[ 235]---> BDD-cost:    2
c ---[ 234]---> BDD-cost:    2
c ---[ 233]---> BDD-cost:    2
c ---[ 232]---> BDD-cost:    2
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    2
c ---[ 229]---> BDD-cost:    2
c ---[ 228]---> BDD-cost:    2
c ---[ 227]---> BDD-cost:    2
c ---[ 226]---> BDD-cost:    2
c ---[ 225]---> BDD-cost:    2
c ---[ 224]---> BDD-cost:    2
c ---[ 223]---> BDD-cost:    2
c ---[ 222]---> BDD-cost:    2
c ---[ 221]---> BDD-cost:    2
c ---[ 220]---> BDD-cost:    2
c ---[ 219]---> BDD-cost:    2
c ---[ 218]---> BDD-cost:    2
c ---[ 217]---> BDD-cost:    2
c ---[ 216]---> BDD-cost:    2
c ---[ 215]---> BDD-cost:    4
c ---[ 214]---> BDD-cost:    2
c ---[ 213]---> BDD-cost:    2
c ---[ 212]---> BDD-cost:    2
c ---[ 211]---> BDD-cost:    2
c ---[ 210]---> BDD-cost:    2
c ---[ 209]---> BDD-cost:    2
c ---[ 208]---> BDD-cost:    2
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    2
c ---[ 205]---> BDD-cost:    2
c ---[ 204]---> BDD-cost:    2
c ---[ 203]---> BDD-cost:    2
c ---[ 202]---> BDD-cost:    2
c ---[ 201]---> BDD-cost:    2
c ---[ 200]---> BDD-cost:    2
c ---[ 191]---> BDD-cost:    2
c ---[ 190]---> BDD-cost:    2
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 181]---> BDD-cost:    2
c ---[ 180]---> BDD-cost:    2
c ---[ 179]---> BDD-cost:    2
c ---[ 178]---> BDD-cost:    2
c ---[ 177]---> BDD-cost:    2
c ---[ 176]---> BDD-cost:    2
c ---[ 175]---> BDD-cost:    2
c ---[ 174]---> BDD-cost:    2
c ---[ 173]---> BDD-cost:    2
c ---[ 172]---> BDD-cost:    2
c ---[ 171]---> BDD-cost:    2
c ---[ 170]---> BDD-cost:    2
c ---[ 169]---> BDD-cost:    2
c ---[ 168]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 166]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 164]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 162]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    2
c ---[ 159]---> BDD-cost:    2
c ---[ 158]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    2
c ---[ 156]---> BDD-cost:    2
c ---[ 155]---> BDD-cost:    2
c ---[ 154]---> BDD-cost:    2
c ---[ 153]---> BDD-cost:    2
c ---[ 152]---> BDD-cost:    2
c ---[ 151]---> BDD-cost:    2
c ---[ 150]---> BDD-cost:    2
c ---[ 149]---> BDD-cost:    2
c ---[ 148]---> BDD-cost:    2
c ---[ 147]---> BDD-cost:    2
c ---[ 146]---> BDD-cost:    2
c ---[ 145]---> BDD-cost:    2
c ---[ 144]---> BDD-cost:    2
c ---[ 143]---> BDD-cost:    2
c ---[ 142]---> BDD-cost:    2
c ---[ 141]---> BDD-cost:    2
c ---[ 140]---> BDD-cost:    2
c ---[ 139]---> BDD-cost:    2
c ---[ 138]---> BDD-cost:    2
c ---[ 137]---> BDD-cost:    2
c ---[ 136]---> BDD-cost:    2
c ---[ 127]---> BDD-cost:    2
c ---[ 126]---> BDD-cost:    2
c ---[ 125]---> BDD-cost:    2
c ---[ 124]---> BDD-cost:    2
c ---[ 123]---> BDD-cost:    2
c ---[ 122]---> BDD-cost:    2
c ---[ 121]---> BDD-cost:    2
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 118]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 116]---> BDD-cost:    2
c ---[ 115]---> BDD-cost:    2
c ---[ 114]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 111]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 109]---> BDD-cost:    2
c ---[ 108]---> BDD-cost:    2
c ---[ 107]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 104]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[ 102]---> BDD-cost:    2
c ---[ 101]---> BDD-cost:    2
c ---[ 100]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  94]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  88]---> BDD-cost:    2
c ---[  87]---> BDD-cost:    2
c ---[  86]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  83]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  81]---> BDD-cost:    2
c ---[  80]---> BDD-cost:    2
c ---[  79]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  76]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  74]---> BDD-cost:    2
c ---[  73]---> BDD-cost:    2
c ---[  72]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  62]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  60]---> BDD-cost:    2
c ---[  59]---> BDD-cost:    2
c ---[  58]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  55]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  53]---> BDD-cost:    2
c ---[  52]---> BDD-cost:    2
c ---[  51]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  48]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  46]---> BDD-cost:    2
c ---[  45]---> BDD-cost:    2
c ---[  44]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  41]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  39]---> BDD-cost:    2
c ---[  38]---> BDD-cost:    2
c ---[  37]---> BDD-cost:    2
c ---[  36]---> BDD-cost:    2
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:    2
c ---[  33]---> BDD-cost:    2
c ---[  32]---> BDD-cost:    2
c ---[  31]---> BDD-cost:    2
c ---[  30]---> BDD-cost:    2
c ---[  29]---> BDD-cost:    2
c ---[  28]---> BDD-cost:    2
c ---[  27]---> BDD-cost:    2
c ---[  26]---> BDD-cost:    2
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost:    2
c ---[  23]---> BDD-cost:    2
c ---[  22]---> BDD-cost:    2
c ---[  21]---> BDD-cost:    2
c ---[  20]---> BDD-cost:    2
c ---[  19]---> BDD-cost:    2
c ---[  18]---> BDD-cost:    2
c ---[  17]---> BDD-cost:    2
c ---[  16]---> BDD-cost:    2
c ---[  15]---> BDD-cost:    2
c ---[  14]---> BDD-cost:    2
c ---[  13]---> BDD-cost:    2
c ---[  12]---> BDD-cost:    2
c ---[  11]---> BDD-cost:    2
c ---[  10]---> BDD-cost:    2
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17376    49254 |    5792       0        0     nan |  0.000 % |
c |       100 |   17376    49254 |    6371     100     1326    13.3 | 27.023 % |
c ==============================================================================
c [1mFound solution: 31956[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36248     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       147 |  112281   271036 |   37427     147     1914    13.0 | 27.023 % |
c ==============================================================================
c [1mFound solution: 31563[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       176 |  113591   274375 |   37863     176     2430    13.8 | 27.023 % |
c |       277 |  113591   274375 |   41649     277     5251    19.0 |  4.757 % |
c ==============================================================================
c [1mFound solution: 31343[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       382 |  113629   274546 |   37876     382     6306    16.5 |  4.757 % |
c ==============================================================================
c [1mFound solution: 31013[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       387 |  113644   274619 |   37881     387     6362    16.4 |  4.757 % |
c |       487 |  113644   274619 |   41669     487     9135    18.8 |  4.758 % |
c |       637 |  113596   274511 |   45836     635    10811    17.0 |  4.787 % |
c ==============================================================================
c [1mFound solution: 30586[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       675 |  113901   275318 |   37967     673    15256    22.7 |  4.787 % |
c ==============================================================================
c [1mFound solution: 28916[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       739 |  113929   275393 |   37976     737    16345    22.2 |  4.787 % |
c ==============================================================================
c [1mFound solution: 28339[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       811 |  114074   275750 |   38024     809    17738    21.9 |  4.787 % |
c ==============================================================================
c [1mFound solution: 28118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       869 |  114087   275872 |   38029     867    20760    23.9 |  4.787 % |
c |       969 |  114073   275840 |   41831     966    24217    25.1 |  4.772 % |
c |      1120 |  114073   275840 |   46015    1117    39019    34.9 |  4.772 % |
c |      1345 |  114073   275840 |   50616    1342    43692    32.6 |  4.772 % |
c |      1683 |  114073   275840 |   55678    1680    47677    28.4 |  4.772 % |
c |      2195 |  114073   275840 |   61246    2192    54895    25.0 |  4.772 % |
c |      2954 |  114073   275840 |   67370    2951   171086    58.0 |  4.772 % |
c ==============================================================================
c [1mFound solution: 27817[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3367 |  114212   276177 |   38070    3364   192128    57.1 |  4.772 % |
c |      3467 |  114212   276177 |   41877    3464   194840    56.2 |  4.765 % |
c |      3617 |  114212   276177 |   46064    3614   206716    57.2 |  4.765 % |
c |      3842 |  114212   276177 |   50671    3839   213401    55.6 |  4.765 % |
c |      4179 |  114212   276177 |   55738    4176   230255    55.1 |  4.765 % |
c |      4686 |  114212   276177 |   61312    4683   242856    51.9 |  4.765 % |
c |      5450 |  114212   276177 |   67443    5447   272764    50.1 |  4.765 % |
c |      6590 |  113989   275672 |   74187    6582   322347    49.0 |  4.915 % |
c |      8299 |  113989   275672 |   81606    8291   447067    53.9 |  4.915 % |
c |     10861 |  113758   275143 |   89767   10843   584131    53.9 |  5.066 % |
c ==============================================================================
c [1mFound solution: 27813[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14491 |  113191   273859 |   37730   14454   705837    48.8 |  5.066 % |
c |     14592 |  113118   273692 |   41503   14554   708940    48.7 |  5.499 % |
c |     14742 |  112774   272909 |   45653   14702   711851    48.4 |  5.717 % |
c |     14970 |  112774   272909 |   50218   14930   730505    48.9 |  5.717 % |
c |     15307 |  112774   272909 |   55240   15267   756401    49.5 |  5.717 % |
c |     15813 |  112774   272909 |   60764   15773   787871    50.0 |  5.717 % |
c ==============================================================================
c [1mFound solution: 27795[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16057 |  112800   272984 |   37600   16017   809097    50.5 |  5.717 % |
c |     16157 |  112800   272984 |   41360   16117   813107    50.5 |  5.717 % |
c ==============================================================================
c [1mFound solution: 27501[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16294 |  112808   273013 |   37602   16254   820930    50.5 |  5.717 % |
c |     16396 |  112808   273013 |   41362   16356   832545    50.9 |  5.718 % |
c |     16547 |  112744   272871 |   45498   16504   833734    50.5 |  5.764 % |
c |     16773 |  112580   272501 |   50048   16707   843676    50.5 |  5.876 % |
c |     17110 |  112580   272501 |   55053   17044   877938    51.5 |  5.876 % |
c |     17616 |  112580   272501 |   60558   17550   917907    52.3 |  5.876 % |
c |     18377 |  112580   272501 |   66614   18311   997681    54.5 |  5.876 % |
c |     19519 |  112545   272422 |   73275   19452  1030099    53.0 |  5.900 % |
c |     21228 |  112157   271542 |   80603   21144  1265877    59.9 |  6.151 % |
c |     23790 |  112109   271433 |   88663   23702  1325656    55.9 |  6.190 % |
c ==============================================================================
c [1mFound solution: 27457[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25312 |  112118   271454 |   37372   25224  1393087    55.2 |  6.190 % |
c |     25413 |  112118   271454 |   41109   25325  1396262    55.1 |  6.192 % |
c |     25565 |  112118   271454 |   45220   25477  1400766    55.0 |  6.192 % |
c |     25791 |  112118   271454 |   49742   25703  1417812    55.2 |  6.192 % |
c |     26128 |  112118   271454 |   54716   26040  1426891    54.8 |  6.192 % |
c |     26634 |  112118   271454 |   60187   26546  1439549    54.2 |  6.192 % |
c |     27393 |  112118   271454 |   66206   27305  1524061    55.8 |  6.192 % |
c |     28532 |  111938   271046 |   72827   28436  1620084    57.0 |  6.315 % |
c |     30240 |  111684   270463 |   80110   30142  1789816    59.4 |  6.499 % |
c |     32802 |  111684   270463 |   88121   32704  1914290    58.5 |  6.499 % |
c |     36646 |  111684   270463 |   96933   36548  2269361    62.1 |  6.499 % |
c ==============================================================================
c [1mFound solution: 27360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38116 |  111697   270494 |   37232   38018  2366385    62.2 |  6.499 % |
c |     38217 |  111697   270494 |   40955   38119  2377846    62.4 |  6.500 % |
c |     38368 |  111697   270494 |   45050   38270  2384323    62.3 |  6.500 % |
c |     38593 |  111697   270494 |   49555   38495  2405792    62.5 |  6.500 % |
c |     38930 |  111697   270494 |   54511   38832  2429420    62.6 |  6.500 % |
c |     39437 |  109953   266516 |   59962   39301  2436439    62.0 |  7.736 % |
c |     40196 |  109953   266516 |   65958   40060  2571897    64.2 |  7.736 % |
c |     41335 |  109953   266516 |   72554   41199  2708593    65.7 |  7.736 % |
c ==============================================================================
c [1mFound solution: 27257[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42092 |  109961   266535 |   36653   41956  2793630    66.6 |  7.736 % |
c |     42193 |  109961   266535 |   40318   16732  1033515    61.8 |  7.738 % |
c |     42344 |  109961   266535 |   44350   16883  1042761    61.8 |  7.738 % |
c |     42570 |  109961   266535 |   48785   17109  1058246    61.9 |  7.738 % |
c |     42908 |  109961   266535 |   53663   17447  1085007    62.2 |  7.738 % |
c |     43416 |  109961   266535 |   59030   17955  1140854    63.5 |  7.738 % |
c |     44175 |  109961   266535 |   64933   18714  1171895    62.6 |  7.738 % |
c |     45316 |  109961   266535 |   71426   19855  1219126    61.4 |  7.738 % |
c |     47027 |  108578   263358 |   78568   21347  1337574    62.7 |  8.749 % |
c |     49590 |  108578   263358 |   86425   23910  1804189    75.5 |  8.749 % |
c |     53436 |  107972   261973 |   95068   27732  2316612    83.5 |  9.198 % |
c |     59204 |  106915   259561 |  104575   33279  2706898    81.3 |  9.953 % |
c |     67855 |  104663   254383 |  115032   41755  3303359    79.1 | 11.578 % |
c ==============================================================================
c [1mFound solution: 27201[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72316 |  104667   254392 |   34889   46216  3745394    81.0 | 11.578 % |
c |     72417 |  104667   254392 |   38377   18616   964264    51.8 | 11.580 % |
c |     72567 |  104667   254392 |   42215   18766   968857    51.6 | 11.580 % |
c |     72792 |  104667   254392 |   46437   18991   976186    51.4 | 11.580 % |
c |     73130 |  104667   254392 |   51080   19329   987298    51.1 | 11.580 % |
c |     73637 |  104667   254392 |   56189   19836  1004080    50.6 | 11.580 % |
c |     74398 |  104667   254392 |   61807   20597  1062430    51.6 | 11.580 % |
c |     75537 |  104667   254392 |   67988   21736  1110020    51.1 | 11.580 % |
c |     77246 |  104667   254392 |   74787   23445  1156496    49.3 | 11.580 % |
c ==============================================================================
c [1mFound solution: 26793[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77295 |  104678   254423 |   34892   23494  1161038    49.4 | 11.580 % |
c |     77395 |  104414   253816 |   38381   23586  1162616    49.3 | 11.786 % |
c |     77545 |  104414   253816 |   42219   23736  1166062    49.1 | 11.786 % |
c |     77770 |  104414   253816 |   46441   23961  1184154    49.4 | 11.786 % |
c |     78109 |  104414   253816 |   51085   24300  1191266    49.0 | 11.786 % |
c |     78615 |  104414   253816 |   56193   24806  1203274    48.5 | 11.786 % |
c |     79374 |  104414   253816 |   61813   25565  1260624    49.3 | 11.786 % |
c |     80515 |  104414   253816 |   67994   26706  1379561    51.7 | 11.786 % |
c |     82225 |  104414   253816 |   74794   28416  1486335    52.3 | 11.786 % |
c |     84789 |  104303   253562 |   82273   30430  1604311    52.7 | 11.883 % |
c ==============================================================================
c [1mFound solution: 26443[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88501 |  104313   253585 |   34771   34142  1877163    55.0 | 11.883 % |
c |     88601 |  104313   253585 |   38248   34242  1881540    54.9 | 11.884 % |
c |     88752 |  104313   253585 |   42072   34393  1899019    55.2 | 11.884 % |
c |     88978 |  104313   253585 |   46280   34619  1915760    55.3 | 11.884 % |
c |     89315 |  104120   253139 |   50908   34918  1920410    55.0 | 12.031 % |
c |     89822 |  104076   253043 |   55999   35420  1977425    55.8 | 12.072 % |
c |     90582 |  104076   253043 |   61598   36180  2032359    56.2 | 12.072 % |
c |     91722 |  104076   253043 |   67758   37320  2142490    57.4 | 12.072 % |
c |     93432 |  104076   253043 |   74534   39030  2221665    56.9 | 12.072 % |
c |     95995 |  104076   253043 |   81988   41593  2714177    65.3 | 12.072 % |
c |     99840 |  103852   252527 |   90187   45433  2925008    64.4 | 12.234 % |
c |    105606 |  102236   248798 |   99205   51130  3306514    64.7 | 13.455 % |
c |    114257 |  101251   246513 |  109126   59672  3654481    61.2 | 14.215 % |
c ==============================================================================
c [1mFound solution: 26442[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 5 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122777 |  101262   246540 |   33754   68192  4590117    67.3 | 14.215 % |
c |    122877 |  101262   246540 |   37129   22956  1167913    50.9 | 14.215 % |
c |    123027 |  101262   246540 |   40842   23106  1175108    50.9 | 14.215 % |
c |    123253 |  101262   246540 |   44926   23332  1184804    50.8 | 14.215 % |
c |    123590 |  101262   246540 |   49419   23669  1207074    51.0 | 14.215 % |
c |    124096 |  101262   246540 |   54361   24175  1259017    52.1 | 14.215 % |
c |    124859 |  101262   246540 |   59797   24938  1364639    54.7 | 14.215 % |
c |    126000 |  101262   246540 |   65776   26079  1414687    54.2 | 14.215 % |
c |    127708 |  101262   246540 |   72354   27787  1547195    55.7 | 14.215 % |
c |    130270 |  101262   246540 |   79590   30349  1854960    61.1 | 14.215 % |
c |    134116 |  100870   245638 |   87549   34177  2194864    64.2 | 14.495 % |
c |    139883 |  100870   245638 |   96304   39944  2475013    62.0 | 14.495 % |
c |    148532 |  100870   245638 |  105934   48593  3332642    68.6 | 14.495 % |
c |    161506 |  100870   245638 |  116527   61567  4104866    66.7 | 14.495 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 14290
Raw data (stat): 14290 (runsolver) R 14289 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479119047 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 4393 0 0 0 987 11 0 0 25 0 1 0 479119047 19054592 3792 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 3792 603 41 0 4611 0
vsize: 18608
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 4505 0 0 0 1986 12 0 0 25 0 1 0 479119047 19582976 3904 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 3904 603 41 0 4740 0
vsize: 19124
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 4693 0 0 0 2985 13 0 0 25 0 1 0 479119047 19976192 4020 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4877 4020 603 41 0 4836 0
vsize: 19508
[startup+40.001 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 4826 0 0 0 3984 14 0 0 25 0 1 0 479119047 20508672 4153 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5007 4153 603 41 0 4966 0
vsize: 20028
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 4932 0 0 0 4984 14 0 0 25 0 1 0 479119047 21041152 4259 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5137 4259 603 41 0 5096 0
vsize: 20548
[startup+60.0024 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 5085 0 0 0 5983 14 0 0 25 0 1 0 479119047 21659648 4412 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5288 4412 603 41 0 5247 0
vsize: 21152
[startup+70.0031 s]
Raw data (loadavg): 1.09 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 5318 0 0 0 6982 15 0 0 25 0 1 0 479119047 22274048 4572 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5438 4572 603 41 0 5397 0
vsize: 21752
[startup+80.0037 s]
Raw data (loadavg): 1.08 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 5407 0 0 0 7982 16 0 0 25 0 1 0 479119047 22671360 4661 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5535 4661 603 41 0 5494 0
vsize: 22140
[startup+90.0044 s]
Raw data (loadavg): 1.07 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 5655 0 0 0 8981 17 0 0 25 0 1 0 479119047 23150592 4764 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5652 4764 603 41 0 5611 0
vsize: 22608
[startup+100.005 s]
Raw data (loadavg): 1.06 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 5768 0 0 0 9980 18 0 0 25 0 1 0 479119047 23674880 4877 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5780 4877 603 41 0 5739 0
vsize: 23120
[startup+110.006 s]
Raw data (loadavg): 1.05 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6049 0 0 0 10980 18 0 0 25 0 1 0 479119047 24743936 5158 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6041 5158 603 41 0 6000 0
vsize: 24164
[startup+120.006 s]
Raw data (loadavg): 1.04 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6126 0 0 0 11979 19 0 0 25 0 1 0 479119047 25141248 5235 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6138 5235 603 41 0 6097 0
vsize: 24552
[startup+130.007 s]
Raw data (loadavg): 1.03 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6316 0 0 0 12978 20 0 0 25 0 1 0 479119047 25489408 5352 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6223 5352 603 41 0 6182 0
vsize: 24892
[startup+140.007 s]
Raw data (loadavg): 1.03 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6417 0 0 0 13978 20 0 0 25 0 1 0 479119047 26001408 5453 4294967295 134512640 134672761 3221224640 3221223824 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6348 5453 603 41 0 6307 0
vsize: 25392
[startup+150.007 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6527 0 0 0 14978 21 0 0 25 0 1 0 479119047 26390528 5563 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6443 5563 603 41 0 6402 0
vsize: 25772
[startup+160.007 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6638 0 0 0 15977 21 0 0 25 0 1 0 479119047 26796032 5674 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6542 5674 603 41 0 6501 0
vsize: 26168
[startup+170.007 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6737 0 0 0 16977 22 0 0 25 0 1 0 479119047 27197440 5773 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6640 5773 603 41 0 6599 0
vsize: 26560
[startup+180.007 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6816 0 0 0 17977 22 0 0 25 0 1 0 479119047 27594752 5852 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6737 5852 603 41 0 6696 0
vsize: 26948
[startup+190.008 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 6909 0 0 0 18977 22 0 0 25 0 1 0 479119047 28123136 5945 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 5945 603 41 0 6825 0
vsize: 27464
[startup+200.009 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7018 0 0 0 19976 23 0 0 25 0 1 0 479119047 28512256 6054 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6961 6054 603 41 0 6920 0
vsize: 27844
[startup+210.008 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7153 0 0 0 20976 24 0 0 25 0 1 0 479119047 29032448 6189 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7088 6189 603 41 0 7047 0
vsize: 28352
[startup+220.008 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7273 0 0 0 21976 24 0 0 25 0 1 0 479119047 29564928 6309 4294967295 134512640 134672761 3221224640 3221223776 134560637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7218 6309 603 41 0 7177 0
vsize: 28872
[startup+230.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7368 0 0 0 22975 25 0 0 25 0 1 0 479119047 29954048 6404 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7313 6404 603 41 0 7272 0
vsize: 29252
[startup+240.009 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7533 0 0 0 23975 25 0 0 25 0 1 0 479119047 30273536 6495 4294967295 134512640 134672761 3221224640 3221223764 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7391 6495 603 41 0 7350 0
vsize: 29564
[startup+250.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7679 0 0 0 24975 25 0 0 25 0 1 0 479119047 30920704 6641 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7549 6641 603 41 0 7508 0
vsize: 30196
[startup+260.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7808 0 0 0 25975 25 0 0 25 0 1 0 479119047 31416320 6770 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7670 6770 603 41 0 7629 0
vsize: 30680
[startup+270.01 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 7902 0 0 0 26975 26 0 0 25 0 1 0 479119047 31801344 6864 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7764 6864 603 41 0 7723 0
vsize: 31056
[startup+280.011 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 27975 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+290.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 28975 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+300.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 29976 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+310.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 30976 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+320.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 31976 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+330.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 32976 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+340.012 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 33976 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+350.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 34977 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+360.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 35977 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+370.013 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 36977 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223824 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+380.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8013 0 0 0 37977 26 0 0 25 0 1 0 479119047 31907840 6902 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7790 6902 603 41 0 7749 0
vsize: 31160
[startup+390.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8024 0 0 0 38977 26 0 0 25 0 1 0 479119047 32034816 6913 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7821 6913 603 41 0 7780 0
vsize: 31284
[startup+400.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8133 0 0 0 39977 26 0 0 25 0 1 0 479119047 32440320 7022 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7920 7022 603 41 0 7879 0
vsize: 31680
[startup+410.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8238 0 0 0 40977 27 0 0 25 0 1 0 479119047 32837632 7127 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8017 7127 603 41 0 7976 0
vsize: 32068
[startup+420.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8324 0 0 0 41977 27 0 0 25 0 1 0 479119047 33243136 7213 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8116 7213 603 41 0 8075 0
vsize: 32464
[startup+430.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8413 0 0 0 42977 27 0 0 25 0 1 0 479119047 33636352 7302 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8212 7302 603 41 0 8171 0
vsize: 32848
[startup+440.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8503 0 0 0 43977 27 0 0 25 0 1 0 479119047 34033664 7392 4294967295 134512640 134672761 3221224640 3221223812 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8309 7392 603 41 0 8268 0
vsize: 33236
[startup+450.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8595 0 0 0 44977 28 0 0 25 0 1 0 479119047 34299904 7484 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8374 7484 603 41 0 8333 0
vsize: 33496
[startup+460.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8702 0 0 0 45977 28 0 0 25 0 1 0 479119047 34832384 7591 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8504 7591 603 41 0 8463 0
vsize: 34016
[startup+470.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8802 0 0 0 46977 28 0 0 25 0 1 0 479119047 35233792 7691 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8602 7691 603 41 0 8561 0
vsize: 34408
[startup+480.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8896 0 0 0 47977 28 0 0 25 0 1 0 479119047 35627008 7785 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 7785 603 41 0 8657 0
vsize: 34792
[startup+490.014 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 8997 0 0 0 48976 29 0 0 25 0 1 0 479119047 36020224 7886 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8794 7886 603 41 0 8753 0
vsize: 35176
[startup+500.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 49977 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223840 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+510.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 50977 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+520.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 51977 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223812 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+530.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 52977 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+540.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 53977 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+550.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 54977 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+560.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 55977 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223824 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+570.015 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 56978 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223808 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+580.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 57978 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+590.016 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9113 0 0 0 58978 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+600.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9155 0 0 0 59978 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+610.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9155 0 0 0 60979 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+620.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9155 0 0 0 61979 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+630.017 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9155 0 0 0 62979 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+640.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9155 0 0 0 63979 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223812 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+650.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9155 0 0 0 64979 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223792 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+660.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9155 0 0 0 65979 29 0 0 25 0 1 0 479119047 36093952 7929 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7929 603 41 0 8771 0
vsize: 35248
[startup+670.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9156 0 0 0 66979 29 0 0 25 0 1 0 479119047 36093952 7930 4294967295 134512640 134672761 3221224640 3221223812 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7930 603 41 0 8771 0
vsize: 35248
[startup+680.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9157 0 0 0 67979 29 0 0 25 0 1 0 479119047 36093952 7931 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7931 603 41 0 8771 0
vsize: 35248
[startup+690.018 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9158 0 0 0 68979 29 0 0 25 0 1 0 479119047 36093952 7932 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7932 603 41 0 8771 0
vsize: 35248
[startup+700.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9160 0 0 0 69980 29 0 0 25 0 1 0 479119047 36093952 7934 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7934 603 41 0 8771 0
vsize: 35248
[startup+710.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9163 0 0 0 70980 29 0 0 25 0 1 0 479119047 36093952 7937 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7937 603 41 0 8771 0
vsize: 35248
[startup+720.019 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9164 0 0 0 71980 29 0 0 25 0 1 0 479119047 36093952 7938 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7938 603 41 0 8771 0
vsize: 35248
[startup+730.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9166 0 0 0 72980 29 0 0 25 0 1 0 479119047 36093952 7940 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8812 7940 603 41 0 8771 0
vsize: 35248
[startup+740.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9205 0 0 0 73980 29 0 0 25 0 1 0 479119047 36356096 7979 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8876 7979 603 41 0 8835 0
vsize: 35504
[startup+750.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9320 0 0 0 74980 30 0 0 25 0 1 0 479119047 36745216 8094 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8971 8094 603 41 0 8930 0
vsize: 35884
[startup+760.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9432 0 0 0 75980 30 0 0 25 0 1 0 479119047 37273600 8206 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9100 8206 603 41 0 9059 0
vsize: 36400
[startup+770.02 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9521 0 0 0 76979 31 0 0 25 0 1 0 479119047 37539840 8295 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9165 8295 603 41 0 9124 0
vsize: 36660
[startup+780.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9629 0 0 0 77979 31 0 0 25 0 1 0 479119047 38060032 8403 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9292 8403 603 41 0 9251 0
vsize: 37168
[startup+790.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9728 0 0 0 78979 31 0 0 25 0 1 0 479119047 38461440 8502 4294967295 134512640 134672761 3221224640 3221223744 134560322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9390 8502 603 41 0 9349 0
vsize: 37560
[startup+800.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9823 0 0 0 79979 32 0 0 25 0 1 0 479119047 38862848 8597 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9488 8597 603 41 0 9447 0
vsize: 37952
[startup+810.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 9922 0 0 0 80979 32 0 0 25 0 1 0 479119047 39518208 8696 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 8696 603 41 0 9607 0
vsize: 38592
[startup+820.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10031 0 0 0 81979 33 0 0 25 0 1 0 479119047 39907328 8805 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9743 8805 603 41 0 9702 0
vsize: 38972
[startup+830.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10147 0 0 0 82978 33 0 0 25 0 1 0 479119047 40435712 8921 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9872 8921 603 41 0 9831 0
vsize: 39488
[startup+840.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 83978 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+850.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 84978 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+860.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 85978 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+870.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 86978 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+880.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 87978 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+890.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 88979 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+900.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 89979 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+910.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 90979 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+920.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 91979 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+930.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 92979 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+940.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 93980 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+950.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 94980 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+960.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 95980 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223824 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+970.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 96980 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+980.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 97980 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+990.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 98981 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 99981 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 100981 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 101981 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 102981 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 103982 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223824 134559601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 104982 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 105982 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 106982 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 107982 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 108983 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 109983 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 110983 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 111983 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 112983 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 113984 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 114984 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 115984 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 116984 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 117984 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 118985 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14290
Raw data (stat): 14290 (minisat+) R 14289 10614 10613 0 -1 0 10287 0 0 0 119985 34 0 0 25 0 1 0 479119047 40620032 8991 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9917 8991 603 41 0 9876 0
vsize: 39668
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.98 0.92 1/54 14290
Raw data (stat): 14290 (minisat+) Z 14289 10614 10613 0 -1 12 10290 0 0 0 119985 36 0 0 25 0 1 0 479119047 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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