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 5600

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        899996 kB
Buffers:         37576 kB
Cached:          77684 kB
SwapCached:          0 kB
Active:          72860 kB
Inactive:        45212 kB
HighTotal:      131008 kB
HighFree:        49448 kB
LowTotal:       903652 kB
LowFree:        850548 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11076 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:03:48 (client local time) WITH STATUS 10 IN 1210.09 SECONDS
stats: 4022 7 1210.09 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4626 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[4624]---> BDD-cost:   17
c ---[4622]---> BDD-cost:   17
c ---[4620]---> BDD-cost:   17
c ---[4618]---> BDD-cost:   17
c ---[4616]---> BDD-cost:   17
c ---[4614]---> BDD-cost:   17
c ---[4612]---> BDD-cost:   17
c ---[4610]---> BDD-cost:   17
c ---[4608]---> BDD-cost:   17
c ---[4606]---> BDD-cost:   17
c ---[4604]---> BDD-cost:   17
c ---[4602]---> BDD-cost:   17
c ---[4600]---> BDD-cost:   17
c ---[4598]---> BDD-cost:   17
c ---[4596]---> BDD-cost:   17
c ---[4594]---> BDD-cost:   17
c ---[4592]---> BDD-cost:   17
c ---[4590]---> BDD-cost:   17
c ---[4588]---> BDD-cost:   17
c ---[4586]---> BDD-cost:   17
c ---[4584]---> BDD-cost:   17
c ---[4582]---> BDD-cost:   17
c ---[4580]---> BDD-cost:   17
c ---[4578]---> BDD-cost:   17
c ---[4576]---> BDD-cost:   17
c ---[4574]---> BDD-cost:   17
c ---[4572]---> BDD-cost:   17
c ---[4570]---> BDD-cost:   17
c ---[4568]---> BDD-cost:   17
c ---[4566]---> BDD-cost:   17
c ---[4265]---> BDD-cost:    7
c ---[4264]---> BDD-cost:    7
c ---[4263]---> BDD-cost:    7
c ---[4262]---> BDD-cost:    7
c ---[4261]---> BDD-cost:    7
c ---[4260]---> BDD-cost:    7
c ---[4259]---> BDD-cost:    7
c ---[4258]---> BDD-cost:    7
c ---[4257]---> BDD-cost:    7
c ---[4256]---> BDD-cost:    7
c ---[4255]---> BDD-cost:    7
c ---[4254]---> BDD-cost:    7
c ---[4253]---> BDD-cost:    7
c ---[4252]---> BDD-cost:    7
c ---[4251]---> BDD-cost:    7
c ---[4250]---> BDD-cost:    7
c ---[4249]---> BDD-cost:    7
c ---[4248]---> BDD-cost:    7
c ---[4247]---> BDD-cost:    7
c ---[4246]---> BDD-cost:    7
c ---[4245]---> BDD-cost:    7
c ---[4244]---> BDD-cost:    7
c ---[4243]---> BDD-cost:    7
c ---[4242]---> BDD-cost:    7
c ---[4241]---> BDD-cost:    7
c ---[4240]---> BDD-cost:    7
c ---[4239]---> BDD-cost:    7
c ---[4238]---> BDD-cost:    7
c ---[4237]---> BDD-cost:    7
c ---[4236]---> BDD-cost:    7
c ---[4235]---> BDD-cost:    7
c ---[4234]---> BDD-cost:    7
c ---[4233]---> BDD-cost:    7
c ---[4232]---> BDD-cost:    7
c ---[4231]---> BDD-cost:    7
c ---[4230]---> BDD-cost:    7
c ---[4229]---> BDD-cost:    7
c ---[4228]---> BDD-cost:    7
c ---[4227]---> BDD-cost:    7
c ---[4226]---> BDD-cost:    7
c ---[4225]---> BDD-cost:    7
c ---[4224]---> BDD-cost:    7
c ---[4223]---> BDD-cost:    7
c ---[4222]---> BDD-cost:    7
c ---[4221]---> BDD-cost:    7
c ---[4220]---> BDD-cost:    7
c ---[4219]---> BDD-cost:    7
c ---[4218]---> BDD-cost:    7
c ---[4217]---> BDD-cost:    7
c ---[4216]---> BDD-cost:    7
c ---[4215]---> BDD-cost:    7
c ---[4214]---> BDD-cost:    7
c ---[4213]---> BDD-cost:    7
c ---[4212]---> BDD-cost:    7
c ---[4211]---> BDD-cost:    7
c ---[4210]---> BDD-cost:    7
c ---[4209]---> BDD-cost:    7
c ---[4208]---> BDD-cost:    7
c ---[4207]---> BDD-cost:    7
c ---[4206]---> BDD-cost:    7
c ---[4204]---> BDD-cost:    9
c ---[4202]---> BDD-cost:    9
c ---[4200]---> BDD-cost:    9
c ---[4198]---> BDD-cost:    9
c ---[4196]---> BDD-cost:    9
c ---[4194]---> BDD-cost:    9
c ---[4192]---> BDD-cost:    9
c ---[4190]---> BDD-cost:    9
c ---[4188]---> BDD-cost:    9
c ---[4186]---> BDD-cost:    9
c ---[4184]---> BDD-cost:    9
c ---[4182]---> BDD-cost:    9
c ---[4180]---> BDD-cost:    9
c ---[4178]---> BDD-cost:    9
c ---[4176]---> BDD-cost:    9
c ---[4174]---> BDD-cost:    9
c ---[4172]---> BDD-cost:    9
c ---[4170]---> BDD-cost:    9
c ---[4168]---> BDD-cost:    9
c ---[4166]---> BDD-cost:    9
c ---[4164]---> BDD-cost:    9
c ---[4162]---> BDD-cost:    9
c ---[4160]---> BDD-cost:    9
c ---[4158]---> BDD-cost:    9
c ---[4156]---> BDD-cost:    9
c ---[4154]---> BDD-cost:    9
c ---[4152]---> BDD-cost:    9
c ---[4150]---> BDD-cost:    9
c ---[4148]---> BDD-cost:    9
c ---[4146]---> BDD-cost:    9
c ---[4144]---> BDD-cost:    9
c ---[4142]---> BDD-cost:    9
c ---[4140]---> BDD-cost:    9
c ---[4138]---> BDD-cost:    9
c ---[4136]---> BDD-cost:    9
c ---[4134]---> BDD-cost:    9
c ---[4132]---> BDD-cost:    9
c ---[4130]---> BDD-cost:    9
c ---[4128]---> BDD-cost:    9
c ---[4126]---> BDD-cost:    9
c ---[4124]---> BDD-cost:    9
c ---[4122]---> BDD-cost:    9
c ---[4120]---> BDD-cost:    9
c ---[4118]---> BDD-cost:    9
c ---[4116]---> BDD-cost:    9
c ---[4114]---> BDD-cost:    9
c ---[4112]---> BDD-cost:    9
c ---[4110]---> BDD-cost:    9
c ---[4108]---> BDD-cost:    9
c ---[4106]---> BDD-cost:    9
c ---[4104]---> BDD-cost:    9
c ---[4102]---> BDD-cost:    9
c ---[4100]---> BDD-cost:    9
c ---[4098]---> BDD-cost:    9
c ---[4096]---> BDD-cost:    9
c ---[4094]---> BDD-cost:    9
c ---[4092]---> BDD-cost:    9
c ---[4090]---> BDD-cost:    9
c ---[4088]---> BDD-cost:    9
c ---[4086]---> BDD-cost:    9
c ---[4079]---> BDD-cost:   64
c ---[4078]---> BDD-cost:   64
c ---[4077]---> BDD-cost:   64
c ---[4076]---> BDD-cost:   64
c ---[4075]---> BDD-cost:   64
c ---[4074]---> BDD-cost:   64
c ---[4067]---> BDD-cost:   67
c ---[4066]---> BDD-cost:   67
c ---[4065]---> BDD-cost:   67
c ---[4064]---> BDD-cost:   67
c ---[4063]---> BDD-cost:   67
c ---[4062]---> BDD-cost:   67
c ---[4055]---> BDD-cost:   67
c ---[4054]---> BDD-cost:   67
c ---[4053]---> BDD-cost:   67
c ---[4052]---> BDD-cost:   67
c ---[4051]---> BDD-cost:   67
c ---[4050]---> BDD-cost:   67
c ---[4043]---> BDD-cost:   67
c ---[4042]---> BDD-cost:   67
c ---[4041]---> BDD-cost:   67
c ---[4040]---> BDD-cost:   67
c ---[4039]---> BDD-cost:   67
c ---[4038]---> BDD-cost:   67
c ---[4031]---> BDD-cost:   67
c ---[4030]---> BDD-cost:   67
c ---[4029]---> BDD-cost:   67
c ---[4028]---> BDD-cost:   67
c ---[4027]---> BDD-cost:   67
c ---[4026]---> BDD-cost:   67
c ---[4019]---> BDD-cost:   67
c ---[4018]---> BDD-cost:   67
c ---[4017]---> BDD-cost:   67
c ---[4016]---> BDD-cost:   67
c ---[4015]---> BDD-cost:   67
c ---[4014]---> BDD-cost:   67
c ---[4007]---> BDD-cost:   67
c ---[4006]---> BDD-cost:   67
c ---[4005]---> BDD-cost:   67
c ---[4004]---> BDD-cost:   67
c ---[4003]---> BDD-cost:   67
c ---[4002]---> BDD-cost:   67
c ---[2050]---> BDD-cost:    7
c ---[2048]---> BDD-cost:    7
c ---[2046]---> BDD-cost:    7
c ---[2044]---> BDD-cost:    7
c ---[2042]---> BDD-cost:    7
c ---[2040]---> BDD-cost:    7
c ---[2038]---> BDD-cost:    7
c ---[2036]---> BDD-cost:    7
c ---[2034]---> BDD-cost:    7
c ---[2032]---> BDD-cost:    7
c ---[2030]---> BDD-cost:    7
c ---[2028]---> BDD-cost:    7
c ---[2026]---> BDD-cost:    7
c ---[2024]---> BDD-cost:    7
c ---[2022]---> BDD-cost:    7
c ---[2020]---> BDD-cost:    7
c ---[2018]---> BDD-cost:    7
c ---[2016]---> BDD-cost:    7
c ---[2014]---> BDD-cost:    7
c ---[2012]---> BDD-cost:    7
c ---[2010]---> BDD-cost:    7
c ---[2008]---> BDD-cost:    7
c ---[2006]---> BDD-cost:    7
c ---[2004]---> BDD-cost:    7
c ---[2002]---> BDD-cost:    7
c ---[2000]---> BDD-cost:    7
c ---[1998]---> BDD-cost:    7
c ---[1996]---> BDD-cost:    7
c ---[1994]---> BDD-cost:    7
c ---[1992]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    7
c ---[1988]---> BDD-cost:    7
c ---[1986]---> BDD-cost:    7
c ---[1984]---> BDD-cost:    7
c ---[1982]---> BDD-cost:    7
c ---[1980]---> BDD-cost:    7
c ---[1978]---> BDD-cost:    7
c ---[1976]---> BDD-cost:    7
c ---[1974]---> BDD-cost:    7
c ---[1972]---> BDD-cost:    7
c ---[1970]---> BDD-cost:    7
c ---[1968]---> BDD-cost:    7
c ---[1966]---> BDD-cost:    7
c ---[1964]---> BDD-cost:    7
c ---[1962]---> BDD-cost:    7
c ---[1960]---> BDD-cost:    7
c ---[1958]---> BDD-cost:    7
c ---[1956]---> BDD-cost:    7
c ---[1954]---> BDD-cost:    7
c ---[1952]---> BDD-cost:    7
c ---[1950]---> BDD-cost:    7
c ---[1948]---> BDD-cost:    7
c ---[1946]---> BDD-cost:    7
c ---[1944]---> BDD-cost:    7
c ---[1942]---> BDD-cost:    7
c ---[1940]---> BDD-cost:    7
c ---[1938]---> BDD-cost:    7
c ---[1936]---> BDD-cost:    7
c ---[1934]---> BDD-cost:    7
c ---[1932]---> BDD-cost:    7
c ---[1931]---> BDD-cost:    7
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:    7
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:    7
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1923]---> BDD-cost:    7
c ---[1922]---> BDD-cost:    7
c ---[1921]---> BDD-cost:    7
c ---[1920]---> BDD-cost:    7
c ---[1919]---> BDD-cost:    9
c ---[1918]---> BDD-cost:    2
c ---[1917]---> BDD-cost:    9
c ---[1916]---> BDD-cost:    2
c ---[1915]---> BDD-cost:    9
c ---[1914]---> BDD-cost:    2
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    2
c ---[1911]---> BDD-cost:    8
c ---[1910]---> BDD-cost:    2
c ---[1909]---> BDD-cost:    8
c ---[1908]---> BDD-cost:    2
c ---[1907]---> BDD-cost:    8
c ---[1906]---> BDD-cost:    2
c ---[1905]---> BDD-cost:    8
c ---[1904]---> BDD-cost:    2
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:    2
c ---[1901]---> BDD-cost:    7
c ---[1900]---> BDD-cost:    2
c ---[1899]---> BDD-cost:    7
c ---[1898]---> BDD-cost:    2
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:    2
c ---[1895]---> BDD-cost:    6
c ---[1894]---> BDD-cost:    2
c ---[1893]---> BDD-cost:    6
c ---[1892]---> BDD-cost:    2
c ---[1891]---> BDD-cost:    6
c ---[1890]---> BDD-cost:    2
c ---[1889]---> BDD-cost:    6
c ---[1888]---> BDD-cost:    2
c ---[1887]---> BDD-cost:    5
c ---[1886]---> BDD-cost:    2
c ---[1885]---> BDD-cost:    5
c ---[1884]---> BDD-cost:    2
c ---[1883]---> BDD-cost:    5
c ---[1882]---> BDD-cost:    2
c ---[1881]---> BDD-cost:    5
c ---[1880]---> BDD-cost:    2
c ---[1879]---> BDD-cost:    4
c ---[1878]---> BDD-cost:    2
c ---[1877]---> BDD-cost:    4
c ---[1876]---> BDD-cost:    2
c ---[1875]---> BDD-cost:    4
c ---[1874]---> BDD-cost:    2
c ---[1873]---> BDD-cost:    4
c ---[1872]---> BDD-cost:    2
c ---[1871]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    2
c ---[1869]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    2
c ---[1867]---> BDD-cost:    3
c ---[1866]---> BDD-cost:    2
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    2
c ---[1855]---> BDD-cost:    6
c ---[1854]---> BDD-cost:    2
c ---[1853]---> BDD-cost:    2
c ---[1852]---> BDD-cost:    2
c ---[1851]---> BDD-cost:    2
c ---[1850]---> BDD-cost:    2
c ---[1849]---> BDD-cost:    2
c ---[1848]---> BDD-cost:    2
c ---[1847]---> BDD-cost:    5
c ---[1846]---> BDD-cost:    2
c ---[1845]---> BDD-cost:    2
c ---[1844]---> BDD-cost:    2
c ---[1843]---> BDD-cost:    2
c ---[1842]---> BDD-cost:    2
c ---[1841]---> BDD-cost:    2
c ---[1840]---> BDD-cost:    2
c ---[1839]---> BDD-cost:    4
c ---[1838]---> BDD-cost:    2
c ---[1837]---> BDD-cost:    2
c ---[1836]---> BDD-cost:    2
c ---[1835]---> BDD-cost:    2
c ---[1834]---> BDD-cost:    2
c ---[1833]---> BDD-cost:    2
c ---[1832]---> BDD-cost:    2
c ---[1831]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    2
c ---[1829]---> BDD-cost:    2
c ---[1828]---> BDD-cost:    2
c ---[1827]---> BDD-cost:    2
c ---[1826]---> BDD-cost:    2
c ---[1825]---> BDD-cost:    2
c ---[1824]---> BDD-cost:    2
c ---[1823]---> BDD-cost:    2
c ---[1822]---> BDD-cost:    2
c ---[1821]---> BDD-cost:    2
c ---[1820]---> BDD-cost:    2
c ---[1819]---> BDD-cost:    2
c ---[1818]---> BDD-cost:    2
c ---[1817]---> BDD-cost:    2
c ---[1816]---> BDD-cost:    2
c ---[1815]---> BDD-cost:    4
c ---[1814]---> BDD-cost:    2
c ---[1813]---> BDD-cost:    2
c ---[1812]---> BDD-cost:    2
c ---[1811]---> BDD-cost:    2
c ---[1810]---> BDD-cost:    2
c ---[1809]---> BDD-cost:    2
c ---[1808]---> BDD-cost:    2
c ---[1807]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    2
c ---[1805]---> BDD-cost:    2
c ---[1804]---> BDD-cost:    2
c ---[1803]---> BDD-cost:    2
c ---[1802]---> BDD-cost:    2
c ---[1801]---> BDD-cost:    2
c ---[1800]---> BDD-cost:    2
c ---[1791]---> BDD-cost:    2
c ---[1790]---> BDD-cost:    2
c ---[1789]---> BDD-cost:    2
c ---[1788]---> BDD-cost:    2
c ---[1787]---> BDD-cost:    2
c ---[1786]---> BDD-cost:    2
c ---[1785]---> BDD-cost:    2
c ---[1784]---> BDD-cost:    2
c ---[1783]---> BDD-cost:    2
c ---[1782]---> BDD-cost:    2
c ---[1781]---> BDD-cost:    2
c ---[1780]---> BDD-cost:    2
c ---[1779]---> BDD-cost:    2
c ---[1778]---> BDD-cost:    2
c ---[1777]---> BDD-cost:    2
c ---[1776]---> BDD-cost:    2
c ---[1775]---> BDD-cost:    2
c ---[1774]---> BDD-cost:    2
c ---[1773]---> BDD-cost:    2
c ---[1772]---> BDD-cost:    2
c ---[1771]---> BDD-cost:    2
c ---[1770]---> BDD-cost:    2
c ---[1769]---> BDD-cost:    2
c ---[1768]---> BDD-cost:    2
c ---[1767]---> BDD-cost:    2
c ---[1766]---> BDD-cost:    2
c ---[1765]---> BDD-cost:    2
c ---[1764]---> BDD-cost:    2
c ---[1763]---> BDD-cost:    2
c ---[1762]---> BDD-cost:    2
c ---[1761]---> BDD-cost:    2
c ---[1760]---> BDD-cost:    2
c ---[1759]---> BDD-cost:    2
c ---[1758]---> BDD-cost:    2
c ---[1757]---> BDD-cost:    2
c ---[1756]---> BDD-cost:    2
c ---[1755]---> BDD-cost:    2
c ---[1754]---> BDD-cost:    2
c ---[1753]---> BDD-cost:    2
c ---[1752]---> BDD-cost:    2
c ---[1751]---> BDD-cost:    2
c ---[1750]---> BDD-cost:    2
c ---[1749]---> BDD-cost:    2
c ---[1748]---> BDD-cost:    2
c ---[1747]---> BDD-cost:    2
c ---[1746]---> BDD-cost:    2
c ---[1745]---> BDD-cost:    2
c ---[1744]---> BDD-cost:    2
c ---[1743]---> BDD-cost:    2
c ---[1742]---> BDD-cost:    2
c ---[1741]---> BDD-cost:    2
c ---[1740]---> BDD-cost:    2
c ---[1739]---> BDD-cost:    2
c ---[1738]---> BDD-cost:    2
c ---[1737]---> BDD-cost:    2
c ---[1736]---> BDD-cost:    2
c ---[1727]---> BDD-cost:    2
c ---[1726]---> BDD-cost:    2
c ---[1725]---> BDD-cost:    2
c ---[1724]---> BDD-cost:    2
c ---[1723]---> BDD-cost:    2
c ---[1722]---> BDD-cost:    2
c ---[1721]---> BDD-cost:    2
c ---[1720]---> BDD-cost:    2
c ---[1719]---> BDD-cost:    2
c ---[1718]---> BDD-cost:    2
c ---[1717]---> BDD-cost:    2
c ---[1716]---> BDD-cost:    2
c ---[1715]---> BDD-cost:    2
c ---[1714]---> BDD-cost:    2
c ---[1713]---> BDD-cost:    2
c ---[1712]---> BDD-cost:    2
c ---[1711]---> BDD-cost:    2
c ---[1710]---> BDD-cost:    2
c ---[1709]---> BDD-cost:    2
c ---[1708]---> BDD-cost:    2
c ---[1707]---> BDD-cost:    2
c ---[1706]---> BDD-cost:    2
c ---[1705]---> BDD-cost:    2
c ---[1704]---> BDD-cost:    2
c ---[1703]---> BDD-cost:    2
c ---[1702]---> BDD-cost:    2
c ---[1701]---> BDD-cost:    2
c ---[1700]---> BDD-cost:    2
c ---[1699]---> BDD-cost:    2
c ---[1698]---> BDD-cost:    2
c ---[1697]---> BDD-cost:    2
c ---[1696]---> BDD-cost:    2
c ---[1695]---> BDD-cost:    2
c ---[1694]---> BDD-cost:    2
c ---[1693]---> BDD-cost:    2
c ---[1692]---> BDD-cost:    2
c ---[1691]---> BDD-cost:    2
c ---[1690]---> BDD-cost:    2
c ---[1689]---> BDD-cost:    2
c ---[1688]---> BDD-cost:    2
c ---[1687]---> BDD-cost:    2
c ---[1686]---> BDD-cost:    2
c ---[1685]---> BDD-cost:    2
c ---[1684]---> BDD-cost:    2
c ---[1683]---> BDD-cost:    2
c ---[1682]---> BDD-cost:    2
c ---[1681]---> BDD-cost:    2
c ---[1680]---> BDD-cost:    2
c ---[1679]---> BDD-cost:    2
c ---[1678]---> BDD-cost:    2
c ---[1677]---> BDD-cost:    2
c ---[1676]---> BDD-cost:    2
c ---[1675]---> BDD-cost:    2
c ---[1674]---> BDD-cost:    2
c ---[1673]---> BDD-cost:    2
c ---[1672]---> BDD-cost:    2
c ---[1663]---> BDD-cost:    2
c ---[1662]---> BDD-cost:    2
c ---[1661]---> BDD-cost:    2
c ---[1660]---> BDD-cost:    2
c ---[1659]---> BDD-cost:    2
c ---[1658]---> BDD-cost:    2
c ---[1657]---> BDD-cost:    2
c ---[1656]---> BDD-cost:    2
c ---[1655]---> BDD-cost:    2
c ---[1654]---> BDD-cost:    2
c ---[1653]---> BDD-cost:    2
c ---[1652]---> BDD-cost:    2
c ---[1651]---> BDD-cost:    2
c ---[1650]---> BDD-cost:    2
c ---[1649]---> BDD-cost:    2
c ---[1648]---> BDD-cost:    2
c ---[1647]---> BDD-cost:    2
c ---[1646]---> BDD-cost:    2
c ---[1645]---> BDD-cost:    2
c ---[1644]---> BDD-cost:    2
c ---[1643]---> BDD-cost:    2
c ---[1642]---> BDD-cost:    2
c ---[1641]---> BDD-cost:    2
c ---[1640]---> BDD-cost:    2
c ---[1639]---> BDD-cost:    2
c ---[1638]---> BDD-cost:    2
c ---[1637]---> BDD-cost:    2
c ---[1636]---> BDD-cost:    2
c ---[1635]---> BDD-cost:    2
c ---[1634]---> BDD-cost:    2
c ---[1633]---> BDD-cost:    2
c ---[1632]---> BDD-cost:    2
c ---[1631]---> BDD-cost:    2
c ---[1630]---> BDD-cost:    2
c ---[1629]---> BDD-cost:    2
c ---[1628]---> BDD-cost:    2
c ---[1627]---> BDD-cost:    2
c ---[1626]---> BDD-cost:    2
c ---[1625]---> BDD-cost:    2
c ---[1624]---> BDD-cost:    2
c ---[1623]---> BDD-cost:    2
c ---[1622]---> BDD-cost:    2
c ---[1621]---> BDD-cost:    2
c ---[1620]---> BDD-cost:    2
c ---[1619]---> BDD-cost:    2
c ---[1618]---> BDD-cost:    2
c ---[1617]---> BDD-cost:    2
c ---[1616]---> BDD-cost:    2
c ---[1615]---> BDD-cost:    2
c ---[1614]---> BDD-cost:    2
c ---[1613]---> BDD-cost:    2
c ---[1612]---> BDD-cost:    2
c ---[1611]---> BDD-cost:    2
c ---[1610]---> BDD-cost:    2
c ---[1609]---> BDD-cost:    2
c ---[1608]---> BDD-cost:    2
c ---[1599]---> BDD-cost:    9
c ---[1598]---> BDD-cost:    2
c ---[1597]---> BDD-cost:    9
c ---[1596]---> BDD-cost:    2
c ---[1595]---> BDD-cost:    9
c ---[1594]---> BDD-cost:    2
c ---[1593]---> BDD-cost:    9
c ---[1592]---> BDD-cost:    2
c ---[1591]---> BDD-cost:    8
c ---[1590]---> BDD-cost:    2
c ---[1589]---> BDD-cost:    8
c ---[1588]---> BDD-cost:    2
c ---[1587]---> BDD-cost:    8
c ---[1586]---> BDD-cost:    2
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    2
c ---[1583]---> BDD-cost:    7
c ---[1582]---> BDD-cost:    2
c ---[1581]---> BDD-cost:    7
c ---[1580]---> BDD-cost:    2
c ---[1579]---> BDD-cost:    7
c ---[1578]---> BDD-cost:    2
c ---[1577]---> BDD-cost:    7
c ---[1576]---> BDD-cost:    2
c ---[1575]---> BDD-cost:    6
c ---[1574]---> BDD-cost:    2
c ---[1573]---> BDD-cost:    6
c ---[1572]---> BDD-cost:    2
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    2
c ---[1569]---> BDD-cost:    6
c ---[1568]---> BDD-cost:    2
c ---[1567]---> BDD-cost:    5
c ---[1566]---> BDD-cost:    2
c ---[1565]---> BDD-cost:    5
c ---[1564]---> BDD-cost:    2
c ---[1563]---> BDD-cost:    5
c ---[1562]---> BDD-cost:    2
c ---[1561]---> BDD-cost:    5
c ---[1560]---> BDD-cost:    2
c ---[1559]---> BDD-cost:    4
c ---[1558]---> BDD-cost:    2
c ---[1557]---> BDD-cost:    4
c ---[1556]---> BDD-cost:    2
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    2
c ---[1553]---> BDD-cost:    4
c ---[1552]---> BDD-cost:    2
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    2
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    2
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    2
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    2
c ---[1535]---> BDD-cost:    6
c ---[1534]---> BDD-cost:    2
c ---[1533]---> BDD-cost:    2
c ---[1532]---> BDD-cost:    2
c ---[1531]---> BDD-cost:    2
c ---[1530]---> BDD-cost:    2
c ---[1529]---> BDD-cost:    2
c ---[1528]---> BDD-cost:    2
c ---[1527]---> BDD-cost:    5
c ---[1526]---> BDD-cost:    2
c ---[1525]---> BDD-cost:    2
c ---[1524]---> BDD-cost:    2
c ---[1523]---> BDD-cost:    2
c ---[1522]---> BDD-cost:    2
c ---[1521]---> BDD-cost:    2
c ---[1520]---> BDD-cost:    2
c ---[1519]---> BDD-cost:    4
c ---[1518]---> BDD-cost:    2
c ---[1517]---> BDD-cost:    2
c ---[1516]---> BDD-cost:    2
c ---[1515]---> BDD-cost:    2
c ---[1514]---> BDD-cost:    2
c ---[1513]---> BDD-cost:    2
c ---[1512]---> BDD-cost:    2
c ---[1511]---> BDD-cost:    3
c ---[1510]---> BDD-cost:    2
c ---[1509]---> BDD-cost:    2
c ---[1508]---> BDD-cost:    2
c ---[1507]---> BDD-cost:    2
c ---[1506]---> BDD-cost:    2
c ---[1505]---> BDD-cost:    2
c ---[1504]---> BDD-cost:    2
c ---[1503]---> BDD-cost:    2
c ---[1502]---> BDD-cost:    2
c ---[1501]---> BDD-cost:    2
c ---[1500]---> BDD-cost:    2
c ---[1499]---> BDD-cost:    2
c ---[1498]---> BDD-cost:    2
c ---[1497]---> BDD-cost:    2
c ---[1496]---> BDD-cost:    2
c ---[1495]---> BDD-cost:    4
c ---[1494]---> BDD-cost:    2
c ---[1493]---> BDD-cost:    2
c ---[1492]---> BDD-cost:    2
c ---[1491]---> BDD-cost:    2
c ---[1490]---> BDD-cost:    2
c ---[1489]---> BDD-cost:    2
c ---[1488]---> BDD-cost:    2
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    2
c ---[1485]---> BDD-cost:    2
c ---[1484]---> BDD-cost:    2
c ---[1483]---> BDD-cost:    2
c ---[1482]---> BDD-cost:    2
c ---[1481]---> BDD-cost:    2
c ---[1480]---> BDD-cost:    2
c ---[1471]---> BDD-cost:    2
c ---[1470]---> BDD-cost:    2
c ---[1469]---> BDD-cost:    2
c ---[1468]---> BDD-cost:    2
c ---[1467]---> BDD-cost:    2
c ---[1466]---> BDD-cost:    2
c ---[1465]---> BDD-cost:    2
c ---[1464]---> BDD-cost:    2
c ---[1463]---> BDD-cost:    2
c ---[1462]---> BDD-cost:    2
c ---[1461]---> BDD-cost:    2
c ---[1460]---> BDD-cost:    2
c ---[1459]---> BDD-cost:    2
c ---[1458]---> BDD-cost:    2
c ---[1457]---> BDD-cost:    2
c ---[1456]---> BDD-cost:    2
c ---[1455]---> BDD-cost:    2
c ---[1454]---> BDD-cost:    2
c ---[1453]---> BDD-cost:    2
c ---[1452]---> BDD-cost:    2
c ---[1451]---> BDD-cost:    2
c ---[1450]---> BDD-cost:    2
c ---[1449]---> BDD-cost:    2
c ---[1448]---> BDD-cost:    2
c ---[1447]---> BDD-cost:    2
c ---[1446]---> BDD-cost:    2
c ---[1445]---> BDD-cost:    2
c ---[1444]---> BDD-cost:    2
c ---[1443]---> BDD-cost:    2
c ---[1442]---> BDD-cost:    2
c ---[1441]---> BDD-cost:    2
c ---[1440]---> BDD-cost:    2
c ---[1439]---> BDD-cost:    2
c ---[1438]---> BDD-cost:    2
c ---[1437]---> BDD-cost:    2
c ---[1436]---> BDD-cost:    2
c ---[1435]---> BDD-cost:    2
c ---[1434]---> BDD-cost:    2
c ---[1433]---> BDD-cost:    2
c ---[1432]---> BDD-cost:    2
c ---[1431]---> BDD-cost:    2
c ---[1430]---> BDD-cost:    2
c ---[1429]---> BDD-cost:    2
c ---[1428]---> BDD-cost:    2
c ---[1427]---> BDD-cost:    2
c ---[1426]---> BDD-cost:    2
c ---[1425]---> BDD-cost:    2
c ---[1424]---> BDD-cost:    2
c ---[1423]---> BDD-cost:    2
c ---[1422]---> BDD-cost:    2
c ---[1421]---> BDD-cost:    2
c ---[1420]---> BDD-cost:    2
c ---[1419]---> BDD-cost:    2
c ---[1418]---> BDD-cost:    2
c ---[1417]---> BDD-cost:    2
c ---[1416]---> BDD-cost:    2
c ---[1407]---> BDD-cost:    2
c ---[1406]---> BDD-cost:    2
c ---[1405]---> BDD-cost:    2
c ---[1404]---> BDD-cost:    2
c ---[1403]---> BDD-cost:    2
c ---[1402]---> BDD-cost:    2
c ---[1401]---> BDD-cost:    2
c ---[1400]---> BDD-cost:    2
c ---[1399]---> BDD-cost:    2
c ---[1398]---> BDD-cost:    2
c ---[1397]---> BDD-cost:    2
c ---[1396]---> BDD-cost:    2
c ---[1395]---> BDD-cost:    2
c ---[1394]---> BDD-cost:    2
c ---[1393]---> BDD-cost:    2
c ---[1392]---> BDD-cost:    2
c ---[1391]---> BDD-cost:    2
c ---[1390]---> BDD-cost:    2
c ---[1389]---> BDD-cost:    2
c ---[1388]---> BDD-cost:    2
c ---[1387]---> BDD-cost:    2
c ---[1386]---> BDD-cost:    2
c ---[1385]---> BDD-cost:    2
c ---[1384]---> BDD-cost:    2
c ---[1383]---> BDD-cost:    2
c ---[1382]---> BDD-cost:    2
c ---[1381]---> BDD-cost:    2
c ---[1380]---> BDD-cost:    2
c ---[1379]---> BDD-cost:    2
c ---[1378]---> BDD-cost:    2
c ---[1377]---> BDD-cost:    2
c ---[1376]---> BDD-cost:    2
c ---[1375]---> BDD-cost:    2
c ---[1374]---> BDD-cost:    2
c ---[1373]---> BDD-cost:    2
c ---[1372]---> BDD-cost:    2
c ---[1371]---> BDD-cost:    2
c ---[1370]---> BDD-cost:    2
c ---[1369]---> BDD-cost:    2
c ---[1368]---> BDD-cost:    2
c ---[1367]---> BDD-cost:    2
c ---[1366]---> BDD-cost:    2
c ---[1365]---> BDD-cost:    2
c ---[1364]---> BDD-cost:    2
c ---[1363]---> BDD-cost:    2
c ---[1362]---> BDD-cost:    2
c ---[1361]---> BDD-cost:    2
c ---[1360]---> BDD-cost:    2
c ---[1359]---> BDD-cost:    2
c ---[1358]---> BDD-cost:    2
c ---[1357]---> BDD-cost:    2
c ---[1356]---> BDD-cost:    2
c ---[1355]---> BDD-cost:    2
c ---[1354]---> BDD-cost:    2
c ---[1353]---> BDD-cost:    2
c ---[1352]---> BDD-cost:    2
c ---[1343]---> BDD-cost:    2
c ---[1342]---> BDD-cost:    2
c ---[1341]---> BDD-cost:    2
c ---[1340]---> BDD-cost:    2
c ---[1339]---> BDD-cost:    2
c ---[1338]---> BDD-cost:    2
c ---[1337]---> BDD-cost:    2
c ---[1336]---> BDD-cost:    2
c ---[1335]---> BDD-cost:    2
c ---[1334]---> BDD-cost:    2
c ---[1333]---> BDD-cost:    2
c ---[1332]---> BDD-cost:    2
c ---[1331]---> BDD-cost:    2
c ---[1330]---> BDD-cost:    2
c ---[1329]---> BDD-cost:    2
c ---[1328]---> BDD-cost:    2
c ---[1327]---> BDD-cost:    2
c ---[1326]---> BDD-cost:    2
c ---[1325]---> BDD-cost:    2
c ---[1324]---> BDD-cost:    2
c ---[1323]---> BDD-cost:    2
c ---[1322]---> BDD-cost:    2
c ---[1321]---> BDD-cost:    2
c ---[1320]---> BDD-cost:    2
c ---[1319]---> BDD-cost:    2
c ---[1318]---> BDD-cost:    2
c ---[1317]---> BDD-cost:    2
c ---[1316]---> BDD-cost:    2
c ---[1315]---> BDD-cost:    2
c ---[1314]---> BDD-cost:    2
c ---[1313]---> BDD-cost:    2
c ---[1312]---> BDD-cost:    2
c ---[1311]---> BDD-cost:    2
c ---[1310]---> BDD-cost:    2
c ---[1309]---> BDD-cost:    2
c ---[1308]---> BDD-cost:    2
c ---[1307]---> BDD-cost:    2
c ---[1306]---> BDD-cost:    2
c ---[1305]---> BDD-cost:    2
c ---[1304]---> BDD-cost:    2
c ---[1303]---> BDD-cost:    2
c ---[1302]---> BDD-cost:    2
c ---[1301]---> BDD-cost:    2
c ---[1300]---> BDD-cost:    2
c ---[1299]---> BDD-cost:    2
c ---[1298]---> BDD-cost:    2
c ---[1297]---> BDD-cost:    2
c ---[1296]---> BDD-cost:    2
c ---[1295]---> BDD-cost:    2
c ---[1294]---> BDD-cost:    2
c ---[1293]---> BDD-cost:    2
c ---[1292]---> BDD-cost:    2
c ---[1291]---> BDD-cost:    2
c ---[1290]---> BDD-cost:    2
c ---[1289]---> BDD-cost:    2
c ---[1288]---> BDD-cost:    2
c ---[1279]---> BDD-cost:    9
c ---[1278]---> BDD-cost:    2
c ---[1277]---> BDD-cost:    9
c ---[1276]---> BDD-cost:    2
c ---[1275]---> BDD-cost:    9
c ---[1274]---> BDD-cost:    2
c ---[1273]---> BDD-cost:    9
c ---[1272]---> BDD-cost:    2
c ---[1271]---> BDD-cost:    8
c ---[1270]---> BDD-cost:    2
c ---[1269]---> BDD-cost:    8
c ---[1268]---> BDD-cost:    2
c ---[1267]---> BDD-cost:    8
c ---[1266]---> BDD-cost:    2
c ---[1265]---> BDD-cost:    8
c ---[1264]---> BDD-cost:    2
c ---[1263]---> BDD-cost:    7
c ---[1262]---> BDD-cost:    2
c ---[1261]---> BDD-cost:    7
c ---[1260]---> BDD-cost:    2
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    2
c ---[1257]---> BDD-cost:    7
c ---[1256]---> BDD-cost:    2
c ---[1255]---> BDD-cost:    6
c ---[1254]---> BDD-cost:    2
c ---[1253]---> BDD-cost:    6
c ---[1252]---> BDD-cost:    2
c ---[1251]---> BDD-cost:    6
c ---[1250]---> BDD-cost:    2
c ---[1249]---> BDD-cost:    6
c ---[1248]---> BDD-cost:    2
c ---[1247]---> BDD-cost:    5
c ---[1246]---> BDD-cost:    2
c ---[1245]---> BDD-cost:    5
c ---[1244]---> BDD-cost:    2
c ---[1243]---> BDD-cost:    5
c ---[1242]---> BDD-cost:    2
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    2
c ---[1239]---> BDD-cost:    4
c ---[1238]---> BDD-cost:    2
c ---[1237]---> BDD-cost:    4
c ---[1236]---> BDD-cost:    2
c ---[1235]---> BDD-cost:    4
c ---[1234]---> BDD-cost:    2
c ---[1233]---> BDD-cost:    4
c ---[1232]---> BDD-cost:    2
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    2
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    2
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    2
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    2
c ---[1215]---> BDD-cost:    6
c ---[1214]---> BDD-cost:    2
c ---[1213]---> BDD-cost:    2
c ---[1212]---> BDD-cost:    2
c ---[1211]---> BDD-cost:    2
c ---[1210]---> BDD-cost:    2
c ---[1209]---> BDD-cost:    2
c ---[1208]---> BDD-cost:    2
c ---[1207]---> BDD-cost:    5
c ---[1206]---> BDD-cost:    2
c ---[1205]---> BDD-cost:    2
c ---[1204]---> BDD-cost:    2
c ---[1203]---> BDD-cost:    2
c ---[1202]---> BDD-cost:    2
c ---[1201]---> BDD-cost:    2
c ---[1200]---> BDD-cost:    2
c ---[1199]---> BDD-cost:    4
c ---[1198]---> BDD-cost:    2
c ---[1197]---> BDD-cost:    2
c ---[1196]---> BDD-cost:    2
c ---[1195]---> BDD-cost:    2
c ---[1194]---> BDD-cost:    2
c ---[1193]---> BDD-cost:    2
c ---[1192]---> BDD-cost:    2
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    2
c ---[1189]---> BDD-cost:    2
c ---[1188]---> BDD-cost:    2
c ---[1187]---> BDD-cost:    2
c ---[1186]---> BDD-cost:    2
c ---[1185]---> BDD-cost:    2
c ---[1184]---> BDD-cost:    2
c ---[1183]---> BDD-cost:    2
c ---[1182]---> BDD-cost:    2
c ---[1181]---> BDD-cost:    2
c ---[1180]---> BDD-cost:    2
c ---[1179]---> BDD-cost:    2
c ---[1178]---> BDD-cost:    2
c ---[1177]---> BDD-cost:    2
c ---[1176]---> BDD-cost:    2
c ---[1175]---> BDD-cost:    4
c ---[1174]---> BDD-cost:    2
c ---[1173]---> BDD-cost:    2
c ---[1172]---> BDD-cost:    2
c ---[1171]---> BDD-cost:    2
c ---[1170]---> BDD-cost:    2
c ---[1169]---> BDD-cost:    2
c ---[1168]---> BDD-cost:    2
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    2
c ---[1165]---> BDD-cost:    2
c ---[1164]---> BDD-cost:    2
c ---[1163]---> BDD-cost:    2
c ---[1162]---> BDD-cost:    2
c ---[1161]---> BDD-cost:    2
c ---[1160]---> BDD-cost:    2
c ---[1151]---> BDD-cost:    2
c ---[1150]---> BDD-cost:    2
c ---[1149]---> BDD-cost:    2
c ---[1148]---> BDD-cost:    2
c ---[1147]---> BDD-cost:    2
c ---[1146]---> BDD-cost:    2
c ---[1145]---> BDD-cost:    2
c ---[1144]---> BDD-cost:    2
c ---[1143]---> BDD-cost:    2
c ---[1142]---> BDD-cost:    2
c ---[1141]---> BDD-cost:    2
c ---[1140]---> BDD-cost:    2
c ---[1139]---> BDD-cost:    2
c ---[1138]---> BDD-cost:    2
c ---[1137]---> BDD-cost:    2
c ---[1136]---> BDD-cost:    2
c ---[1135]---> BDD-cost:    2
c ---[1134]---> BDD-cost:    2
c ---[1133]---> BDD-cost:    2
c ---[1132]---> BDD-cost:    2
c ---[1131]---> BDD-cost:    2
c ---[1130]---> BDD-cost:    2
c ---[1129]---> BDD-cost:    2
c ---[1128]---> BDD-cost:    2
c ---[1127]---> BDD-cost:    2
c ---[1126]---> BDD-cost:    2
c ---[1125]---> BDD-cost:    2
c ---[1124]---> BDD-cost:    2
c ---[1123]---> BDD-cost:    2
c ---[1122]---> BDD-cost:    2
c ---[1121]---> BDD-cost:    2
c ---[1120]---> BDD-cost:    2
c ---[1119]---> BDD-cost:    2
c ---[1118]---> BDD-cost:    2
c ---[1117]---> BDD-cost:    2
c ---[1116]---> BDD-cost:    2
c ---[1115]---> BDD-cost:    2
c ---[1114]---> BDD-cost:    2
c ---[1113]---> BDD-cost:    2
c ---[1112]---> BDD-cost:    2
c ---[1111]---> BDD-cost:    2
c ---[1110]---> BDD-cost:    2
c ---[1109]---> BDD-cost:    2
c ---[1108]---> BDD-cost:    2
c ---[1107]---> BDD-cost:    2
c ---[1106]---> BDD-cost:    2
c ---[1105]---> BDD-cost:    2
c ---[1104]---> BDD-cost:    2
c ---[1103]---> BDD-cost:    2
c ---[1102]---> BDD-cost:    2
c ---[1101]---> BDD-cost:    2
c ---[1100]---> BDD-cost:    2
c ---[1099]---> BDD-cost:    2
c ---[1098]---> BDD-cost:    2
c ---[1097]---> BDD-cost:    2
c ---[1096]---> BDD-cost:    2
c ---[1087]---> BDD-cost:    2
c ---[1086]---> BDD-cost:    2
c ---[1085]---> BDD-cost:    2
c ---[1084]---> BDD-cost:    2
c ---[1083]---> BDD-cost:    2
c ---[1082]---> BDD-cost:    2
c ---[1081]---> BDD-cost:    2
c ---[1080]---> BDD-cost:    2
c ---[1079]---> BDD-cost:    2
c ---[1078]---> BDD-cost:    2
c ---[1077]---> BDD-cost:    2
c ---[1076]---> BDD-cost:    2
c ---[1075]---> BDD-cost:    2
c ---[1074]---> BDD-cost:    2
c ---[1073]---> BDD-cost:    2
c ---[1072]---> BDD-cost:    2
c ---[1071]---> BDD-cost:    2
c ---[1070]---> BDD-cost:    2
c ---[1069]---> BDD-cost:    2
c ---[1068]---> BDD-cost:    2
c ---[1067]---> BDD-cost:    2
c ---[1066]---> BDD-cost:    2
c ---[1065]---> BDD-cost:    2
c ---[1064]---> BDD-cost:    2
c ---[1063]---> BDD-cost:    2
c ---[1062]---> BDD-cost:    2
c ---[1061]---> BDD-cost:    2
c ---[1060]---> BDD-cost:    2
c ---[1059]---> BDD-cost:    2
c ---[1058]---> BDD-cost:    2
c ---[1057]---> BDD-cost:    2
c ---[1056]---> BDD-cost:    2
c ---[1055]---> BDD-cost:    2
c ---[1054]---> BDD-cost:    2
c ---[1053]---> BDD-cost:    2
c ---[1052]---> BDD-cost:    2
c ---[1051]---> BDD-cost:    2
c ---[1050]---> BDD-cost:    2
c ---[1049]---> BDD-cost:    2
c ---[1048]---> BDD-cost:    2
c ---[1047]---> BDD-cost:    2
c ---[1046]---> BDD-cost:    2
c ---[1045]---> BDD-cost:    2
c ---[1044]---> BDD-cost:    2
c ---[1043]---> BDD-cost:    2
c ---[1042]---> BDD-cost:    2
c ---[1041]---> BDD-cost:    2
c ---[1040]---> BDD-cost:    2
c ---[1039]---> BDD-cost:    2
c ---[1038]---> BDD-cost:    2
c ---[1037]---> BDD-cost:    2
c ---[1036]---> BDD-cost:    2
c ---[1035]---> BDD-cost:    2
c ---[1034]---> BDD-cost:    2
c ---[1033]---> BDD-cost:    2
c ---[1032]---> BDD-cost:    2
c ---[1023]---> BDD-cost:    2
c ---[1022]---> BDD-cost:    2
c ---[1021]---> BDD-cost:    2
c ---[1020]---> BDD-cost:    2
c ---[1019]---> BDD-cost:    2
c ---[1018]---> BDD-cost:    2
c ---[1017]---> BDD-cost:    2
c ---[1016]---> BDD-cost:    2
c ---[1015]---> BDD-cost:    2
c ---[1014]---> BDD-cost:    2
c ---[1013]---> BDD-cost:    2
c ---[1012]---> BDD-cost:    2
c ---[1011]---> BDD-cost:    2
c ---[1010]---> BDD-cost:    2
c ---[1009]---> BDD-cost:    2
c ---[1008]---> BDD-cost:    2
c ---[1007]---> BDD-cost:    2
c ---[1006]---> BDD-cost:    2
c ---[1005]---> BDD-cost:    2
c ---[1004]---> BDD-cost:    2
c ---[1003]---> BDD-cost:    2
c ---[1002]---> BDD-cost:    2
c ---[1001]---> BDD-cost:    2
c ---[1000]---> BDD-cost:    2
c ---[ 999]---> BDD-cost:    2
c ---[ 998]---> BDD-cost:    2
c ---[ 997]---> BDD-cost:    2
c ---[ 996]---> BDD-cost:    2
c ---[ 995]---> BDD-cost:    2
c ---[ 994]---> BDD-cost:    2
c ---[ 993]---> BDD-cost:    2
c ---[ 992]---> BDD-cost:    2
c ---[ 991]---> BDD-cost:    2
c ---[ 990]---> BDD-cost:    2
c ---[ 989]---> BDD-cost:    2
c ---[ 988]---> BDD-cost:    2
c ---[ 987]---> BDD-cost:    2
c ---[ 986]---> BDD-cost:    2
c ---[ 985]---> BDD-cost:    2
c ---[ 984]---> BDD-cost:    2
c ---[ 983]---> BDD-cost:    2
c ---[ 982]---> BDD-cost:    2
c ---[ 981]---> BDD-cost:    2
c ---[ 980]---> BDD-cost:    2
c ---[ 979]---> BDD-cost:    2
c ---[ 978]---> BDD-cost:    2
c ---[ 977]---> BDD-cost:    2
c ---[ 976]---> BDD-cost:    2
c ---[ 975]---> BDD-cost:    2
c ---[ 974]---> BDD-cost:    2
c ---[ 973]---> BDD-cost:    2
c ---[ 972]---> BDD-cost:    2
c ---[ 971]---> BDD-cost:    2
c ---[ 970]---> BDD-cost:    2
c ---[ 969]---> BDD-cost:    2
c ---[ 968]---> BDD-cost:    2
c ---[ 959]---> BDD-cost:    9
c ---[ 958]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    9
c ---[ 956]---> BDD-cost:    2
c ---[ 955]---> BDD-cost:    9
c ---[ 954]---> BDD-cost:    2
c ---[ 953]---> BDD-cost:    9
c ---[ 952]---> BDD-cost:    2
c ---[ 951]---> BDD-cost:    8
c ---[ 950]---> BDD-cost:    2
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    2
c ---[ 947]---> BDD-cost:    8
c ---[ 946]---> BDD-cost:    2
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    2
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    2
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    2
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    2
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    2
c ---[ 935]---> BDD-cost:    6
c ---[ 934]---> BDD-cost:    2
c ---[ 933]---> BDD-cost:    6
c ---[ 932]---> BDD-cost:    2
c ---[ 931]---> BDD-cost:    6
c ---[ 930]---> BDD-cost:    2
c ---[ 929]---> BDD-cost:    6
c ---[ 928]---> BDD-cost:    2
c ---[ 927]---> BDD-cost:    5
c ---[ 926]---> BDD-cost:    2
c ---[ 925]---> BDD-cost:    5
c ---[ 924]---> BDD-cost:    2
c ---[ 923]---> BDD-cost:    5
c ---[ 922]---> BDD-cost:    2
c ---[ 921]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:    2
c ---[ 919]---> BDD-cost:    4
c ---[ 918]---> BDD-cost:    2
c ---[ 917]---> BDD-cost:    4
c ---[ 916]---> BDD-cost:    2
c ---[ 915]---> BDD-cost:    4
c ---[ 914]---> BDD-cost:    2
c ---[ 913]---> BDD-cost:    4
c ---[ 912]---> BDD-cost:    2
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    2
c ---[ 909]---> BDD-cost:    3
c ---[ 908]---> BDD-cost:    2
c ---[ 907]---> BDD-cost:    3
c ---[ 906]---> BDD-cost:    2
c ---[ 905]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    2
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    2
c ---[ 893]---> BDD-cost:    2
c ---[ 892]---> BDD-cost:    2
c ---[ 891]---> BDD-cost:    2
c ---[ 890]---> BDD-cost:    2
c ---[ 889]---> BDD-cost:    2
c ---[ 888]---> BDD-cost:    2
c ---[ 887]---> BDD-cost:    5
c ---[ 886]---> BDD-cost:    2
c ---[ 885]---> BDD-cost:    2
c ---[ 884]---> BDD-cost:    2
c ---[ 883]---> BDD-cost:    2
c ---[ 882]---> BDD-cost:    2
c ---[ 881]---> BDD-cost:    2
c ---[ 880]---> BDD-cost:    2
c ---[ 879]---> BDD-cost:    4
c ---[ 878]---> BDD-cost:    2
c ---[ 877]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    2
c ---[ 875]---> BDD-cost:    2
c ---[ 874]---> BDD-cost:    2
c ---[ 873]---> BDD-cost:    2
c ---[ 872]---> BDD-cost:    2
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    2
c ---[ 869]---> BDD-cost:    2
c ---[ 868]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 866]---> BDD-cost:    2
c ---[ 865]---> BDD-cost:    2
c ---[ 864]---> BDD-cost:    2
c ---[ 863]---> BDD-cost:    2
c ---[ 862]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 859]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    2
c ---[ 857]---> BDD-cost:    2
c ---[ 856]---> BDD-cost:    2
c ---[ 855]---> BDD-cost:    4
c ---[ 854]---> BDD-cost:    2
c ---[ 853]---> BDD-cost:    2
c ---[ 852]---> BDD-cost:    2
c ---[ 851]---> BDD-cost:    2
c ---[ 850]---> BDD-cost:    2
c ---[ 849]---> BDD-cost:    2
c ---[ 848]---> BDD-cost:    2
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 844]---> BDD-cost:    2
c ---[ 843]---> BDD-cost:    2
c ---[ 842]---> BDD-cost:    2
c ---[ 841]---> BDD-cost:    2
c ---[ 840]---> BDD-cost:    2
c ---[ 831]---> BDD-cost:    2
c ---[ 830]---> BDD-cost:    2
c ---[ 829]---> BDD-cost:    2
c ---[ 828]---> BDD-cost:    2
c ---[ 827]---> BDD-cost:    2
c ---[ 826]---> BDD-cost:    2
c ---[ 825]---> BDD-cost:    2
c ---[ 824]---> BDD-cost:    2
c ---[ 823]---> BDD-cost:    2
c ---[ 822]---> BDD-cost:    2
c ---[ 821]---> BDD-cost:    2
c ---[ 820]---> BDD-cost:    2
c ---[ 819]---> BDD-cost:    2
c ---[ 818]---> BDD-cost:    2
c ---[ 817]---> BDD-cost:    2
c ---[ 816]---> BDD-cost:    2
c ---[ 815]---> BDD-cost:    2
c ---[ 814]---> BDD-cost:    2
c ---[ 813]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 811]---> BDD-cost:    2
c ---[ 810]---> BDD-cost:    2
c ---[ 809]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    2
c ---[ 807]---> BDD-cost:    2
c ---[ 806]---> BDD-cost:    2
c ---[ 805]---> BDD-cost:    2
c ---[ 804]---> BDD-cost:    2
c ---[ 803]---> BDD-cost:    2
c ---[ 802]---> BDD-cost:    2
c ---[ 801]---> BDD-cost:    2
c ---[ 800]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 798]---> BDD-cost:    2
c ---[ 797]---> BDD-cost:    2
c ---[ 796]---> BDD-cost:    2
c ---[ 795]---> BDD-cost:    2
c ---[ 794]---> BDD-cost:    2
c ---[ 793]---> BDD-cost:    2
c ---[ 792]---> BDD-cost:    2
c ---[ 791]---> BDD-cost:    2
c ---[ 790]---> BDD-cost:    2
c ---[ 789]---> BDD-cost:    2
c ---[ 788]---> BDD-cost:    2
c ---[ 787]---> BDD-cost:    2
c ---[ 786]---> BDD-cost:    2
c ---[ 785]---> BDD-cost:    2
c ---[ 784]---> BDD-cost:    2
c ---[ 783]---> BDD-cost:    2
c ---[ 782]---> BDD-cost:    2
c ---[ 781]---> BDD-cost:    2
c ---[ 780]---> BDD-cost:    2
c ---[ 779]---> BDD-cost:    2
c ---[ 778]---> BDD-cost:    2
c ---[ 777]---> BDD-cost:    2
c ---[ 776]---> BDD-cost:    2
c ---[ 767]---> BDD-cost:    2
c ---[ 766]---> BDD-cost:    2
c ---[ 765]---> BDD-cost:    2
c ---[ 764]---> BDD-cost:    2
c ---[ 763]---> BDD-cost:    2
c ---[ 762]---> BDD-cost:    2
c ---[ 761]---> BDD-cost:    2
c ---[ 760]---> BDD-cost:    2
c ---[ 759]---> BDD-cost:    2
c ---[ 758]---> BDD-cost:    2
c ---[ 757]---> BDD-cost:    2
c ---[ 756]---> BDD-cost:    2
c ---[ 755]---> BDD-cost:    2
c ---[ 754]---> BDD-cost:    2
c ---[ 753]---> BDD-cost:    2
c ---[ 752]---> BDD-cost:    2
c ---[ 751]---> BDD-cost:    2
c ---[ 750]---> BDD-cost:    2
c ---[ 749]---> BDD-cost:    2
c ---[ 748]---> BDD-cost:    2
c ---[ 747]---> BDD-cost:    2
c ---[ 746]---> BDD-cost:    2
c ---[ 745]---> BDD-cost:    2
c ---[ 744]---> BDD-cost:    2
c ---[ 743]---> BDD-cost:    2
c ---[ 742]---> BDD-cost:    2
c ---[ 741]---> BDD-cost:    2
c ---[ 740]---> BDD-cost:    2
c ---[ 739]---> BDD-cost:    2
c ---[ 738]---> BDD-cost:    2
c ---[ 737]---> BDD-cost:    2
c ---[ 736]---> BDD-cost:    2
c ---[ 735]---> BDD-cost:    2
c ---[ 734]---> BDD-cost:    2
c ---[ 733]---> BDD-cost:    2
c ---[ 732]---> BDD-cost:    2
c ---[ 731]---> BDD-cost:    2
c ---[ 730]---> BDD-cost:    2
c ---[ 729]---> BDD-cost:    2
c ---[ 728]---> BDD-cost:    2
c ---[ 727]---> BDD-cost:    2
c ---[ 726]---> BDD-cost:    2
c ---[ 725]---> BDD-cost:    2
c ---[ 724]---> BDD-cost:    2
c ---[ 723]---> BDD-cost:    2
c ---[ 722]---> BDD-cost:    2
c ---[ 721]---> BDD-cost:    2
c ---[ 720]---> BDD-cost:    2
c ---[ 719]---> BDD-cost:    2
c ---[ 718]---> BDD-cost:    2
c ---[ 717]---> BDD-cost:    2
c ---[ 716]---> BDD-cost:    2
c ---[ 715]---> BDD-cost:    2
c ---[ 714]---> BDD-cost:    2
c ---[ 713]---> BDD-cost:    2
c ---[ 712]---> BDD-cost:    2
c ---[ 703]---> BDD-cost:    2
c ---[ 702]---> BDD-cost:    2
c ---[ 701]---> BDD-cost:    2
c ---[ 700]---> BDD-cost:    2
c ---[ 699]---> BDD-cost:    2
c ---[ 698]---> BDD-cost:    2
c ---[ 697]---> BDD-cost:    2
c ---[ 696]---> BDD-cost:    2
c ---[ 695]---> BDD-cost:    2
c ---[ 694]---> BDD-cost:    2
c ---[ 693]---> BDD-cost:    2
c ---[ 692]---> BDD-cost:    2
c ---[ 691]---> BDD-cost:    2
c ---[ 690]---> BDD-cost:    2
c ---[ 689]---> BDD-cost:    2
c ---[ 688]---> BDD-cost:    2
c ---[ 687]---> BDD-cost:    2
c ---[ 686]---> BDD-cost:    2
c ---[ 685]---> BDD-cost:    2
c ---[ 684]---> BDD-cost:    2
c ---[ 683]---> BDD-cost:    2
c ---[ 682]---> BDD-cost:    2
c ---[ 681]---> BDD-cost:    2
c ---[ 680]---> BDD-cost:    2
c ---[ 679]---> BDD-cost:    2
c ---[ 678]---> BDD-cost:    2
c ---[ 677]---> BDD-cost:    2
c ---[ 676]---> BDD-cost:    2
c ---[ 675]---> BDD-cost:    2
c ---[ 674]---> BDD-cost:    2
c ---[ 673]---> BDD-cost:    2
c ---[ 672]---> BDD-cost:    2
c ---[ 671]---> BDD-cost:    2
c ---[ 670]---> BDD-cost:    2
c ---[ 669]---> BDD-cost:    2
c ---[ 668]---> BDD-cost:    2
c ---[ 667]---> BDD-cost:    2
c ---[ 666]---> BDD-cost:    2
c ---[ 665]---> BDD-cost:    2
c ---[ 664]---> BDD-cost:    2
c ---[ 663]---> BDD-cost:    2
c ---[ 662]---> BDD-cost:    2
c ---[ 661]---> BDD-cost:    2
c ---[ 660]---> BDD-cost:    2
c ---[ 659]---> BDD-cost:    2
c ---[ 658]---> BDD-cost:    2
c ---[ 657]---> BDD-cost:    2
c ---[ 656]---> BDD-cost:    2
c ---[ 655]---> BDD-cost:    2
c ---[ 654]---> BDD-cost:    2
c ---[ 653]---> BDD-cost:    2
c ---[ 652]---> BDD-cost:    2
c ---[ 651]---> BDD-cost:    2
c ---[ 650]---> BDD-cost:    2
c ---[ 649]---> BDD-cost:    2
c ---[ 648]---> BDD-cost:    2
c ---[ 639]---> BDD-cost:    9
c ---[ 638]---> BDD-cost:    2
c ---[ 637]---> BDD-cost:    9
c ---[ 636]---> BDD-cost:    2
c ---[ 635]---> BDD-cost:    9
c ---[ 634]---> BDD-cost:    2
c ---[ 633]---> BDD-cost:    9
c ---[ 632]---> BDD-cost:    2
c ---[ 631]---> BDD-cost:    8
c ---[ 630]---> BDD-cost:    2
c ---[ 629]---> BDD-cost:    8
c ---[ 628]---> BDD-cost:    2
c ---[ 627]---> BDD-cost:    8
c ---[ 626]---> BDD-cost:    2
c ---[ 625]---> BDD-cost:    8
c ---[ 624]---> BDD-cost:    2
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    2
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    2
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    2
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    2
c ---[ 615]---> BDD-cost:    6
c ---[ 614]---> BDD-cost:    2
c ---[ 613]---> BDD-cost:    6
c ---[ 612]---> BDD-cost:    2
c ---[ 611]---> BDD-cost:    6
c ---[ 610]---> BDD-cost:    2
c ---[ 609]---> BDD-cost:    6
c ---[ 608]---> BDD-cost:    2
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:    2
c ---[ 605]---> BDD-cost:    5
c ---[ 604]---> BDD-cost:    2
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    2
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost:    2
c ---[ 599]---> BDD-cost:    4
c ---[ 598]---> BDD-cost:    2
c ---[ 597]---> BDD-cost:    4
c ---[ 596]---> BDD-cost:    2
c ---[ 595]---> BDD-cost:    4
c ---[ 594]---> BDD-cost:    2
c ---[ 593]---> BDD-cost:    4
c ---[ 592]---> BDD-cost:    2
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    2
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    2
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    2
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    2
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    2
c ---[ 573]---> BDD-cost:    2
c ---[ 572]---> BDD-cost:    2
c ---[ 571]---> BDD-cost:    2
c ---[ 570]---> BDD-cost:    2
c ---[ 569]---> BDD-cost:    2
c ---[ 568]---> BDD-cost:    2
c ---[ 567]---> BDD-cost:    5
c ---[ 566]---> BDD-cost:    2
c ---[ 565]---> BDD-cost:    2
c ---[ 564]---> BDD-cost:    2
c ---[ 563]---> BDD-cost:    2
c ---[ 562]---> BDD-cost:    2
c ---[ 561]---> BDD-cost:    2
c ---[ 560]---> BDD-cost:    2
c ---[ 559]---> BDD-cost:    4
c ---[ 558]---> BDD-cost:    2
c ---[ 557]---> BDD-cost:    2
c ---[ 556]---> BDD-cost:    2
c ---[ 555]---> BDD-cost:    2
c ---[ 554]---> BDD-cost:    2
c ---[ 553]---> BDD-cost:    2
c ---[ 552]---> BDD-cost:    2
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    2
c ---[ 549]---> BDD-cost:    2
c ---[ 548]---> BDD-cost:    2
c ---[ 547]---> BDD-cost:    2
c ---[ 546]---> BDD-cost:    2
c ---[ 545]---> BDD-cost:    2
c ---[ 544]---> BDD-cost:    2
c ---[ 543]---> BDD-cost:    2
c ---[ 542]---> BDD-cost:    2
c ---[ 541]---> BDD-cost:    2
c ---[ 540]---> BDD-cost:    2
c ---[ 539]---> BDD-cost:    2
c ---[ 538]---> BDD-cost:    2
c ---[ 537]---> BDD-cost:    2
c ---[ 536]---> BDD-cost:    2
c ---[ 535]---> BDD-cost:    4
c ---[ 534]---> BDD-cost:    2
c ---[ 533]---> BDD-cost:    2
c ---[ 532]---> BDD-cost:    2
c ---[ 531]---> BDD-cost:    2
c ---[ 530]---> BDD-cost:    2
c ---[ 529]---> BDD-cost:    2
c ---[ 528]---> BDD-cost:    2
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    2
c ---[ 525]---> BDD-cost:    2
c ---[ 524]---> BDD-cost:    2
c ---[ 523]---> BDD-cost:    2
c ---[ 522]---> BDD-cost:    2
c ---[ 521]---> BDD-cost:    2
c ---[ 520]---> BDD-cost:    2
c ---[ 511]---> BDD-cost:    2
c ---[ 510]---> BDD-cost:    2
c ---[ 509]---> BDD-cost:    2
c ---[ 508]---> BDD-cost:    2
c ---[ 507]---> BDD-cost:    2
c ---[ 506]---> BDD-cost:    2
c ---[ 505]---> BDD-cost:    2
c ---[ 504]---> BDD-cost:    2
c ---[ 503]---> BDD-cost:    2
c ---[ 502]---> BDD-cost:    2
c ---[ 501]---> BDD-cost:    2
c ---[ 500]---> BDD-cost:    2
c ---[ 499]---> BDD-cost:    2
c ---[ 498]---> BDD-cost:    2
c ---[ 497]---> BDD-cost:    2
c ---[ 496]---> BDD-cost:    2
c ---[ 495]---> BDD-cost:    2
c ---[ 494]---> BDD-cost:    2
c ---[ 493]---> BDD-cost:    2
c ---[ 492]---> BDD-cost:    2
c ---[ 491]---> BDD-cost:    2
c ---[ 490]---> BDD-cost:    2
c ---[ 489]---> BDD-cost:    2
c ---[ 488]---> BDD-cost:    2
c ---[ 487]---> BDD-cost:    2
c ---[ 486]---> BDD-cost:    2
c ---[ 485]---> BDD-cost:    2
c ---[ 484]---> BDD-cost:    2
c ---[ 483]---> BDD-cost:    2
c ---[ 482]---> BDD-cost:    2
c ---[ 481]---> BDD-cost:    2
c ---[ 480]---> BDD-cost:    2
c ---[ 479]---> BDD-cost:    2
c ---[ 478]---> BDD-cost:    2
c ---[ 477]---> BDD-cost:    2
c ---[ 476]---> BDD-cost:    2
c ---[ 475]---> BDD-cost:    2
c ---[ 474]---> BDD-cost:    2
c ---[ 473]---> BDD-cost:    2
c ---[ 472]---> BDD-cost:    2
c ---[ 471]---> BDD-cost:    2
c ---[ 470]---> BDD-cost:    2
c ---[ 469]---> BDD-cost:    2
c ---[ 468]---> BDD-cost:    2
c ---[ 467]---> BDD-cost:    2
c ---[ 466]---> BDD-cost:    2
c ---[ 465]---> BDD-cost:    2
c ---[ 464]---> BDD-cost:    2
c ---[ 463]---> BDD-cost:    2
c ---[ 462]---> BDD-cost:    2
c ---[ 461]---> BDD-cost:    2
c ---[ 460]---> BDD-cost:    2
c ---[ 459]---> BDD-cost:    2
c ---[ 458]---> BDD-cost:    2
c ---[ 457]---> BDD-cost:    2
c ---[ 456]---> BDD-cost:    2
c ---[ 447]---> BDD-cost:    2
c ---[ 446]---> BDD-cost:    2
c ---[ 445]---> BDD-cost:    2
c ---[ 444]---> BDD-cost:    2
c ---[ 443]---> BDD-cost:    2
c ---[ 442]---> BDD-cost:    2
c ---[ 441]---> BDD-cost:    2
c ---[ 440]---> BDD-cost:    2
c ---[ 439]---> BDD-cost:    2
c ---[ 438]---> BDD-cost:    2
c ---[ 437]---> BDD-cost:    2
c ---[ 436]---> BDD-cost:    2
c ---[ 435]---> BDD-cost:    2
c ---[ 434]---> BDD-cost:    2
c ---[ 433]---> BDD-cost:    2
c ---[ 432]---> BDD-cost:    2
c ---[ 431]---> BDD-cost:    2
c ---[ 430]---> BDD-cost:    2
c ---[ 429]---> BDD-cost:    2
c ---[ 428]---> BDD-cost:    2
c ---[ 427]---> BDD-cost:    2
c ---[ 426]---> BDD-cost:    2
c ---[ 425]---> BDD-cost:    2
c ---[ 424]---> BDD-cost:    2
c ---[ 423]---> BDD-cost:    2
c ---[ 422]---> BDD-cost:    2
c ---[ 421]---> BDD-cost:    2
c ---[ 420]---> BDD-cost:    2
c ---[ 419]---> BDD-cost:    2
c ---[ 418]---> BDD-cost:    2
c ---[ 417]---> BDD-cost:    2
c ---[ 416]---> BDD-cost:    2
c ---[ 415]---> BDD-cost:    2
c ---[ 414]---> BDD-cost:    2
c ---[ 413]---> BDD-cost:    2
c ---[ 412]---> BDD-cost:    2
c ---[ 411]---> BDD-cost:    2
c ---[ 410]---> BDD-cost:    2
c ---[ 409]---> BDD-cost:    2
c ---[ 408]---> BDD-cost:    2
c ---[ 407]---> BDD-cost:    2
c ---[ 406]---> BDD-cost:    2
c ---[ 405]---> BDD-cost:    2
c ---[ 404]---> BDD-cost:    2
c ---[ 403]---> BDD-cost:    2
c ---[ 402]---> BDD-cost:    2
c ---[ 401]---> BDD-cost:    2
c ---[ 400]---> BDD-cost:    2
c ---[ 399]---> BDD-cost:    2
c ---[ 398]---> BDD-cost:    2
c ---[ 397]---> BDD-cost:    2
c ---[ 396]---> BDD-cost:    2
c ---[ 395]---> BDD-cost:    2
c ---[ 394]---> BDD-cost:    2
c ---[ 393]---> BDD-cost:    2
c ---[ 392]---> BDD-cost:    2
c ---[ 383]---> BDD-cost:    2
c ---[ 382]---> BDD-cost:    2
c ---[ 381]---> BDD-cost:    2
c ---[ 380]---> BDD-cost:    2
c ---[ 379]---> BDD-cost:    2
c ---[ 378]---> BDD-cost:    2
c ---[ 377]---> BDD-cost:    2
c ---[ 376]---> BDD-cost:    2
c ---[ 375]---> BDD-cost:    2
c ---[ 374]---> BDD-cost:    2
c ---[ 373]---> BDD-cost:    2
c ---[ 372]---> BDD-cost:    2
c ---[ 371]---> BDD-cost:    2
c ---[ 370]---> BDD-cost:    2
c ---[ 369]---> BDD-cost:    2
c ---[ 368]---> BDD-cost:    2
c ---[ 367]---> BDD-cost:    2
c ---[ 366]---> BDD-cost:    2
c ---[ 365]---> BDD-cost:    2
c ---[ 364]---> BDD-cost:    2
c ---[ 363]---> BDD-cost:    2
c ---[ 362]---> BDD-cost:    2
c ---[ 361]---> BDD-cost:    2
c ---[ 360]---> BDD-cost:    2
c ---[ 359]---> BDD-cost:    2
c ---[ 358]---> BDD-cost:    2
c ---[ 357]---> BDD-cost:    2
c ---[ 356]---> BDD-cost:    2
c ---[ 355]---> BDD-cost:    2
c ---[ 354]---> BDD-cost:    2
c ---[ 353]---> BDD-cost:    2
c ---[ 352]---> BDD-cost:    2
c ---[ 351]---> BDD-cost:    2
c ---[ 350]---> BDD-cost:    2
c ---[ 349]---> BDD-cost:    2
c ---[ 348]---> BDD-cost:    2
c ---[ 347]---> BDD-cost:    2
c ---[ 346]---> BDD-cost:    2
c ---[ 345]---> BDD-cost:    2
c ---[ 344]---> BDD-cost:    2
c ---[ 343]---> BDD-cost:    2
c ---[ 342]---> BDD-cost:    2
c ---[ 341]---> BDD-cost:    2
c ---[ 340]---> BDD-cost:    2
c ---[ 339]---> BDD-cost:    2
c ---[ 338]---> BDD-cost:    2
c ---[ 337]---> BDD-cost:    2
c ---[ 336]---> BDD-cost:    2
c ---[ 335]---> BDD-cost:    2
c ---[ 334]---> BDD-cost:    2
c ---[ 333]---> BDD-cost:    2
c ---[ 332]---> BDD-cost:    2
c ---[ 331]---> BDD-cost:    2
c ---[ 330]---> BDD-cost:    2
c ---[ 329]---> BDD-cost:    2
c ---[ 328]---> BDD-cost:    2
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    2
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    2
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    2
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    2
c ---[ 311]---> BDD-cost:    8
c ---[ 310]---> BDD-cost:    2
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    2
c ---[ 307]---> BDD-cost:    8
c ---[ 306]---> BDD-cost:    2
c ---[ 305]---> BDD-cost:    8
c ---[ 304]---> BDD-cost:    2
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    2
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    2
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    2
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    2
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    2
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    2
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    2
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    2
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:    2
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:    2
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    2
c ---[ 281]---> BDD-cost:    5
c ---[ 280]---> BDD-cost:    2
c ---[ 279]---> BDD-cost:    4
c ---[ 278]---> BDD-cost:    2
c ---[ 277]---> BDD-cost:    4
c ---[ 276]---> BDD-cost:    2
c ---[ 275]---> BDD-cost:    4
c ---[ 274]---> BDD-cost:    2
c ---[ 273]---> BDD-cost:    4
c ---[ 272]---> BDD-cost:    2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    2
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    2
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    2
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    2
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    2
c ---[ 253]---> BDD-cost:    2
c ---[ 252]---> BDD-cost:    2
c ---[ 251]---> BDD-cost:    2
c ---[ 250]---> BDD-cost:    2
c ---[ 249]---> BDD-cost:    2
c ---[ 248]---> BDD-cost:    2
c ---[ 247]---> BDD-cost:    5
c ---[ 246]---> BDD-cost:    2
c ---[ 245]---> BDD-cost:    2
c ---[ 244]---> BDD-cost:    2
c ---[ 243]---> BDD-cost:    2
c ---[ 242]---> BDD-cost:    2
c ---[ 241]---> BDD-cost:    2
c ---[ 240]---> BDD-cost:    2
c ---[ 239]---> BDD-cost:    4
c ---[ 238]---> BDD-cost:    2
c ---[ 237]---> BDD-cost:    2
c ---[ 236]---> BDD-cost:    2
c ---[ 235]---> BDD-cost:    2
c ---[ 234]---> BDD-cost:    2
c ---[ 233]---> BDD-cost:    2
c ---[ 232]---> BDD-cost:    2
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    2
c ---[ 229]---> BDD-cost:    2
c ---[ 228]---> BDD-cost:    2
c ---[ 227]---> BDD-cost:    2
c ---[ 226]---> BDD-cost:    2
c ---[ 225]---> BDD-cost:    2
c ---[ 224]---> BDD-cost:    2
c ---[ 223]---> BDD-cost:    2
c ---[ 222]---> BDD-cost:    2
c ---[ 221]---> BDD-cost:    2
c ---[ 220]---> BDD-cost:    2
c ---[ 219]---> BDD-cost:    2
c ---[ 218]---> BDD-cost:    2
c ---[ 217]---> BDD-cost:    2
c ---[ 216]---> BDD-cost:    2
c ---[ 215]---> BDD-cost:    4
c ---[ 214]---> BDD-cost:    2
c ---[ 213]---> BDD-cost:    2
c ---[ 212]---> BDD-cost:    2
c ---[ 211]---> BDD-cost:    2
c ---[ 210]---> BDD-cost:    2
c ---[ 209]---> BDD-cost:    2
c ---[ 208]---> BDD-cost:    2
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    2
c ---[ 205]---> BDD-cost:    2
c ---[ 204]---> BDD-cost:    2
c ---[ 203]---> BDD-cost:    2
c ---[ 202]---> BDD-cost:    2
c ---[ 201]---> BDD-cost:    2
c ---[ 200]---> BDD-cost:    2
c ---[ 191]---> BDD-cost:    2
c ---[ 190]---> BDD-cost:    2
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 181]---> BDD-cost:    2
c ---[ 180]---> BDD-cost:    2
c ---[ 179]---> BDD-cost:    2
c ---[ 178]---> BDD-cost:    2
c ---[ 177]---> BDD-cost:    2
c ---[ 176]---> BDD-cost:    2
c ---[ 175]---> BDD-cost:    2
c ---[ 174]---> BDD-cost:    2
c ---[ 173]---> BDD-cost:    2
c ---[ 172]---> BDD-cost:    2
c ---[ 171]---> BDD-cost:    2
c ---[ 170]---> BDD-cost:    2
c ---[ 169]---> BDD-cost:    2
c ---[ 168]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 166]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 164]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 162]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    2
c ---[ 159]---> BDD-cost:    2
c ---[ 158]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    2
c ---[ 156]---> BDD-cost:    2
c ---[ 155]---> BDD-cost:    2
c ---[ 154]---> BDD-cost:    2
c ---[ 153]---> BDD-cost:    2
c ---[ 152]---> BDD-cost:    2
c ---[ 151]---> BDD-cost:    2
c ---[ 150]---> BDD-cost:    2
c ---[ 149]---> BDD-cost:    2
c ---[ 148]---> BDD-cost:    2
c ---[ 147]---> BDD-cost:    2
c ---[ 146]---> BDD-cost:    2
c ---[ 145]---> BDD-cost:    2
c ---[ 144]---> BDD-cost:    2
c ---[ 143]---> BDD-cost:    2
c ---[ 142]---> BDD-cost:    2
c ---[ 141]---> BDD-cost:    2
c ---[ 140]---> BDD-cost:    2
c ---[ 139]---> BDD-cost:    2
c ---[ 138]---> BDD-cost:    2
c ---[ 137]---> BDD-cost:    2
c ---[ 136]---> BDD-cost:    2
c ---[ 127]---> BDD-cost:    2
c ---[ 126]---> BDD-cost:    2
c ---[ 125]---> BDD-cost:    2
c ---[ 124]---> BDD-cost:    2
c ---[ 123]---> BDD-cost:    2
c ---[ 122]---> BDD-cost:    2
c ---[ 121]---> BDD-cost:    2
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 118]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 116]---> BDD-cost:    2
c ---[ 115]---> BDD-cost:    2
c ---[ 114]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 111]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 109]---> BDD-cost:    2
c ---[ 108]---> BDD-cost:    2
c ---[ 107]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 104]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[ 102]---> BDD-cost:    2
c ---[ 101]---> BDD-cost:    2
c ---[ 100]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  94]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  88]---> BDD-cost:    2
c ---[  87]---> BDD-cost:    2
c ---[  86]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  83]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  81]---> BDD-cost:    2
c ---[  80]---> BDD-cost:    2
c ---[  79]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  76]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  74]---> BDD-cost:    2
c ---[  73]---> BDD-cost:    2
c ---[  72]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  62]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  60]---> BDD-cost:    2
c ---[  59]---> BDD-cost:    2
c ---[  58]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  55]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  53]---> BDD-cost:    2
c ---[  52]---> BDD-cost:    2
c ---[  51]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  48]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  46]---> BDD-cost:    2
c ---[  45]---> BDD-cost:    2
c ---[  44]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  41]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  39]---> BDD-cost:    2
c ---[  38]---> BDD-cost:    2
c ---[  37]---> BDD-cost:    2
c ---[  36]---> BDD-cost:    2
c ---[  35]---> BDD-cost:    2
c ---[  34]---> BDD-cost:    2
c ---[  33]---> BDD-cost:    2
c ---[  32]---> BDD-cost:    2
c ---[  31]---> BDD-cost:    2
c ---[  30]---> BDD-cost:    2
c ---[  29]---> BDD-cost:    2
c ---[  28]---> BDD-cost:    2
c ---[  27]---> BDD-cost:    2
c ---[  26]---> BDD-cost:    2
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost:    2
c ---[  23]---> BDD-cost:    2
c ---[  22]---> BDD-cost:    2
c ---[  21]---> BDD-cost:    2
c ---[  20]---> BDD-cost:    2
c ---[  19]---> BDD-cost:    2
c ---[  18]---> BDD-cost:    2
c ---[  17]---> BDD-cost:    2
c ---[  16]---> BDD-cost:    2
c ---[  15]---> BDD-cost:    2
c ---[  14]---> BDD-cost:    2
c ---[  13]---> BDD-cost:    2
c ---[  12]---> BDD-cost:    2
c ---[  11]---> BDD-cost:    2
c ---[  10]---> BDD-cost:    2
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   17376    49254 |    5212       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5250          
c   -- var.elim.:  2000/5250          
c   -- var.elim.:  3000/5250          
c   -- var.elim.:  4000/5250          
c   -- var.elim.:  5000/5250          
c   -- var.elim.:  5250/5250          
c   -- var.elim.:  1000/1626          
c   -- var.elim.:  1626/1626          
c   -- subsuming                       
c   -- var.elim.:  1000/1249          
c   -- var.elim.:  1249/1249          
c   -- var.elim.:  1000/1110          
c   -- var.elim.:  1110/1110          
c   -- subsuming                       
c   -- var.elim.:  601/601          
c |         0 |   15960    43686 |      --       0       --      -- |     --   | -1416/-3096
c |         0 |   15960    43686 |    6384       0        0     nan |  0.000 % |
c |       101 |   15960    43686 |    7022     101     2080    20.6 | 32.207 % |
c ==============================================================================
c (current CPU-time: 0.894863 s)
c ==============================================================================
c [1mFound solution: 33397[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       156 |  111058   265905 |   33317     156     3869    24.8 | 32.207 % |
c   -- subsuming                       
c   -- var.elim.:  1000/33236          
c   -- var.elim.:  2000/33236          
c   -- var.elim.:  3000/33236          
c   -- var.elim.:  4000/33236          
c   -- var.elim.:  5000/33236          
c   -- var.elim.:  6000/33236          
c   -- var.elim.:  7000/33236          
c   -- var.elim.:  8000/33236          
c   -- var.elim.:  9000/33236          
c   -- var.elim.:  10000/33236          
c   -- var.elim.:  11000/33236          
c   -- var.elim.:  12000/33236          
c   -- var.elim.:  13000/33236          
c   -- var.elim.:  14000/33236          
c   -- var.elim.:  15000/33236          
c   -- var.elim.:  16000/33236          
c   -- var.elim.:  17000/33236          
c   -- var.elim.:  18000/33236          
c   -- var.elim.:  19000/33236          
c   -- var.elim.:  20000/33236          
c   -- var.elim.:  21000/33236          
c   -- var.elim.:  22000/33236          
c   -- var.elim.:  23000/33236          
c   -- var.elim.:  24000/33236          
c   -- var.elim.:  25000/33236          
c   -- var.elim.:  26000/33236          
c   -- var.elim.:  27000/33236          
c   -- var.elim.:  28000/33236          
c   -- var.elim.:  29000/33236          
c   -- var.elim.:  30000/33236          
c   -- var.elim.:  31000/33236          
c   -- var.elim.:  32000/33236          
c   -- var.elim.:  33000/33236          
c   -- var.elim.:  33236/33236          
c   -- var.elim.:  1000/18060          
c   -- var.elim.:  2000/18060          
c   -- var.elim.:  3000/18060          
c   -- var.elim.:  4000/18060          
c   -- var.elim.:  5000/18060          
c   -- var.elim.:  6000/18060          
c   -- var.elim.:  7000/18060          
c   -- var.elim.:  8000/18060          
c   -- var.elim.:  9000/18060          
c   -- var.elim.:  10000/18060          
c   -- var.elim.:  11000/18060          
c   -- var.elim.:  12000/18060          
c   -- var.elim.:  13000/18060          
c   -- var.elim.:  14000/18060          
c   -- var.elim.:  15000/18060          
c   -- var.elim.:  16000/18060          
c   -- var.elim.:  17000/18060          
c   -- var.elim.:  18000/18060          
c   -- var.elim.:  18060/18060          
c   -- var.elim.:  150/150          
c   -- subsuming                       
c   -- var.elim.:  1000/1500          
c   -- var.elim.:  1500/1500          
c   -- var.elim.:  236/236          
c   -- subsuming                       
c   -- var.elim.:  42/42          
c   -- var.elim.:  23/23          
c |       156 |  101738   311999 |      --     156       --      -- |     --   | -9320/46095
c |       156 |  101738   311999 |   40695     156     3869    24.8 | 32.207 % |
c |       256 |  101738   311999 |   44764     256     5177    20.2 |  8.100 % |
c ==============================================================================
c (current CPU-time: 7.01193 s)
c ==============================================================================
c [1mFound solution: 31043[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       265 |  103876   317659 |   31162     265     5283    19.9 |  8.100 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3096          
c   -- var.elim.:  2000/3096          
c   -- var.elim.:  3000/3096          
c   -- var.elim.:  3096/3096          
c   -- var.elim.:  1000/1720          
c   -- var.elim.:  1720/1720          
c   -- subsuming                       
c   -- var.elim.:  183/183          
c |       265 |  102700   318173 |      --     265       --      -- |     --   | -1176/515
c |       265 |  102700   318173 |   41080     265     5283    19.9 |  8.100 % |
c ==============================================================================
c (current CPU-time: 8.28674 s)
c ==============================================================================
c [1mFound solution: 30496[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       343 |  103116   319518 |   30934     343     6690    19.5 |  8.100 % |
c   -- subsuming                       
c   -- var.elim.:  871/871          
c   -- var.elim.:  596/596          
c   -- subsuming                       
c |       343 |  102885   320130 |      --     343       --      -- |     --   | -231/613
c |       343 |  102885   320130 |   41154     343     6690    19.5 |  8.100 % |
c ==============================================================================
c (current CPU-time: 9.2266 s)
c ==============================================================================
c [1mFound solution: 29630[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       381 |  103800   322714 |   31139     381     8126    21.3 |  8.100 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1477          
c   -- var.elim.:  1477/1477          
c   -- var.elim.:  855/855          
c   -- subsuming                       
c   -- var.elim.:  243/243          
c |       381 |  103311   323036 |      --     381       --      -- |     --   | -489/323
c |       381 |  103311   323036 |   41324     381     8126    21.3 |  8.100 % |
c ==============================================================================
c (current CPU-time: 10.4854 s)
c ==============================================================================
c [1mFound solution: 29580[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       445 |  103385   323613 |   31015     445    12643    28.4 |  8.100 % |
c   -- subsuming                       
c   -- var.elim.:  499/499          
c   -- var.elim.:  448/448          
c |       445 |  103340   324185 |      --     445       --      -- |     --   | -45/573
c |       445 |  103340   324185 |   41336     445    12643    28.4 |  8.100 % |
c ==============================================================================
c (current CPU-time: 11.3193 s)
c ==============================================================================
c [1mFound solution: 28933[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       468 |  103400   324759 |   31019     468    13166    28.1 |  8.100 % |
c   -- subsuming                       
c   -- var.elim.:  510/510          
c   -- var.elim.:  466/466          
c |       468 |  103361   325359 |      --     468       --      -- |     --   | -39/601
c |       468 |  103361   325359 |   41344     468    13166    28.1 |  8.100 % |
c ==============================================================================
c (current CPU-time: 12.3361 s)
c ==============================================================================
c [1mFound solution: 28166[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       533 |  104265   327936 |   31279     533    16071    30.2 |  8.100 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1610          
c   -- var.elim.:  1610/1610          
c   -- var.elim.:  908/908          
c   -- subsuming                       
c   -- var.elim.:  315/315          
c |       533 |  103763   328366 |      --     533       --      -- |     --   | -502/431
c |       533 |  103763   328366 |   41505     533    16071    30.2 |  8.100 % |
c |       634 |  103763   328366 |   45655     634    22883    36.1 |  7.967 % |
c ==============================================================================
c (current CPU-time: 14.9777 s)
c ==============================================================================
c [1mFound solution: 28077[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       751 |  103819   328921 |   31145     751    49908    66.5 |  7.967 % |
c   -- subsuming                       
c   -- var.elim.:  497/497          
c   -- var.elim.:  455/455          
c |       751 |  103784   331140 |      --     751       --      -- |     --   | -35/2220
c |       751 |  103784   331140 |   41513     751    49908    66.5 |  7.967 % |
c |       851 |  103784   331140 |   45664     851    54242    63.7 |  7.971 % |
c |      1001 |  103784   331140 |   50231    1001    70924    70.9 |  7.971 % |
c |      1226 |  103784   331140 |   55254    1226    94923    77.4 |  7.971 % |
c |      1563 |  103663   330051 |   60709    1560   105467    67.6 |  8.020 % |
c |      2069 |  103507   326810 |   66679    2062   118917    57.7 |  8.098 % |
c |      2828 |  102946   323855 |   72950    2801   167160    59.7 |  8.400 % |
c |      3968 |  102946   323855 |   80245    3941   586906   148.9 |  8.400 % |
c |      5677 |  102305   319442 |   87719    5418   713201   131.6 |  8.706 % |
c |      8239 |  102305   319442 |   96491    7980  1133395   142.0 |  8.706 % |
c ==============================================================================
c (current CPU-time: 53.8778 s)
c ==============================================================================
c [1mFound solution: 27912[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9109 |  102358   319972 |   30707    8850  1404612   158.7 |  8.706 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1712          
c   -- var.elim.:  1712/1712          
c   -- var.elim.:  1000/1459          
c   -- var.elim.:  1459/1459          
c   -- var.elim.:  783/783          
c   -- var.elim.:  191/191          
c   -- subsuming                       
c   -- var.elim.:  340/340          
c   -- var.elim.:  15/15          
c |      9109 |  102008   321184 |      --    8850       --      -- |     --   | -346/1221
c |      9109 |  102008   321184 |   40803    7455   280565    37.6 |  8.706 % |
c |      9209 |  102008   321184 |   44883    7555   283597    37.5 |  8.820 % |
c |      9359 |  101763   320279 |   49253    7699   285941    37.1 |  8.935 % |
c |      9584 |  101649   319836 |   54117    7923   322929    40.8 |  9.005 % |
c |      9921 |  101649   319836 |   59529    8260   338506    41.0 |  9.005 % |
c |     10427 |  101649   319836 |   65482    8766   351166    40.1 |  9.005 % |
c |     11187 |  101516   318721 |   71936    9514   370496    38.9 |  9.071 % |
c |     12326 |  101516   318721 |   79130   10653   440895    41.4 |  9.071 % |
c |     14035 |  101480   318593 |   87012   12361   825540    66.8 |  9.088 % |
c |     16597 |  101480   318593 |   95713   14923  1159651    77.7 |  9.088 % |
c ==============================================================================
c (current CPU-time: 120.796 s)
c ==============================================================================
c [1mFound solution: 27680[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19258 |  101591   319251 |   30477   17584  2234954   127.1 |  9.088 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1266          
c   -- var.elim.:  1266/1266          
c   -- var.elim.:  949/949          
c   -- var.elim.:  38/38          
c   -- var.elim.:  194/194          
c   -- subsuming                       
c   -- var.elim.:  15/15          
c   -- var.elim.:  16/16          
c |     19258 |  101447   320433 |      --   17584       --      -- |     --   | -143/1185
c |     19258 |  101447   320433 |   40578   16651  1134210    68.1 |  9.088 % |
c |     19358 |  101381   319211 |   44607   16749  1135318    67.8 |  9.134 % |
c |     19508 |  101381   319211 |   49068   16899  1137079    67.3 |  9.134 % |
c |     19733 |  101381   319211 |   53975   17124  1156373    67.5 |  9.134 % |
c |     20070 |  101205   318584 |   59269   17457  1167186    66.9 |  9.216 % |
c |     20578 |  101128   318331 |   65147   17962  1239485    69.0 |  9.257 % |
c ==============================================================================
c (current CPU-time: 127.64 s)
c ==============================================================================
c [1mFound solution: 27449[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20844 |  101459   319373 |   30437   18226  1249894    68.6 |  9.257 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1729          
c   -- var.elim.:  1729/1729          
c   -- var.elim.:  1000/1325          
c   -- var.elim.:  1325/1325          
c   -- var.elim.:  61/61          
c   -- var.elim.:  163/163          
c   -- subsuming                       
c   -- var.elim.:  37/37          
c   -- var.elim.:  16/16          
c |     20844 |  101045   320320 |      --   18226       --      -- |     --   | -412/952
c |     20844 |  101045   320320 |   40418   18226  1249894    68.6 |  9.257 % |
c |     20946 |  101045   320320 |   44459   18328  1258709    68.7 |  9.345 % |
c |     21096 |  101045   320320 |   48905   18478  1313591    71.1 |  9.345 % |
c |     21322 |  101045   320320 |   53796   18704  1321139    70.6 |  9.345 % |
c |     21659 |  101045   320320 |   59175   19041  1378440    72.4 |  9.345 % |
c |     22166 |  101045   320320 |   65093   19548  1457406    74.6 |  9.345 % |
c ==============================================================================
c (current CPU-time: 142.559 s)
c ==============================================================================
c [1mFound solution: 27353[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     22489 |  101128   321049 |   30338   19871  1590314    80.0 |  9.345 % |
c   -- subsuming                       
c   -- var.elim.:  628/628          
c   -- var.elim.:  589/589          
c   -- var.elim.:  374/374          
c |     22489 |  101059   321618 |      --   19871       --      -- |     --   | -66/576
c |     22489 |  101059   321618 |   40423   19464  1203145    61.8 |  9.345 % |
c |     22589 |  100915   319093 |   44402   19563  1205823    61.6 |  9.428 % |
c |     22741 |  100915   319093 |   48842   19715  1207664    61.3 |  9.428 % |
c |     22967 |  100542   317555 |   53528   19936  1210744    60.7 |  9.596 % |
c |     23304 |  100542   317555 |   58881   20273  1313331    64.8 |  9.596 % |
c |     23811 |  100542   317555 |   64769   20780  1404641    67.6 |  9.596 % |
c |     24572 |  100542   317555 |   71246   21541  1671017    77.6 |  9.596 % |
c |     25711 |  100542   317555 |   78371   22680  1842930    81.3 |  9.596 % |
c |     27419 |  100037   315345 |   85775   24369  2096852    86.0 |  9.843 % |
c |     29983 |  100037   315345 |   94352   26933  3260193   121.0 |  9.843 % |
c ==============================================================================
c (current CPU-time: 200.396 s)
c ==============================================================================
c [1mFound solution: 26245[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     32422 |   99896   314776 |   29968   29338  3932595   134.0 |  9.843 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1794          
c   -- var.elim.:  1794/1794          
c   -- var.elim.:  1000/1522          
c   -- var.elim.:  1522/1522          
c   -- var.elim.:  19/19          
c   -- subsuming                       
c   -- var.elim.:  457/457          
c   -- var.elim.:  203/203          
c |     32422 |   99746   315647 |      --   29338       --      -- |     --   | -150/872
c |     32422 |   99746   315647 |   39898   26473  1365468    51.6 |  9.843 % |
c |     32523 |   99746   315647 |   43888   26574  1389872    52.3 |  9.967 % |
c |     32674 |   99746   315647 |   48277   26725  1458965    54.6 |  9.967 % |
c |     32904 |   99746   315647 |   53104   26955  1463886    54.3 |  9.967 % |
c |     33245 |   99746   315647 |   58415   27296  1471199    53.9 |  9.967 % |
c ==============================================================================
c (current CPU-time: 207.182 s)
c ==============================================================================
c [1mFound solution: 26100[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     33295 |   99853   316328 |   29955   27346  1475760    54.0 |  9.967 % |
c   -- subsuming                       
c   -- var.elim.:  553/553          
c   -- var.elim.:  500/500          
c   -- var.elim.:  295/295          
c   -- var.elim.:  364/364          
c |     33295 |   99753   316281 |      --   27346       --      -- |     --   | -97/-40
c |     33295 |   99753   316281 |   39901   27346  1475760    54.0 |  9.967 % |
c |     33396 |   99753   316281 |   43891   27447  1480798    54.0 |  9.974 % |
c |     33546 |   99753   316281 |   48280   27597  1495900    54.2 |  9.974 % |
c |     33771 |   99753   316281 |   53108   27822  1592567    57.2 |  9.974 % |
c |     34111 |   99753   316281 |   58419   28162  1696928    60.3 |  9.974 % |
c |     34618 |   99554   315566 |   64133   28639  1727583    60.3 | 10.090 % |
c |     35377 |   99370   314878 |   70416   29390  1769745    60.2 | 10.173 % |
c |     36516 |   99216   314322 |   77337   30525  1974583    64.7 | 10.251 % |
c |     38225 |   98955   313346 |   84847   32179  2113038    65.7 | 10.412 % |
c |     40787 |   98955   313346 |   93332   34741  2467515    71.0 | 10.412 % |
c |     44633 |   98666   312112 |  102365   38578  3385167    87.7 | 10.565 % |
c |     50399 |   97914   309471 |  111744   44317  4959287   111.9 | 10.970 % |
c |     59048 |   97672   308599 |  122614   52947  6577245   124.2 | 11.114 % |
c |     72023 |   95510   299643 |  131890   65646 10822464   164.9 | 12.407 % |
c |     91485 |   95510   299643 |  145079   85108 18504345   217.4 | 12.407 % |
c |    120677 |   94697   296700 |  158229  113957 31334082   275.0 | 12.927 % |
c ==============================================================================
c (current CPU-time: 996.925 s)
c ==============================================================================
c [1mFound solution: 25808[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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    128708 |   93864   294165 |   28159  121784 34335583   281.9 | 12.927 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4070          
c   -- var.elim.:  2000/4070          
c   -- var.elim.:  3000/4070          
c   -- var.elim.:  4000/4070          
c   -- var.elim.:  4070/4070          
c   -- var.elim.:  1000/2886          
c   -- var.elim.:  2000/2886          
c   -- var.elim.:  2886/2886          
c   -- var.elim.:  955/955          
c   -- var.elim.:  944/944          
c   -- var.elim.:  242/242          
c   -- subsuming                       
c   -- var.elim.:  840/840          
c   -- var.elim.:  54/54          
c |    128708 |   93122   292607 |      --  121784       --      -- |     --   | -738/-1549
c |    128708 |   93122   292607 |   37248   84720  3842354    45.4 | 12.927 % |
c |    128809 |   93122   292607 |   40973   15511   457572    29.5 | 13.766 % |
c |    128959 |   93122   292607 |   45071   15661   474256    30.3 | 13.766 % |
c |    129184 |   93122   292607 |   49578   15886   545117    34.3 | 13.766 % |
c |    129521 |   93056   292381 |   54497   16222   650095    40.1 | 13.808 % |
c |    130027 |   92772   291404 |   59764   16726   669643    40.0 | 13.951 % |
c |    130786 |   92460   290309 |   65519   17484   954538    54.6 | 14.131 % |
c |    131926 |   9#### 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 27028
Raw data (stat): 27028 (runsolver) R 27027 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422146230 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99996 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 11608 0 0 0 944 41 0 0 25 0 1 0 422146230 37007360 7466 4294967295 134512640 134672761 3221224576 3221222840 1075730078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9035 7466 603 41 0 8994 0
vsize: 36140
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 17912 0 0 0 1920 64 0 0 25 0 1 0 422146230 30130176 6266 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7356 6266 603 41 0 7315 0
vsize: 29424
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 18407 0 0 0 2918 66 0 0 25 0 1 0 422146230 32268288 6761 4294967295 134512640 134672761 3221224576 3221223760 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7878 6761 603 41 0 7837 0
vsize: 31512
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 18671 0 0 0 3917 67 0 0 25 0 1 0 422146230 33304576 7025 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8131 7025 603 41 0 8090 0
vsize: 32524
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 18965 0 0 0 4916 67 0 0 25 0 1 0 422146230 34476032 7319 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8417 7319 603 41 0 8376 0
vsize: 33668
[startup+60.0015 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 21104 0 0 0 5910 74 0 0 25 0 1 0 422146230 35540992 7580 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8677 7580 603 41 0 8636 0
vsize: 34708
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 21106 0 0 0 6910 74 0 0 25 0 1 0 422146230 35540992 7582 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8677 7582 603 41 0 8636 0
vsize: 34708
[startup+80.0027 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 21107 0 0 0 7910 74 0 0 25 0 1 0 422146230 35540992 7583 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8677 7583 603 41 0 8636 0
vsize: 34708
[startup+90.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 21109 0 0 0 8910 74 0 0 25 0 1 0 422146230 35540992 7585 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8677 7585 603 41 0 8636 0
vsize: 34708
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 21111 0 0 0 9910 74 0 0 25 0 1 0 422146230 35540992 7587 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8677 7587 603 41 0 8636 0
vsize: 34708
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 21443 0 0 0 10909 75 0 0 25 0 1 0 422146230 36990976 7919 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9031 7919 603 41 0 8990 0
vsize: 36124
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 21896 0 0 0 11908 76 0 0 25 0 1 0 422146230 38842368 8372 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9483 8372 603 41 0 9442 0
vsize: 37932
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 25601 0 0 0 12897 87 0 0 25 0 1 0 422146230 39497728 8548 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9643 8548 603 41 0 9602 0
vsize: 38572
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 25602 0 0 0 13896 87 0 0 25 0 1 0 422146230 39497728 8549 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9643 8549 603 41 0 9602 0
vsize: 38572
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 27030 0 0 0 14888 94 0 0 25 0 1 0 422146230 39497728 8550 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8550 603 41 0 9602 0
vsize: 38572
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 27031 0 0 0 15888 94 0 0 25 0 1 0 422146230 39497728 8551 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8551 603 41 0 9602 0
vsize: 38572
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 27033 0 0 0 16889 94 0 0 25 0 1 0 422146230 39497728 8553 4294967295 134512640 134672761 3221224576 3221223728 134614555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8553 603 41 0 9602 0
vsize: 38572
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 27132 0 0 0 17889 94 0 0 25 0 1 0 422146230 40017920 8652 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9770 8652 603 41 0 9729 0
vsize: 39080
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 28113 0 0 0 18886 97 0 0 25 0 1 0 422146230 43966464 9633 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10734 9633 603 41 0 10693 0
vsize: 42936
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 28721 0 0 0 19884 99 0 0 25 0 1 0 422146230 46460928 10241 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11343 10241 603 41 0 11302 0
vsize: 45372
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32101 0 0 0 20870 112 0 0 25 0 1 0 422146230 46616576 10305 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11381 10305 603 41 0 11340 0
vsize: 45524
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32101 0 0 0 21869 113 0 0 25 0 1 0 422146230 46616576 10305 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11381 10305 603 41 0 11340 0
vsize: 45524
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32103 0 0 0 22869 113 0 0 25 0 1 0 422146230 46616576 10307 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11381 10307 603 41 0 11340 0
vsize: 45524
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32137 0 0 0 23869 113 0 0 25 0 1 0 422146230 46878720 10341 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11445 10341 603 41 0 11404 0
vsize: 45780
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32139 0 0 0 24870 113 0 0 25 0 1 0 422146230 46878720 10343 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11445 10343 603 41 0 11404 0
vsize: 45780
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32141 0 0 0 25870 113 0 0 25 0 1 0 422146230 46878720 10345 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11445 10345 603 41 0 11404 0
vsize: 45780
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32142 0 0 0 26870 113 0 0 25 0 1 0 422146230 46878720 10346 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11445 10346 603 41 0 11404 0
vsize: 45780
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32144 0 0 0 27870 113 0 0 25 0 1 0 422146230 46878720 10348 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11445 10348 603 41 0 11404 0
vsize: 45780
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 32609 0 0 0 28869 114 0 0 25 0 1 0 422146230 48787456 10813 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11911 10813 603 41 0 11870 0
vsize: 47644
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 33107 0 0 0 29868 116 0 0 25 0 1 0 422146230 50880512 11311 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12422 11311 603 41 0 12381 0
vsize: 49688
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 33313 0 0 0 30867 117 0 0 25 0 1 0 422146230 51675136 11517 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12616 11517 603 41 0 12575 0
vsize: 50464
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 33426 0 0 0 31867 117 0 0 25 0 1 0 422146230 52207616 11630 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12746 11630 603 41 0 12705 0
vsize: 50984
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 33539 0 0 0 32867 117 0 0 25 0 1 0 422146230 52609024 11743 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12844 11743 603 41 0 12803 0
vsize: 51376
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 33818 0 0 0 33867 118 0 0 25 0 1 0 422146230 53751808 12022 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13123 12022 603 41 0 13082 0
vsize: 52492
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 34220 0 0 0 34866 119 0 0 25 0 1 0 422146230 55463936 12424 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13541 12424 603 41 0 13500 0
vsize: 54164
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 34981 0 0 0 35864 121 0 0 25 0 1 0 422146230 58478592 13185 4294967295 134512640 134672761 3221224576 3221223712 134614739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14277 13185 603 41 0 14236 0
vsize: 57108
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 35256 0 0 0 36864 121 0 0 25 0 1 0 422146230 59629568 13460 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14558 13460 603 41 0 14517 0
vsize: 58232
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 35655 0 0 0 37863 122 0 0 25 0 1 0 422146230 61304832 13859 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14967 13859 603 41 0 14926 0
vsize: 59868
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 35937 0 0 0 38863 123 0 0 25 0 1 0 422146230 62480384 14141 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15254 14141 603 41 0 15213 0
vsize: 61016
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 36222 0 0 0 39862 124 0 0 25 0 1 0 422146230 63619072 14426 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15532 14426 603 41 0 15491 0
vsize: 62128
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 36841 0 0 0 40861 125 0 0 25 0 1 0 422146230 66060288 15045 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16128 15045 603 41 0 16087 0
vsize: 64512
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 37602 0 0 0 41858 128 0 0 25 0 1 0 422146230 69177344 15806 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16889 15806 603 41 0 16848 0
vsize: 67556
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 38260 0 0 0 42857 130 0 0 25 0 1 0 422146230 71868416 16464 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17546 16464 603 41 0 17505 0
vsize: 70184
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 38928 0 0 0 43855 131 0 0 25 0 1 0 422146230 74612736 17132 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18216 17132 603 41 0 18175 0
vsize: 72864
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 39283 0 0 0 44855 132 0 0 25 0 1 0 422146230 76304384 17487 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18629 17487 603 41 0 18588 0
vsize: 74516
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 39394 0 0 0 45855 132 0 0 25 0 1 0 422146230 76828672 17598 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18757 17598 603 41 0 18716 0
vsize: 75028
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 39643 0 0 0 46854 133 0 0 25 0 1 0 422146230 77762560 17847 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18985 17847 603 41 0 18944 0
vsize: 75940
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 39975 0 0 0 47853 134 0 0 25 0 1 0 422146230 79171584 18179 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19329 18179 603 41 0 19288 0
vsize: 77316
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 40343 0 0 0 48852 135 0 0 25 0 1 0 422146230 80719872 18547 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19707 18547 603 41 0 19666 0
vsize: 78828
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 40614 0 0 0 49852 136 0 0 25 0 1 0 422146230 81727488 18818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19953 18818 603 41 0 19912 0
vsize: 79812
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 40863 0 0 0 50851 137 0 0 25 0 1 0 422146230 82743296 19067 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20201 19067 603 41 0 20160 0
vsize: 80804
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 41269 0 0 0 51851 137 0 0 25 0 1 0 422146230 84398080 19473 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20605 19473 603 41 0 20564 0
vsize: 82420
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 41679 0 0 0 52850 138 0 0 25 0 1 0 422146230 86073344 19883 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21014 19883 603 41 0 20973 0
vsize: 84056
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 41957 0 0 0 53850 139 0 0 25 0 1 0 422146230 87244800 20161 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21300 20161 603 41 0 21259 0
vsize: 85200
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 42272 0 0 0 54849 140 0 0 25 0 1 0 422146230 88555520 20476 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21620 20476 603 41 0 21579 0
vsize: 86480
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 42734 0 0 0 55848 141 0 0 25 0 1 0 422146230 90386432 20938 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22067 20938 603 41 0 22026 0
vsize: 88268
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 43090 0 0 0 56847 142 0 0 25 0 1 0 422146230 91938816 21294 4294967295 134512640 134672761 3221224576 3221223776 134610709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22446 21294 603 41 0 22405 0
vsize: 89784
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 43595 0 0 0 57847 143 0 0 25 0 1 0 422146230 93966336 21799 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22941 21799 603 41 0 22900 0
vsize: 91764
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 43915 0 0 0 58846 144 0 0 25 0 1 0 422146230 95260672 22119 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23257 22119 603 41 0 23216 0
vsize: 93028
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 44323 0 0 0 59845 145 0 0 25 0 1 0 422146230 96931840 22527 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23665 22527 603 41 0 23624 0
vsize: 94660
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 44739 0 0 0 60844 146 0 0 25 0 1 0 422146230 98598912 22943 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24072 22943 603 41 0 24031 0
vsize: 96288
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 45112 0 0 0 61843 147 0 0 25 0 1 0 422146230 100159488 23316 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24453 23316 603 41 0 24412 0
vsize: 97812
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 45673 0 0 0 62842 148 0 0 25 0 1 0 422146230 102461440 23877 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25015 23877 603 41 0 24974 0
vsize: 100060
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 46090 0 0 0 63841 150 0 0 25 0 1 0 422146230 104202240 24294 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25440 24294 603 41 0 25399 0
vsize: 101760
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 46518 0 0 0 64840 151 0 0 25 0 1 0 422146230 105967616 24722 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25871 24722 603 41 0 25830 0
vsize: 103484
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 46970 0 0 0 65839 152 0 0 25 0 1 0 422146230 107773952 25174 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26312 25174 603 41 0 26271 0
vsize: 105248
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 47296 0 0 0 66839 153 0 0 25 0 1 0 422146230 109076480 25500 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26630 25500 603 41 0 26589 0
vsize: 106520
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 47624 0 0 0 67838 153 0 0 25 0 1 0 422146230 110374912 25828 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26947 25828 603 41 0 26906 0
vsize: 107788
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 47894 0 0 0 68838 154 0 0 25 0 1 0 422146230 111542272 26098 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27232 26098 603 41 0 27191 0
vsize: 108928
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 48189 0 0 0 69838 154 0 0 25 0 1 0 422146230 112717824 26393 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27519 26393 603 41 0 27478 0
vsize: 110076
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 48649 0 0 0 70838 155 0 0 25 0 1 0 422146230 114634752 26853 4294967295 134512640 134672761 3221224576 3221223760 134615991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27987 26853 603 41 0 27946 0
vsize: 111948
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 48903 0 0 0 71837 156 0 0 25 0 1 0 422146230 115666944 27107 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28239 27107 603 41 0 28198 0
vsize: 112956
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 49892 0 0 0 72834 159 0 0 25 0 1 0 422146230 119685120 28096 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29220 28096 603 41 0 29179 0
vsize: 116880
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 50377 0 0 0 73833 160 0 0 25 0 1 0 422146230 121630720 28581 4294967295 134512640 134672761 3221224576 3221223616 134612659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29695 28581 603 41 0 29654 0
vsize: 118780
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 51022 0 0 0 74832 161 0 0 25 0 1 0 422146230 124276736 29226 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30341 29226 603 41 0 30300 0
vsize: 121364
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 51329 0 0 0 75831 162 0 0 25 0 1 0 422146230 125583360 29533 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30660 29533 603 41 0 30619 0
vsize: 122640
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 51618 0 0 0 76831 163 0 0 25 0 1 0 422146230 126730240 29822 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30940 29822 603 41 0 30899 0
vsize: 123760
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 51933 0 0 0 77830 164 0 0 25 0 1 0 422146230 128012288 30137 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31253 30137 603 41 0 31212 0
vsize: 125012
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 52397 0 0 0 78829 165 0 0 25 0 1 0 422146230 129953792 30601 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31727 30601 603 41 0 31686 0
vsize: 126908
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 53003 0 0 0 79828 166 0 0 25 0 1 0 422146230 132349952 31207 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32312 31207 603 41 0 32271 0
vsize: 129248
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 53323 0 0 0 80827 167 0 0 25 0 1 0 422146230 133754880 31527 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32655 31527 603 41 0 32614 0
vsize: 130620
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 53828 0 0 0 81826 168 0 0 25 0 1 0 422146230 135815168 32032 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33158 32032 603 41 0 33117 0
vsize: 132632
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 54407 0 0 0 82825 169 0 0 25 0 1 0 422146230 138174464 32611 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33734 32611 603 41 0 33693 0
vsize: 134936
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 54881 0 0 0 83824 171 0 0 25 0 1 0 422146230 140111872 33085 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34207 33085 603 41 0 34166 0
vsize: 136828
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 55711 0 0 0 84822 173 0 0 25 0 1 0 422146230 143454208 33915 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35023 33915 603 41 0 34982 0
vsize: 140092
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 56403 0 0 0 85820 175 0 0 25 0 1 0 422146230 146288640 34607 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35715 34607 603 41 0 35674 0
vsize: 142860
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 57303 0 0 0 86819 177 0 0 25 0 1 0 422146230 150028288 35507 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36628 35507 603 41 0 36587 0
vsize: 146512
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 58185 0 0 0 87816 179 0 0 25 0 1 0 422146230 153571328 36389 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37493 36389 603 41 0 37452 0
vsize: 149972
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 59234 0 0 0 88815 180 0 0 25 0 1 0 422146230 157933568 37438 4294967295 134512640 134672761 3221224576 3221223396 1075755419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38558 37438 603 41 0 38517 0
vsize: 154232
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 60083 0 0 0 89813 183 0 0 25 0 1 0 422146230 161394688 38287 4294967295 134512640 134672761 3221224576 3221223760 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39403 38287 603 41 0 39362 0
vsize: 157612
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 60257 0 0 0 90813 183 0 0 25 0 1 0 422146230 162078720 38461 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39570 38461 603 41 0 39529 0
vsize: 158280
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 60679 0 0 0 91812 184 0 0 25 0 1 0 422146230 163885056 38883 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40011 38883 603 41 0 39970 0
vsize: 160044
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 60998 0 0 0 92812 185 0 0 25 0 1 0 422146230 165142528 39202 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40318 39202 603 41 0 40277 0
vsize: 161272
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 61312 0 0 0 93811 185 0 0 25 0 1 0 422146230 166494208 39516 4294967295 134512640 134672761 3221224576 3221223720 134616170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40648 39516 603 41 0 40607 0
vsize: 162592
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 61391 0 0 0 94811 185 0 0 25 0 1 0 422146230 166756352 39595 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40712 39595 603 41 0 40671 0
vsize: 162848
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 61843 0 0 0 95810 187 0 0 25 0 1 0 422146230 168566784 40047 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41154 40047 603 41 0 41113 0
vsize: 164616
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 62097 0 0 0 96810 187 0 0 25 0 1 0 422146230 169598976 40301 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41406 40301 603 41 0 41365 0
vsize: 165624
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27028
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 62436 0 0 0 97809 188 0 0 25 0 1 0 422146230 171008000 40640 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41750 40640 603 41 0 41709 0
vsize: 167000
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 27051
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 62775 0 0 0 98808 189 0 0 25 0 1 0 422146230 172429312 40979 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42097 40979 603 41 0 42056 0
vsize: 168388
[startup+1000.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27081
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 64768 0 0 0 99803 194 0 0 25 0 1 0 422146230 173711360 41312 4294967295 134512640 134672761 3221224576 3221223024 134643705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42410 41312 603 41 0 42369 0
vsize: 169640
[startup+1010.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27081
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 100802 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1020.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27081
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 101802 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1030.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27081
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 102801 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1040.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27081
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 103802 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1050.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27081
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 104802 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223616 134613118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1060.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 105802 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1070.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 106802 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1080.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 107802 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1090.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 108803 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1100.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 109803 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1110.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 110803 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1120.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 111803 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 112803 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 113803 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 114804 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 115804 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 116804 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 117804 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223720 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 118804 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 119804 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
[startup+1210.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27083
Raw data (stat): 27028 (minisat+) R 27027 22932 22931 0 -1 0 65173 0 0 0 120805 195 0 0 25 0 1 0 422146230 174219264 41413 4294967295 134512640 134672761 3221224576 3221223760 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42534 41413 603 41 0 42493 0
vsize: 170136
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 27083
Raw data (stat): 27028 (minisat+) Z 27027 22932 22931 0 -1 12 65174 0 0 0 120805 204 0 0 25 0 1 0 422146230 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.1
CPU time (s): 1210.09
CPU user time (s): 1208.05
CPU system time (s): 2.04169
CPU usage (%): 99.9993
Max. virtual memory (Kb): 170136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####