From 0b961447f23343b093c053e000b4de2342bc223f Mon Sep 17 00:00:00 2001 From: Florian Lanzinger Date: Tue, 14 Jul 2026 19:01:48 +0200 Subject: [PATCH 01/24] Only recreate Isabelle session files if path has actually changed --- .../isabelletranslation/IsabelleTranslationSettings.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java index 0e3674527d5..d63f7ffadc7 100644 --- a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java @@ -156,7 +156,7 @@ public void save() { public void readSettings(Properties props) { isabellePath = Path.of(props.getProperty(isabellePathKey)); Path newTranslationPath = Path.of(props.getProperty(translationPathKey)); - if (newTranslationPath != translationPath) { + if (!newTranslationPath.equals(translationPath)) { translationPath = newTranslationPath; createSessionFiles(); } @@ -180,7 +180,7 @@ public void readSettings(@NonNull Configuration props) { Path newTranslationPath = Path.of(props.getString(translationPathKey, translationPath.toString())); - if (newTranslationPath != translationPath) { + if (!newTranslationPath.equals(translationPath)) { translationPath = newTranslationPath; createSessionFiles(); } From 291ba270f0ec99977b7da136ef3cf4b397fc5f82 Mon Sep 17 00:00:00 2001 From: Florian Lanzinger Date: Tue, 14 Jul 2026 19:09:05 +0200 Subject: [PATCH 02/24] Removed double dbg msg --- .../java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java | 1 - 1 file changed, 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java index b1f617a2a7b..0cdfefc4741 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java @@ -196,7 +196,6 @@ KeyStroke getKeyStroke(String key, KeyStroke defaultValue) { } public void save() { - LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE.toAbsolutePath()); try { Files.createDirectories(SETTINGS_FILE.getParent()); LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE.toAbsolutePath()); From 14aca31bb04f4f9122b169237238d64eb71196fa Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 15 Jul 2026 13:33:24 +0200 Subject: [PATCH 03/24] Fixes empty taclet option even if problem is loaded If no settings file was available and a file without settings was loaded (e.g. a .java file directly), the taclet options pane in settings stayed empty (until a file with explicit settings was loaded). --- .../de/uka/ilkd/key/proof/init/InitConfig.java | 8 ++++++++ .../ilkd/key/proof/init/ProblemInitializer.java | 8 +++++--- .../uka/ilkd/key/settings/ChoiceSettings.java | 17 +++++++++++++++-- 3 files changed, 28 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java index 9b2da179fb6..02d8245063d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java @@ -203,6 +203,14 @@ public Map> getTaclet2Builder() { } + /** + * @return an immutable mapping from a category to its default choice + */ + public @NonNull Map getCategory2DefaultChoices() { + return Collections.unmodifiableMap(category2DefaultChoice); + } + + /** * sets the set of activated choices of this initial configuration. For categories without a * specified choice the default choice contained in category2DefaultChoice is added. diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index f60e1578a60..2c83735ee49 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -392,11 +392,13 @@ private void populateNamespaces(Proof proof) { } } - // what is the purpose of this method? + /** + * Updates the global settings the taclet options that declared in {@code optionDeclaration.key}. + * A proof created afterwards inherits these settings unless it overwrites it. + */ private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) { - // TODO: what does this actually do? ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().updateChoices(initConfig.choiceNS(), - false); + initConfig.getCategory2DefaultChoices(), false); return initConfig; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java index 9ecfe75f261..3cd1dc3dab2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java @@ -97,9 +97,12 @@ public void setChoiceCategories(Map> c2C) { * updates category2Choices if new entries are found in choiceNS or if * entries of category2Choices are no longer present in choiceNS * + * @param choiceNS the choices declared by the loaded problem file + * @param defaults the default choice of each category * @param remove remove entries not present in choiceNS */ - public void updateChoices(Namespace choiceNS, boolean remove) { + public void updateChoices(Namespace choiceNS, Map defaults, + boolean remove) { // Translate the given namespace into a map of 'string -> list[string]' HashMap> c2C = new LinkedHashMap<>(); for (Choice c : choiceNS.allElements()) { @@ -118,11 +121,11 @@ public void updateChoices(Namespace choiceNS, boolean remove) { } } + // ensure that default values are set if a key is present var defaultTmp = new HashMap<>(category2Default); for (var pair : category2Default.entrySet()) { var s = pair.getKey(); var v = pair.getValue(); - // if key is known then the default value should exist if (category2Choices.containsKey(s)) { if (!category2Choices.get(s).contains(v)) { defaultTmp.put(s, category2Choices.get(s).iterator().next()); @@ -131,6 +134,16 @@ public void updateChoices(Namespace choiceNS, boolean remove) { defaultTmp.remove(s); } } + + for (var category : category2Choices.keySet()) { + if (!defaultTmp.containsKey(category)) { + var declared = defaults.get(category); + if (declared != null) { + defaultTmp.put(category, declared.name().toString()); + } + } + } + setDefaultChoices(defaultTmp); } From 8040348a14910bccab3a528362e41b556cf034d9 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 15 Jul 2026 17:25:33 +0200 Subject: [PATCH 04/24] fix for #3927: make examples loadable (JML modifiers before return type) --- key.ui/examples/newBook/Chapter_16/Sort/Sort.java | 2 +- key.ui/examples/newBook/Chapter_16/SortPerm/SortPerm.java | 2 +- .../java_dl/payCardJML/paycard/LimitedIntContainer.java | 2 +- .../visualdebugger/src/paycard/LimitedIntContainer.java | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/key.ui/examples/newBook/Chapter_16/Sort/Sort.java b/key.ui/examples/newBook/Chapter_16/Sort/Sort.java index 4a14d0923e1..29fe71ab084 100644 --- a/key.ui/examples/newBook/Chapter_16/Sort/Sort.java +++ b/key.ui/examples/newBook/Chapter_16/Sort/Sort.java @@ -6,7 +6,7 @@ public class Sort { @ ensures (\forall int i; start <= i && i= a[i]); @ ensures start <= \result && \result < a.length; @ */ - int /*@ strictly_pure @*/ max(int start) { + /*@ strictly_pure @*/ int max(int start) { int counter = start; int idx = start; /*@ loop_invariant start<=counter && counter<=a.length @ && start<=idx && idx= a[i]); @ ensures start <= \result && \result < a.length; @*/ - int /*@ strictly_pure @*/ max(int start) { + /*@ strictly_pure @*/ int max(int start) { int counter = start; int idx = start; /*@ loop_invariant start<=counter && counter<=a.length diff --git a/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java b/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java index 6100333c72c..6882d449cc3 100644 --- a/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java +++ b/key.ui/examples/standard_key/java_dl/payCardJML/paycard/LimitedIntContainer.java @@ -12,5 +12,5 @@ public interface LimitedIntContainer { /*@ public normal_behavior @ ensures regularState ==> \result == value; @*/ - int /*@ pure @*/ available(); + /*@ pure @*/ int available(); } diff --git a/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java b/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java index a70776551c7..57ed1721678 100644 --- a/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java +++ b/key.ui/examples/standard_key/visualdebugger/src/paycard/LimitedIntContainer.java @@ -10,6 +10,6 @@ public interface LimitedIntContainer{ /*@ public normal_behavior @ ensures regularState ==> \result == value; @*/ - int /*@ pure @*/ available(); + /*@ pure @*/ int available(); } From 242d821d3eedac50dcc0a962e62865e6192f70d2 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 17 Jul 2026 13:59:08 +0200 Subject: [PATCH 05/24] Add a command line parameter to clear GUI prefrences Currently one has to delete the gui prefernce file (Linux, macOS) or to edit Windows registry to fix broken GUI preferences which might cause the KeY window to be outside the screen or otherwise unavailable. --- .../ilkd/key/proof/init/ProblemInitializer.java | 3 ++- .../src/main/java/de/uka/ilkd/key/core/Main.java | 15 +++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index 2c83735ee49..de129b2a756 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -393,7 +393,8 @@ private void populateNamespaces(Proof proof) { } /** - * Updates the global settings the taclet options that declared in {@code optionDeclaration.key}. + * Updates the global settings the taclet options that declared in + * {@code optionDeclaration.key}. * A proof created afterwards inherits these settings unless it overwrites it. */ private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java index 5d41c039641..0b144d16d38 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java @@ -12,6 +12,7 @@ import java.util.List; import java.util.Locale; import java.util.concurrent.Callable; +import java.util.prefs.Preferences; import javax.xml.parsers.ParserConfigurationException; import de.uka.ilkd.key.control.UserInterfaceControl; @@ -132,6 +133,9 @@ public final class Main implements Callable { @Option(names = "--debug", description = "start KeY in debug mode") private boolean debug = false; + @Option(names = "--clear-prefs", description = "clear the GUI preferences") + private boolean clearPrefs = false; + @Option(names = "--macro", paramLabel = "STRING", description = "apply automatic proof macro") private @Nullable String macro = null; @@ -258,6 +262,17 @@ public Integer call() throws Exception { LOGGER.info("Assertion evaluation is enabled."); } + if (clearPrefs) { + try { + var prefs = Preferences.userNodeForPackage(MainWindow.class); + if (prefs != null) { + prefs.clear(); + } + } finally { + // nothing to do + } + } + if (tacletDir != null) { System.setProperty(RuleSourceFactory.STD_TACLET_DIR_PROP_KEY, tacletDir.toAbsolutePath().toString()); From df8f7c6fbf0ee2f64fee46068afdf33ee86f06c5 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 17 Jul 2026 16:14:18 +0200 Subject: [PATCH 06/24] update the THIRD_PARTY_LICENSES.txt --- build.gradle | 14 + gradle/libs.versions.toml | 1 + .../uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt | 277 ++++++++++++++---- 3 files changed, 234 insertions(+), 58 deletions(-) diff --git a/build.gradle b/build.gradle index 87ffcd8eb76..91cacf35b5c 100644 --- a/build.gradle +++ b/build.gradle @@ -19,8 +19,20 @@ plugins { // Plugin for publishing via the new Nexus API alias(libs.plugins.maven.publish) apply false + + //alias(libs.plugins.license.report) } +/* // required for generated the license report THIRD_PARTY_LICENSES.txt +licenseReport { + unionParentPomLicenses = false + outputDir = layout.buildDirectory.dir("licenses").get().asFile + projects = [project] + project.subprojects + configurations = ['runtimeClasspath'] + excludeOwnGroup = true + excludeBoms = false +} +*/ // Configure this project for use inside IntelliJ: idea { @@ -46,6 +58,8 @@ subprojects { apply plugin: "idea" apply plugin: "eclipse" +// apply plugin: libs.plugins.license.report + apply plugin: "com.diffplug.spotless" apply plugin: "org.checkerframework" apply plugin: "com.vanniktech.maven.publish" diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index e87424ba15a..3e5c71cc9f9 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -98,3 +98,4 @@ spotless = { id = "com.diffplug.spotless", version.ref = "spotless" } checkerframework = { id = "org.checkerframework", version.ref = "checkerframework-gradle" } maven-publish = { id = "com.vanniktech.maven.publish", version.ref = "maven-publish" } shadow = { id = "com.gradleup.shadow", version.ref = "shadow" } +license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" } \ No newline at end of file diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt b/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt index 777b1ff1bb0..d2c52785cc5 100644 --- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt +++ b/key.ui/src/main/resources/de/uka/ilkd/key/gui/THIRD_PARTY_LICENSES.txt @@ -1,71 +1,232 @@ -=============================================================================== -Font Awesome 5.9 -Icons — CC BY 4.0 License -https://fontawesome.com/license/free - -=============================================================================== -Docking Frames 1.1.3p1 -Project URL: http://www.docking-frames.org/ -License: LGPL 2.1 - https://www.gnu.org/licenses/old-licenses/lgpl-2.1.en.html - -=============================================================================== -Group: antlr Name: antlr Version: 2.7.7 -POM Project URL: http://www.antlr.org/ -POM License: BSD License - http://www.antlr.org/license.html - -=============================================================================== -Group: com.atlassian.commonmark Name: commonmark Version: 0.15.2 -POM License: Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt -POM License: Atlassian Customer Agreement - https://www.atlassian.com/legal/customer-agreement -POM License: BSD 2-Clause License - http://opensource.org/licenses/BSD-2-Clause - -=============================================================================== -4. Group: com.atlassian.commonmark Name: commonmark-ext-gfm-tables Version: 0.15.2 -POM License: Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt -POM License: Atlassian Customer Agreement - https://www.atlassian.com/legal/customer-agreement -POM License: BSD 2-Clause License - http://opensource.org/licenses/BSD-2-Clause - -=============================================================================== -Group: com.miglayout Name: miglayout-core Version: 5.2 +Dependency and their licenses of KeY +This report was generated at Fri Jul 17 16:07:09 CEST 2026 . + +--- + +1. Group: ch.qos.logback Name: logback-classic Version: 1.5.37 + +Manifest Project URL: http://www.qos.ch +POM License: EPL-2.0 - https://www.eclipse.org/legal/epl-v20.html +POM License: LGPL-2.1-only - https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html + +2. Group: ch.qos.logback Name: logback-core Version: 1.5.37 + +Manifest Project URL: http://www.qos.ch +POM License: EPL-2.0 - https://www.eclipse.org/legal/epl-v20.html +POM License: LGPL-2.1-only - https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html + +3. Group: com.formdev Name: flatlaf Version: 3.7.1 + +POM Project URL: https://github.com/JFormDesigner/FlatLaf +POM License: The Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt +Embedded license files: flatlaf-3.7.1.jar/META-INF/LICENSE + +4. Group: com.google.errorprone Name: error_prone_annotations Version: 2.41.0 + +Manifest Project URL: https://errorprone.info/error_prone_annotations +Manifest License: Apache 2.0 +POM License: Apache 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +5. Group: com.google.guava Name: failureaccess Version: 1.0.3 + +Manifest Project URL: https://github.com/google/guava/ +POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt +Embedded license files: failureaccess-1.0.3.jar/META-INF/LICENSE + +6. Group: com.google.guava Name: guava Version: 33.5.0-jre + +Manifest Project URL: https://github.com/google/guava/ +POM Project URL: https://github.com/google/guava +POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +Embedded license files: guava-33.5.0-jre.jar/META-INF/LICENSE + +7. Group: com.google.guava Name: listenablefuture Version: 9999.0-empty-to-avoid-conflict-with-guava + +POM License: The Apache Software License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +8. Group: com.google.j2objc Name: j2objc-annotations Version: 3.1 + +POM Project URL: https://github.com/google/j2objc/ +POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +9. Group: com.ibm.icu Name: icu4j Version: 75.1 + +POM License: Unicode-3.0 - https://raw.githubusercontent.com/unicode-org/icu/main/LICENSE +Embedded license files: icu4j-75.1.jar/LICENSE + +10. Group: com.miglayout Name: miglayout-core Version: 11.4.3 + +POM Project URL: http://www.miglayout.com/ POM License: BSD - http://www.debian.org/misc/bsd.license -=============================================================================== -Group: com.miglayout Name: miglayout-swing Version: 5.2 +11. Group: com.miglayout Name: miglayout-swing Version: 11.4.3 + +POM Project URL: http://www.miglayout.com/ POM License: BSD - http://www.debian.org/misc/bsd.license -=============================================================================== -Group: javax.activation Name: javax.activation-api Version: 1.2.0 -Manifest Project URL: http://www.oracle.com -POM License: CDDL/GPLv2+CE - https://github.com/javaee/activation/blob/master/LICENSE.txt - -=============================================================================== -Group: javax.xml.bind Name: jaxb-api Version: 2.4.0-b180830.0359 -Manifest Project URL: http://www.oracle.com/ -POM License: CDDL 1.1 - https://oss.oracle.com/licenses/CDDL+GPL-1.1 -POM License: GPL2 w/ CPE - https://oss.oracle.com/licenses/CDDL+GPL-1.1 - -=============================================================================== -Group: net.java.dev.javacc Name: javacc Version: 4.0 -POM Project URL: http://javacc.dev.java.net/ -POM License: The BSD License - http://www.opensource.org/licenses/bsd-license.html - -=============================================================================== -Group: org.antlr Name: ST4 Version: 4.0.8 -POM Project URL: http://www.stringtemplate.org -POM License: BSD licence - http://antlr.org/license.html +12. Group: com.squareup Name: javapoet Version: 1.13.0 -=============================================================================== -Group: org.antlr Name: antlr Version: 3.5.2 -POM License: BSD licence - http://antlr.org/license.html +POM Project URL: http://github.com/square/javapoet/ +POM License: Apache 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +13. Group: commons-io Name: commons-io Version: 2.16.1 + +Project URL: https://commons.apache.org/proper/commons-io/ +POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt + +Embedded license files: commons-io-2.16.1.jar/META-INF/LICENSE.txt +commons-io-2.16.1.jar/META-INF/NOTICE.txt + +14. Group: de.unruh Name: java-patterns Version: 0.1.0 + +POM Project URL: https://github.com/dominique-unruh/java-patterns +POM License: MIT - https://raw.githubusercontent.com/dominique-unruh/java-patterns/655c7cc5c71eb9ea0fcfee0ae797269e61845d8a/LICENSE + +15. Group: de.unruh Name: scala-isabelle_2.13 Version: 0.4.5 + +POM Project URL: https://dominique-unruh.github.io/scala-isabelle +POM License: Isabelle - https://raw.githubusercontent.com/dominique-unruh/scala-isabelle/5f28d8e6248f39dd7a31649d92c9850498e3985c/COPYRIGHT.Isabelle +POM License: MIT - https://raw.githubusercontent.com/dominique-unruh/scala-isabelle/5f28d8e6248f39dd7a31649d92c9850498e3985c/LICENSE + +16. Group: info.picocli Name: picocli Version: 4.7.7 + +POM Project URL: https://picocli.info +POM License: The Apache Software License, version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +17. Group: jakarta.json Name: jakarta.json-api Version: 2.1.3 + +Manifest Project URL: https://www.eclipse.org +POM Project URL: https://github.com/eclipse-ee4j/jsonp +POM License: Eclipse Public License 2.0 - https://projects.eclipse.org/license/epl-2.0 +POM License: GNU General Public License, version 2 with the GNU Classpath Exception - https://projects.eclipse.org/license/secondary-gpl-2.0-cp + +Embedded license files: jakarta.json-api-2.1.3.jar/META-INF/LICENSE.md + +18. Group: org.antlr Name: ST4 Version: 4.3.4 + +POM License: The BSD License - http://www.antlr.org/license.html + +19. Group: org.antlr Name: antlr-runtime Version: 3.5.3 -=============================================================================== -Group: org.antlr Name: antlr-runtime Version: 3.5.2 POM Project URL: http://www.antlr.org POM License: BSD licence - http://antlr.org/license.html -=============================================================================== -Group: org.jetbrains Name: annotations Version: 20.1.0 +20. Group: org.antlr Name: antlr4-runtime Version: 4.13.2 + +Manifest Project URL: https://www.antlr.org/ +POM License: BSD-3-Clause - https://www.antlr.org/license.html + +21. Group: org.apache.commons Name: commons-lang3 Version: 3.14.0 + +Project URL: https://commons.apache.org/proper/commons-lang/ +POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt + +Embedded license files: commons-lang3-3.14.0.jar/META-INF/LICENSE.txt + +22. Group: org.apache.commons Name: commons-text Version: 1.12.0 + +Project URL: https://commons.apache.org/proper/commons-text +POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt + +23. Group: org.checkerframework Name: checker-qual Version: 3.53.0 + +Manifest License: MIT +POM Project URL: https://checkerframework.org/ +POM License: The MIT License - http://opensource.org/licenses/MIT + +24. Group: org.javassist Name: javassist Version: 3.30.2-GA + +POM Project URL: https://www.javassist.org/ +POM License: Apache License 2.0 - https://www.apache.org/licenses/LICENSE-2.0 +POM License: LGPL 2.1 - https://www.gnu.org/licenses/lgpl-2.1.html +POM License: MPL 1.1 - https://www.mozilla.org/en-US/MPL/1.1/ + +25. Group: org.jetbrains Name: annotations Version: 24.1.0 + POM Project URL: https://github.com/JetBrains/java-annotations POM License: The Apache Software License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt +26. Group: org.jspecify Name: jspecify Version: 1.0.0 + +Manifest Project URL: https://jspecify.dev/docs/start-here +POM Project URL: http://jspecify.org/ +POM License: The Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +27. Group: org.junit Name: junit-bom Version: 5.14.2 + +POM Project URL: https://junit.org/ +POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html + +28. Group: org.junit.jupiter Name: junit-jupiter-api Version: 5.14.2 + +POM Project URL: https://junit.org/ +POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html + + +29. Group: org.junit.jupiter Name: junit-jupiter-engine Version: 5.14.2 + +POM Project URL: https://junit.org/ +POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html + +30. Group: org.junit.platform Name: junit-platform-commons Version: 1.14.2 + +POM Project URL: https://junit.org/ +POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html + + +31. Group: org.junit.platform Name: junit-platform-engine Version: 1.14.2 + +POM Project URL: https://junit.org/ +POM License: Eclipse Public License v2.0 - https://www.eclipse.org/legal/epl-v20.html + + +32. Group: org.key-project.proofjava Name: javaparser-core Version: 3.28.0-K13.5 + +Manifest Project URL: https://javaparser.org +Manifest License: Apache License, Version 2.0 +Manifest License: GNU Lesser General Public License + +POM Project URL: https://github.com/javaparser +POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt +POM License: GNU Lesser General Public License - http://www.gnu.org/licenses/lgpl-3.0.html + +33. Group: org.key-project.proofjava Name: javaparser-core-serialization Version: 3.28.0-K13.5 + +POM Project URL: https://github.com/javaparser +POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt +POM License: GNU Lesser General Public License - http://www.gnu.org/licenses/lgpl-3.0.html + +34. Group: org.key-project.proofjava Name: javaparser-symbol-solver-core Version: 3.28.0-K13.5 + +POM Project URL: https://github.com/javaparser +POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt +POM License: GNU Lesser General Public License - http://www.gnu.org/licenses/lgpl-3.0.html + +35. Group: org.log4s Name: log4s_2.13 Version: 1.10.0 + +POM Project URL: http://log4s.org/ +POM License: Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + +36. Group: org.opentest4j Name: opentest4j Version: 1.3.0 + +Manifest License: The Apache License, Version 2.0 +POM Project URL: https://github.com/ota4j-team/opentest4j +POM License: The Apache License, Version 2.0 - https://www.apache.org/licenses/LICENSE-2.0.txt + +Embedded license files: opentest4j-1.3.0.jar/META-INF/LICENSE + +37. Group: org.scala-lang Name: scala-library Version: 2.13.14 + +POM Project URL: https://www.scala-lang.org/ +POM License: Apache-2.0 - https://www.apache.org/licenses/LICENSE-2.0 + +38. Group: org.scalaz Name: scalaz-core_2.13 Version: 7.3.8 + +POM Project URL: http://scalaz.org +POM License: BSD-style - https://opensource.org/licenses/BSD-3-Clause + +39. Group: org.slf4j Name: slf4j-api Version: 2.0.18 +Project URL: http://www.slf4j.org +POM License: MIT - https://opensource.org/license/mit From d3f63012e5df29423d2cc6a4c75e8833aa9e9a1d Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 17 Jul 2026 18:58:25 +0200 Subject: [PATCH 07/24] Fix saving-loading when path contains symlink fixes also broader release tests on macos --- .../src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java | 6 +++--- .../src/main/java/org/key_project/util/java/IOUtil.java | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java index 29fe353e691..53a53f3218d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java @@ -256,7 +256,7 @@ public Path readBootClassPath() { if (!bootClassPathFile.isAbsolute()) { // convert to absolute by resolving against the parent path of the parsed file Path parentDirectory = file.file().getParent(); - bootClassPathFile = parentDirectory.resolve(bootClassPathFile); + bootClassPathFile = parentDirectory.resolve(bootClassPathFile).normalize(); } if (!Files.isDirectory(bootClassPathFile)) { // Report the missing directory at the \bootclasspath declaration in the .key file, @@ -297,7 +297,7 @@ private static Location locationOrUndefined(ProblemInformation pi, String path) } else { var f = Paths.get(normalizeStoredPath(cp)); if (!f.isAbsolute()) { - f = parentDirectory.resolve(f); + f = parentDirectory.resolve(f).normalize(); } if (!Files.exists(f)) { // Point at the \classpath declaration in the .key file instead of letting the @@ -321,7 +321,7 @@ public Path readJavaPath() throws ProofInputException { if (!absFile.isAbsolute()) { // convert to absolute by resolving against the parent path of the parsed file Path parent = file.file().getParent(); - absFile = parent.resolve(javaPath); + absFile = parent.resolve(javaPath).normalize(); } if (!Files.exists(absFile)) { throw new ProofInputException(String.format( diff --git a/key.util/src/main/java/org/key_project/util/java/IOUtil.java b/key.util/src/main/java/org/key_project/util/java/IOUtil.java index ea7caf8d9b3..1d866ac0fd1 100644 --- a/key.util/src/main/java/org/key_project/util/java/IOUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/IOUtil.java @@ -908,11 +908,11 @@ public static String safePath(Path path) { public static String safePathRelativeTo(Path source, Path basePath) { if (Objects.equals(source.getRoot(), basePath.getRoot())) { // required on Windows - var abs = source.toAbsolutePath(); + var abs = source.toAbsolutePath().normalize(); return safePath(basePath.relativize(abs)); } else { // fallback: return absolute path - return safePath(source.toAbsolutePath()); + return safePath(source.toAbsolutePath().normalize()); } } } From 024c5595f4c4f261e921e7f1e8a877181017752e Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 17 Jul 2026 21:06:19 +0200 Subject: [PATCH 08/24] Proof > Show All Active Settings > Active Taclet Options shows actual active settings --- .../key/gui/actions/SettingsTreeModel.java | 33 +++++++++++++++---- .../gui/actions/ShowActiveSettingsAction.java | 8 +---- 2 files changed, 28 insertions(+), 13 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java index e9336b37363..31051db3517 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java @@ -12,6 +12,7 @@ import javax.swing.tree.DefaultTreeModel; import de.uka.ilkd.key.gui.smt.OptionContentNode; +import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ChoiceSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ProofSettings; @@ -19,6 +20,9 @@ import org.key_project.logic.Choice; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * * A swing model for {@link ShowActiveSettingsAction}. @@ -28,18 +32,21 @@ public class SettingsTreeModel extends DefaultTreeModel { + private static final Logger LOGGER = LoggerFactory.getLogger(SettingsTreeModel.class); + private static final long serialVersionUID = -3282304543262262159L; private final ProofSettings proofSettings; private final ProofIndependentSettings independentSettings; + private final Proof proof; private OptionContentNode tacletOptionsItem; - public SettingsTreeModel(ProofSettings proofSettings, - ProofIndependentSettings independentSettings) { + public SettingsTreeModel(Proof proof) { super(new DefaultMutableTreeNode("All Settings")); - this.proofSettings = proofSettings; - this.independentSettings = independentSettings; + this.proof = proof; + this.proofSettings = proof == null ? null : proof.getSettings(); + this.independentSettings = ProofIndependentSettings.DEFAULT_INSTANCE; generateTree(); } @@ -56,7 +63,6 @@ private void generateTree() { "These are the proof dependent settings."); root.add(proofSettingsNode); - // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings); proofSettingsNode.add(tacletOptionsItem); @@ -99,8 +105,23 @@ public JComponent getStartComponent() { private Properties getChoicesAsProperties(ChoiceSettings settings) { Properties prop = new Properties(); - for (Choice choice : settings.getDefaultChoicesAsSet()) { + // Issue https://github.com/KeYProject/key/issues/3934 revealed a bug that the + // choices in proof settings were inconsistent with the actual settings the proof uses + // (determined by initConfig). We use the authorative source here and log inconsistencies + // for + // bug finding + + // settings.getDefaultChoicesAsSet() + for (Choice choice : proof.getInitConfig().getActivatedChoices()) { prop.put(choice.category(), choice.name()); + + final String choiceName = settings.getDefaultChoices().get(choice.category()); + if (choiceName != null && !choiceName.equals(choice.name().toString())) { + LOGGER.warn("Inconsistent proof settings for taclet option " + choice.category()); + } else if (choiceName == null) { + LOGGER.warn("Taclet option active in proof but unknown by its choice settings " + + choice.category()); + } } return prop; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java index 40d266773b2..dd6f1c9a7b0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java @@ -14,8 +14,6 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.smt.OptionContentNode; -import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.ProofSettings; /** * for debugging - opens a window with the settings from current Proof and the default settings @@ -36,11 +34,7 @@ public void actionPerformed(ActionEvent e) { } private ViewSettingsDialog showDialog() { - ProofSettings settings = - (getMediator().getSelectedProof() == null) ? null - : getMediator().getSelectedProof().getSettings(); - SettingsTreeModel model = - new SettingsTreeModel(settings, ProofIndependentSettings.DEFAULT_INSTANCE); + SettingsTreeModel model = new SettingsTreeModel(getMediator().getSelectedProof()); ViewSettingsDialog dialog = new ViewSettingsDialog(model, model.getStartComponent()); dialog.setTitle("All active settings"); dialog.setLocationRelativeTo(mainWindow); From c0c0905253c8d2e3ec09f050222d4bc0e852f2f9 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 17 Jul 2026 21:58:43 +0200 Subject: [PATCH 09/24] Fix taclet options not activated after change and reloading (closes issue #3934) --- .../main/java/de/uka/ilkd/key/proof/init/InitConfig.java | 7 +++++++ .../de/uka/ilkd/key/proof/init/ProblemInitializer.java | 3 ++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java index 02d8245063d..281cdc20579 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java @@ -80,6 +80,7 @@ public class InitConfig { /** HashMap for quick lookups taclet name->taclet */ private Map activatedTacletCache = null; + private boolean defaultsComputed; /** the fileRepo which is responsible for consistency between source code and proof */ private FileRepo fileRepo; @@ -104,6 +105,9 @@ public InitConfig(Services services) { /// combines the found choices in KeY files, together with the current settings. /// The namespace of choices has to be filled. public void computeDefaults(ChoiceInformation ci) { + if (defaultsComputed) { + return; + } var currentDefaultChoices = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); @@ -145,6 +149,8 @@ public void computeDefaults(ChoiceInformation ci) { } settings.getChoiceSettings().setDefaultChoices(defaults); } + activatedTacletCache = null; + defaultsComputed = true; } /** @@ -456,6 +462,7 @@ public InitConfig copyWithServices(Services services) { ic.header = header; ic.justifInfo = justifInfo.copy(); ic.fileRepo = fileRepo; // TODO: copy instead? delete via dispose method? + ic.defaultsComputed = defaultsComputed; return ic; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index de129b2a756..ffea403696b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -23,6 +23,7 @@ import de.uka.ilkd.key.logic.label.OriginTermLabelFactory; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.nparser.ChoiceInformation; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.JavaModel; import de.uka.ilkd.key.proof.Proof; @@ -508,7 +509,7 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException { var warnings = ic.getProfile() .prepareInitConfig(ic, additionalProfileOptions); addWarnings(warnings); - + ic.computeDefaults(new ChoiceInformation()); return ic; } From 2109cc801a6b34b08218ec38094ebdedede83c9b Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 17 Jul 2026 22:18:10 +0200 Subject: [PATCH 10/24] Fix that open most recent file was not enabled when starting KeY fresh (first after first file was opened) --- key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 6 +++++- .../src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java | 2 +- .../uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java | 6 +++++- 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 2487d19eb5b..749ead9509f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -332,7 +332,11 @@ private MainWindow() { notificationManager = new NotificationManager(mediator, this); recentFileMenu = new RecentFileMenu(this); // Postpone load for faster UI creation. - SwingUtilities.invokeLater(recentFileMenu::loadEntries); + SwingUtilities.invokeLater(() -> { + recentFileMenu.loadEntries(); + // otherwise open most recent cannot be used with a fresh started KeY + openMostRecentFileAction.updateEnabledStatus(); + }); proofTreeView = new ProofTreeView(mediator); infoView = new InfoView(mediator); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 1416a019c2a..7c645310d72 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -183,7 +183,7 @@ public JMenu getMenu() { /** * read the recent files from the given properties file */ - public final void loadFrom(Path filename) { + final void loadFrom(Path filename) { try { if (!Files.exists(filename)) { return; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java index c9750f1d060..3216866acae 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java @@ -27,9 +27,13 @@ public OpenMostRecentFileAction(MainWindow mainWindow) { setName("Reload"); setIcon(IconFactory.openMostRecent(MainWindow.TOOLBAR_ICON_SIZE)); setTooltip("Reload last opened file."); + updateEnabledStatus(); + mainWindow.getMediator().addKeYSelectionListener(this); + } + + public void updateEnabledStatus() { setEnabled(mainWindow.getRecentFiles() != null && mainWindow.getRecentFiles().getMostRecent() != null); - mainWindow.getMediator().addKeYSelectionListener(this); } public void actionPerformed(ActionEvent e) { From aa642e156dced58c2326af38adca52cb1943c08c Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 17 Jul 2026 22:19:28 +0200 Subject: [PATCH 11/24] Minor robustness add-on for last commit --- key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 749ead9509f..9efdb7fac14 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -335,7 +335,10 @@ private MainWindow() { SwingUtilities.invokeLater(() -> { recentFileMenu.loadEntries(); // otherwise open most recent cannot be used with a fresh started KeY - openMostRecentFileAction.updateEnabledStatus(); + if (openMostRecentFileAction != null) { + // should always be the case, but better safe than sorry + openMostRecentFileAction.updateEnabledStatus(); + } }); proofTreeView = new ProofTreeView(mediator); From fbebeb0b9c8b5e3ca7e62281c7c9f7e0cd2e5c04 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 17 Jul 2026 22:55:06 +0200 Subject: [PATCH 12/24] Increas forked JVM memory: macOS has less memory on CI, so the default is not enough --- .../de/uka/ilkd/key/proof/runallproofs/ProofCollections.java | 5 +++-- .../key/proof/runallproofs/proofcollection/TestFile.java | 1 + 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index 236fe99821b..8447fa0bb7c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -212,9 +212,10 @@ public static ProofCollection automaticJavaDL() throws IOException { * If the fork mode is not set to noFork, the launched subprocesses * get the specified amount of heap memory. * - * Heap memory for subprocesses (like 500m or 2G) + * Heap memory for subprocesses (like 500m or 3G) */ - // forkMemory = 1000m + settings.setForkMemory("3g"); + /* * To run the forked JVM in debug mode, set the TCP port to listen to here. diff --git a/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java index fa70826f758..cd7e6f53bc1 100644 --- a/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java +++ b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java @@ -256,6 +256,7 @@ protected void reload(boolean verbose, Path proofFile, Proof loadedProof, boolea if (settings.reloadEnabled() && (testProperty == TestProperty.PROVABLE) && success) { // Save the available proof to a temporary file. ProofSaver.saveToFile(proofFile, loadedProof); + loadedProof.dispose(); reloadProof(proofFile); if (verbose) { LOGGER.debug("... success: reloaded."); From 7bdccfb03ece4905dec971073f21baf9813644b9 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 18 Jul 2026 02:50:39 +0200 Subject: [PATCH 13/24] add description to modules --- build.gradle | 6 +++++- gradle.properties | 5 ++++- key.core.infflow/build.gradle | 1 + key.core.wd/build.gradle | 3 +++ key.ncore.calculus/build.gradle | 2 ++ key.ncore.matcher/build.gradle | 4 +--- 6 files changed, 16 insertions(+), 5 deletions(-) diff --git a/build.gradle b/build.gradle index 91cacf35b5c..b6a7211b062 100644 --- a/build.gradle +++ b/build.gradle @@ -313,7 +313,11 @@ subprojects { pom { name = project.name - description = project.description + afterEvaluate { + description = project.description + assert (project.description != null && project.description != "") : "Description of modules are required at maven-central" + print(project.description) + } url = 'https://key-project.org/' licenses { diff --git a/gradle.properties b/gradle.properties index 7937f1c737f..e12aa899dbf 100644 --- a/gradle.properties +++ b/gradle.properties @@ -1 +1,4 @@ -org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8 \ No newline at end of file +org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8 + +# do not release automatically at Maven Central +mavenCentralAutomaticPublishing=false diff --git a/key.core.infflow/build.gradle b/key.core.infflow/build.gradle index 208feccfd64..a5d119bc749 100644 --- a/key.core.infflow/build.gradle +++ b/key.core.infflow/build.gradle @@ -1,3 +1,4 @@ +description = "Information-Flow / Non-interference calculus for Java using the KeY theorem prover" dependencies { diff --git a/key.core.wd/build.gradle b/key.core.wd/build.gradle index ccf546b22cc..233b71c8d66 100644 --- a/key.core.wd/build.gradle +++ b/key.core.wd/build.gradle @@ -1,3 +1,6 @@ +description = "Well-defined calculus for JML specifciation and Java using the KeY theorem prover" + + dependencies { api(project(":key.core")) diff --git a/key.ncore.calculus/build.gradle b/key.ncore.calculus/build.gradle index e54af4cf6bb..c2a26ef8629 100644 --- a/key.ncore.calculus/build.gradle +++ b/key.ncore.calculus/build.gradle @@ -1,3 +1,5 @@ +description = "Pattern Matchern New core KeY theorem prover" + repositories { mavenCentral() } diff --git a/key.ncore.matcher/build.gradle b/key.ncore.matcher/build.gradle index 0ae89f3256f..a4014c8f4ec 100644 --- a/key.ncore.matcher/build.gradle +++ b/key.ncore.matcher/build.gradle @@ -1,6 +1,4 @@ -repositories { - mavenCentral() -} +description = "Compiling Matching Algorithm of the KeY theorem prover" dependencies { api project(':key.util') From b15472911db21aed282440625e82f38455ad5335 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Mon, 20 Jul 2026 15:44:48 +0200 Subject: [PATCH 14/24] KeY 3.0 logo (used in About KeY), extended copyright notice --- .../java/de/uka/ilkd/key/util/KeYConstants.java | 2 +- .../uka/ilkd/key/gui/actions/AboutAction.java | 12 ------------ .../uka/ilkd/key/gui/fonticons/IconFactory.java | 2 +- .../uka/ilkd/key/gui/images/key-shadow-3.0.png | Bin 0 -> 94495 bytes 4 files changed, 2 insertions(+), 14 deletions(-) create mode 100644 key.ui/src/main/resources/de/uka/ilkd/key/gui/images/key-shadow-3.0.png diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java b/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java index ad764324f60..5a5f59039bc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java @@ -10,6 +10,6 @@ public interface KeYConstants { KeYResourceManager.getManager().getVersion() + " (internal: " + INTERNAL_VERSION + ")"; String COPYRIGHT = UnicodeHelper.COPYRIGHT + " Copyright 2001" - + UnicodeHelper.ENDASH + "2024 " + "Karlsruhe Institute of Technology, " + + UnicodeHelper.ENDASH + "2026 " + "Karlsruhe Institute of Technology, " + "Chalmers University of Technology, and Technische Universit\u00e4t Darmstadt"; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java index a1f5b133083..1fb5cb65aa3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AboutAction.java @@ -22,7 +22,6 @@ public AboutAction(MainWindow mainWindow) { super(mainWindow); setName("About KeY"); setIcon(IconFactory.help(16)); - // About KeY } @Override @@ -31,21 +30,10 @@ public void actionPerformed(ActionEvent e) { } public void showAbout() { - JOptionPane.showMessageDialog(mainWindow, new Object[] { IconFactory.keyVersionLogo(), KeYConstants.COPYRIGHT.replace("and", "\n" + UnicodeHelper.emSpaces(8) + "and") + "\n\nWWW: http://key-project.org/" + "\n\nVersion " + KeYConstants.VERSION }, "The KeY Project", JOptionPane.INFORMATION_MESSAGE); - - // JOptionPane pane = new JOptionPane( - // KeYConstants.COPYRIGHT.replace("and", "\n"+UnicodeHelper.emSpaces(8)+"and") - // + "\n\nWWW: http://key-project.org/" - // + "\n\nVersion " + KeYConstants.VERSION - // , JOptionPane.INFORMATION_MESSAGE, - // JOptionPane.DEFAULT_OPTION, IconFactory.keyVersionLogo(108, 68)); - // JDialog dialog = pane.createDialog(mainWindow, "The KeY Project"); - // dialog.setVisible(true); } - } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java index bd5006b3a56..d3503a96fcc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java @@ -169,7 +169,7 @@ public final class IconFactory { private static final Image keyLogo = getImage("images/key-color.png"); private static final Image keyLogoShadow = getImage("images/key-shadow.png"); // The following should be updated with every major version step. - private static final Image keyVersionLogo = getImage("images/key-shadow-2.12.png"); + private static final Image keyVersionLogo = getImage("images/key-shadow-3.0.png"); private static final Image keyLogoSmall = getImage("images/key-color-icon-square.gif"); private static final Image oneStepSimplifier = getImage("images/toolbar/oneStepSimplifier.png"); diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/key-shadow-3.0.png b/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/key-shadow-3.0.png new file mode 100644 index 0000000000000000000000000000000000000000..d900bee497efb18b3f42b567cdb64f4c183ab66a GIT binary patch literal 94495 zcmXtfbyyVL`}fctiy%nqiqZ|zAhI-)N-QY|5=wWYB1<>YND9JIvLX%A-3tmVDM&8e z@y_%8UGE=z0n5(p%$#%X^Qk*RM@xl*l#vtw017o#m>vM&oPaMSVnXm8R@BHF@CS*D zs#c3?l&C z2h?B+FMP7Ln|+gCt9Wt*U}F%c<^~2{FAd8$Qwo(EKTgunJc~+Dczc)dp^UZ6P}X_c zK6B;UA4Wq&gEJ07?%hwy6huPyg>T-D1c;!|q<;uC3JF^ZGJNFO*2*#E=CNq$rQeV85B64ogbKyVQ$ylTy@?;JkXc9H z!C$Et>SkcVi>(}6`Eci5HJoB4>}|BvJ}iR?SUDH!jtCd3o<l@BbpV&T+aTLHT2ZShwx6-C9pcy=(0uuI1s{ryif!Xjd7b$0vN9y1Yg|-;CsJ_U%1GRaLnR-o4%4 z-fp9kYx;upe!wJPYW!c_A6~h9MV%`Nnx_K^z1KvNw%~%F7PyGofy!e?fTXu(oGCJrB%WOs)BEW zfPVs(9Z@st_*nW1Ca0eY2GY&@`C{FEF6Hj*>_@xqll>OExcAn2D22Y`u*i7hu-etv#ZAVg0cAf&IkzC1M~Gy3U+taU;Du#2HD z7earST2qryF@So=%L5mgn3T0%zjdOv14-P`Tn?TgNXXdXYt3EjEKY_ymyazU7PkC( zpHj?4A@E`eN(bk_X%~>jEH6U=X5*4)Th^|wy3Z0VsQ&L6wAsdA*n%f0$mJNaO}c(l zF02gz-R?HgEANG>*&d=Bjc}rWjH~b&1mzt>y*OvSvc5g z6l_cA8W1ogqGUEonVYUr?T(saD0@{@FC00kV!Uy9c*sEGS2hI=kxPGLtXwvfuqPJs z@X#9NyBrbZle4|h%9hB!gnH8cw>}0OmOtR!vu>+4x?ga&EPnJmZ$V#QpF=|bVOCl_ zyzpwp_PeCZoYq%70D!$PX1=LzwMQ1sI|-Ql%ouuHiL(3e3oYh8>XhFb~=BW{zE)6JZzA9DZ?kKMQqB zz@zz23OdIc=)g~e8T>aS&UxaD6mG+>bZJ+!I+P1S(Qqr<==|PB7M=kX;3yaz7d*w7!8czrM zQn}gm?!@qaDm1@;QCNSHpIuQnTE))u<6Utejd#GKa#{pd7@_(wU!l{+ zfEa3k#Q`R^jx}@E`%QLXg)u_hkx)`(qH=)(8V)|c7qkR^1M^?!!%`9QBf5@bGr0Gx z8MaX9aGP)OlN=lzeMx>f>&eBX{WawcIoD#j#ihH)evb!g9Bw`yvUB4o9uoA|)7-ED z3`LV6J>WocTSsqtNPQc#<8-bb85!{>p)fpfL)zBI33c0Ay{&epcHG!3<9m@a*_^U# z7U7$tuS-kYBV_Ez6$!0DC%VUGxzj2^KAnQAjN!-tQKybjrPhti-wRd9TCe9UN<$QK zk}AU@@_YaK4#ORXYocR>n3W(@CJ({osbUPZE(?r~v1~?P{Q8B9!@TbhR=6t*$Ee5U zBMxK?mrP&Tigu5xyFWVe@TE?mhOGMr4IbLeOo+v5gOyo<4J)wsy4|6WwSl%d1>=Ac z91vEYc%h^V8!Rt@RZi=7GvES|D`_zN7@=>bX*w|Q|GXANKuA6(@C6G$5{E2F#CE|4 z5WTQYb*|wW@)#j4$C$xr3^x(bTSE?nG_N@!Z9>`|Ov%W|B<6UnqlKPCE}i4Lu;XIr z)4ArcbfuRRE;;LkCNkr7#f$wL#8~A1xwzhO|Gx439=u9b7J19&aKg3+&9%m%A=si^)1kbP+i3; zvFoXK!M9W$S(Feqlu|`Wq)H-7tM{;H4vLzvRmLCj@Me z`7#sn!o6EQyk(m%B{&LbV^_06sD>YY_qZ%Gul$rPH-NX8=Sa)ZO zRyiFn(P-|^j@{GxdP#EnQo%p6lLXiK51@2;mjsX5U0To1!tBlrXuH~!fqsHvc$uP= zc(;x&EjPQjZTI+b1R9=|p5C6%Ir@2%9Kx$-B8=gn*^^lD$-S+%48zLr{o!<+mkhTV zR8iWLd&(aP<&Jz7b|3nZwyWl!w>*bIhQNco%k?04Q(7ey*GcaBdRg3uz8cMQihbLJ zO9pFZ9`G6|%WHn}Pmm}MSO*0Kg-jN3>NT5d+ZY!I=)_XJ)ky4w>55v~WVT>OSAAK- z&Zk)MR)j7VhFI}c@IkOB)m`jc485by+Zfy;`bo#QjkL66u)A76Cdx+d7Wk- z#Sa7&HJVqhPehKw$&6E%T-M7tpikVF=Ew&eA0p+$g*HvKJhFdeiBGv>mvAM<+X#R! z(TX^>-C(V5rqB6KMy8_<%L}Q&Rd;(#sAH8)o)46}xGCQFCS_#~w@D$w7s-UJL69A_i_R zjpR;YZR+e*dR23rdIIyY>gl7g+hlYo1I8J5#PkPne&}nmZtn`7~7d$vq z?vB#;J65u_Rz`kY2(FZzy{uv^4Ic^jJO<%~acY84@%W@lg5RRlWH&?Q2OcDfpI?6G z_dzYXwc;<#m{rIkcu&m6BZzKD+SFnee)+L#MqGWZfH(k)X_nCZ(^0W9)Xi5nrx$qR zf^G-z&Xsn*GJH?_bv_#;ngj%gX~kSL5Mhxgna}S-d2g;}TPbhXe$yk0-%Re$pB456 zC&-;v}Q(t)| z9orYU<+87WX-GmfWH>OIL8_BGI9hHSn8uNE=(HKbHf7IaL0q}#`dK+S%GTsDF0Gfi zBBU3LKM8?%$f;4P$uZ%&ox-d9i6A`Jtzb6VTA$lrCTFo&mNkiPVUDzBY0THL>|O~2 zD3u5!S`kywOKiEaPt?+SDtMJIf7QTo6Mv)vxq-iCi=B>m#;Bmc2r$gOxDeIOwxM)x zz7_jz^Cke7xbEF`-7}B%tfS(9r9G-64Bn{&QVmv8yC^i`F4}FG$bKJMg8C#g^2lT0 zt37weD&@nugEFupWyWb>PTim9WSw)-l=BU1KE2sJ5fA!j$f|me5q)w za`YDaB>_>B`{+&?L5u^W-`mJ#llZdsqczG~D^L}fN)5)z|0p1TINx-;KYcg+b1H5W z3pFG%Kjcg5M+WQrBkr7$xCm9om`_K3vKDN(raPC!Z()W+48*C2$K?@-5>8TXK2Oqltf1FA_YhJ{HC&`tsLRs@L*y-vovXuz2$m9N8Q?qTUBm6V!qgXfdX_!s(>y|_%xyasW zsB0_nCB^WbH4vh^5wg{FbA8#~=!SD4+aAsqt`N24ee_XY^P~)NeJ5hIBj#~RXudA( zgP^4f0siZOH#d@++EBWld)6LNlA#u2)zG+Z*T>bC9tshtHH~`Wl?W)lqvkKGcpWXBSM6&I(XxAGc zHr>E+@QQ}*u}d&kO*$G)IRW6r*52Y9v3?dLeMPmGo}O+Ke41Ip8HsNhe-&6Zzju9O zidH<*ev$abRx`2Cul#nI35&X&j>9H?^0npb$#pQzX?;CiRxq-2&DIfoxSGQrQD{$U zoT|Wlx{@#3(*7%k?Ga`*2rDm&wK)9C^5@;kN1hKsZ35) z$IR7nLe)ePaI-)Oqv6jHkMh4!$518mIO8daChH|g+xS)d{Ff|_Gxg;hLAzPO);z#s zv|WDk1c{DQ`uTz0r-aJm7B_N2482oGY9L3HmDBm| z?17`eRj|TDY)rt{0s`#Z4fpBx1h&}uW-(LHBO-N`U!9AK&zoyNvMisIeL#5Q*zaZG z)zy_u?1zobE)n^Q;hpzKHGjU<2?8X6yP1`@I~`&y)gT9-4%KbAP;Yl@HXr%AewO7C zhERubTM0xyW3u+prB&vli_p{c8me!_AvN*LqLRHjV^gvSUX&g%=SXy_BLh_KPU#kY ze>qd)*^+237dfZ`@l{>!z~Akgg_~Ske4W@2uDr30zE?GV8PkD|i*LFz65!{5FGQHE zm*UBKLm3qnMMKlV;qUyrQu!!T>7eHszyHa0=zOC$-qYZTrPc*-!mIcR0vFS^8O3;+ z-0q9}N-c+N&VS6l1`*qBO$#gNoOgX~5|gVsdVIC?kVpw%*{lXZ3=T%9#~^RP`wfHf z*+8WpSHbzUrGvQEZb5c=3RR}eFFgRqRh)Orjp8ZVvx(Z;N}yWTOct?>^f(rN^ywF_ zs9K^OLp$X~lm9raN1Y4yO=vNk4-veqRw5fBo7HkFp682AEyH*Uj!EWdB01d^%+i zYk|F}U+icN$8Y`llUOZL^MtNCUSJCu^mj>pn)@3Xjevl7##<{HS zJ2YLENIm#NaE!Wa;p2FI<1H?KJYcdfo2pROcSZ2#*7j&U91}@^hwt|@SNld82GU7( zH7JbTH^;EuV^|VgVtI<;lsNbl)&OA*Yq#I!;|Hj|D21t&-(34`W|g;l(}3KIl?QR4 zy5!<9WM(irRc2Wa0;f!+5}6UYlYx2%&aEFjMdU!*a=%CpcCFa_MUSuE(%qx4Sf4tJ zkY5N4??55>#lE#U&t{EYFE{*eq`}qS&0uV5n!E=m>*=n0tPI;= zZ|OOSRT!=B$B_s_WSf1?yPOd>2S2D3B@M4mxmF&^R2zOA9$eN}`Cut!&X?v?Ugu2d z1p<>dd3y9{ucrwoORRx%Lkb zU4SDEl>RB{p7roTt&jxArLzls@`u~<@v1|}^_d=0Ir~|%ZL;Ck>8tDcTzp{9y&paR zcjWA;8^;6|Hcc-Xk`^;0j9t;*4c@^XIY_Ol$`nNeioL&w zo-*Wlw&HmV*5FOA#)0>Lf9>iZ?2`2!8^+J9=iGYfit6^%eVhflrw3-WV>(E zs}<3TxGQbL*j<@LAg;Q!js(LLSMN|^wjv~fV!|Ue(OOa)>{V#1dY$~bUa;U4jO}r0 z{v&D9to+v7JiSF>wC>7G^>ZbH_}AcjT^Jipo%f?~#p$hM_5kO-oPJVr5(~#6gzAnL zQ?wBID2Lyz|2^xO#$83nAjGOH3DT~M>Q2D9&%Dz`0m+xcg`URcj-fYd|4f7UqlopT zvAu@a#xc3uIVxaztszwz2WR^?$F;ww%ZA+XJf61$vMa6tb(cCJ+nq)Uawp-nF=33d z^^m0$1AXOh(X8_x@yE}51j2&~zQCWtEapzhS`P~vV(Vyf#yeYR3?`-mnGCcyLEbz* z6)4@aWGN|ORk|hoX8xz4%$A?MvPv${j8oEunI3wx`}1A|1Hb^e2Px};LSdcu8IkT< zpe`5Z(ov~l!4`&OKLR0hUS{)TS097E@!uV<%>O2r8W%x~@&^D&O9udu+kaX$3ksx# zMCX@4Pvd{a2<7w|Jn{?yYbQsXGaMl>ryCj6`hyWW2@U zI8Vz_DdIR6Zl5`eU|d}`-VGE)6FAXP({E`Jh>^3I%pg*PLy67|5#9m{E5_D@tXM%3 z$_kesa)rcfZoYzK=onH(je>Aa3C103ZAPm^$NLpU$>+V3eh*t^Z&S2RCGTPU zU?7__Lv3$Fy3l~|YfurQhJ?DuCbBDNV?fQR%O8gSD=YX`VnCQ0av4CX=&h#-wiE$uL?-6Go@TXzk+a z3IQ1vIK3PXq`kIF%FjkqILJem!b=G>oqEHSr-$c0Jx zcXy}zT93#}OnB0qOq*;EtF{VS{ltJQ-C3M$8R5K%k!i0cvAyKlnK)%bwyA2q$*Dk_ zdWl#Sf`NN%yz5%Qf9`eFf0w7y>G-71?i{dkbIY6U(H9{I6^2y1SHPKNOILk|m2`VM zJMlkD?PNHeP1UxdTK*{iryi5e@0b(rQ+Pk-;7CAJ&F;CE1>*Ca*^6^`O`vYq>c88 zZ;rnkRfIVLf#;Yb+Xogva1EsB{S!NX#nbZpty@VK9xumPjKf|Pt`H7$^&b?v2J{?2 z87I_j0tfu)K(SysYK?b5LXGAwgg^2fx#c{n)%%wy+NU3KIkve8?%F%-flTNs;+RU_&+GNm<3y%=fMpd# zEOI^j*h|Ml^PSr?0nV4pyEm}ii?P5*d5vvwZ(Ul~RGYy;aBDEFXQzTT7Q#S8X+?Qw=5v zj)|Hn7hS^!51DM$Vh3Vx(|17uWSVe!E#Uy{hhP0ycKf>68&~@jQW1@NciIPeyBS=E zs}U}V>{iHQ_L0zIxu*x&THzX7*#(@8HeChN%T%l~oCU;~+zCPwOk6r}WHJ?7^C!^b zYIT*Jrzjr5?cIb*&32~*RJoJ}H6K+=11^(1Zr3S|!2>Nm)0bP3ua+i?Ep~&pvl^G! zu-6W1Yd{eXhG9h(@)9u9fzD_M2+GRxwJ06@^cfmkn#-(Mu!Z{B^L@Gl0C<9ZZ%(h5 zi72PsnmqG=3_szJLKl=>uJN~6o8+u>kGL114Ai-lV37#I&Gv`+2I}|Lv$QOJYz>VH za!k9*ZR)JECAGG$I|FUP->q%GCV$(_cGu$SDmv)__ta=1<{lvqwO?SZE#QRnF$VeI z7=KP-b;|iwZEj?AzcoQB;H)YmJG%(1hua=f$?OrJS0XAYsb-_dGPUFNGNbt0?9Qg! zl^DPP9S1D^n$79T)7T?kt@Se8xn~W9M8Mds))48|kcebGP@`>Sy_~+5g>&?cb*P(d7_*BPQudT$5tEcO_Wf#WYirjN%R>A5gJnkXzjeed z-@tnXBR^~O_jV?=XK+VJpS>^BXd8QbwWhZ(HaAUa!xm~?(&v|w^uApI*=^f$BY-k^;Eoq_ShV zZR7+l$Mz(MR;0VB_qypfdrJ(dC#hwOpS4|2v`h#5%KrR7o9%I{B|0pBYG{c2V)n&W@8I&Jc^OQpZy1}hZMfZjM`i=PBt~;P( zoa&2YjuGmYRQXSn@2`nY)?wA7%lWsgG#P3u?l*zRGGUbrFLEKV~HR5wp(ieg&_ z;o;*n0`eTZjGX|W&Lxmp<*t=h-~Sc>_>ax_&6>=E*Cb+p!w1w7_lPxenlmjNccii@ zQ=V&N>5+a;O?~a=me@=wFCy|VFNziLDH5$utTklE>P|oRi9x#-=+jSq>F41Yk`gsq{-rFueoHD6n!WCe(%^u8 zK>W!O_h!wNJ>7&uJ+oIYm`B^ zgV2hWBpwI25A7IK3jP9v)$rSKXKi_Ad8G1se@<)UVjg?lC4Yh+hxj$fOf46s%Aoof zXd4_f59hz_NxAJA9F(&YR-@65r0Y{$Kn}qjcRi$xPKYe62Z8pw*>}XEK7Uc?Q%9%c zN?2qQD6FhY6D(^OkpGyAOv{1A;DxQtTp)>}ueettl2e^^-l}(!D&z zhL@I>Iw;(8t+oC!{-2Ynr((p^=J>Bg`Dwve8^{KaP=}F&kc33`ym2YRK~v+k!E%{& zke%go97Zl)H*>hc*opP#5SryKyR?e4+7qI#+zO&mC2y#Y)c^+~Tru>OnKFsFf-N${ zh}v7Vjg_XFjQk`%34;?A&Q^QX8#E9;i>W!e+rZ(keKxp_bTLfCC(2>4wKaq{YQbh0 z3e?GRa6<5SFuv~v^d%+PeJcMOlC;dsB+f`XiRZhV$kWInXyw4dj#oW- zh=-h0ess)U4ugrGfof>~ioo2l$?pMyi!Thas5NI4i3`Vb^OWYjE5i(dx$|H&X)%v1 zRb+p+P#In2J&30GurpD}fKx+IDur2;80xJxzSpzh!};mkx*|BG4{e(nTi{A1u9MtG zRTA5-|26goJ9INw(C%lp2U>Obqa4hYTz+QFpiAvkR|eLPtz$;ss4MGbKB1QxYPu$?`Tm5s5_&?}qz#XG<`a)?7F z`=3YZhYPx3$>@w)^lRkHoT|$_yujs?xB*pfx_AkQ?(vMtU((E3tM7+zW02qJw6dPl z=His+68Z#K>%z`lL#}XAk6N;3PwB4qWa|U}-G>N4g+&Zu7INO0piEnArDa_%_)-H zHU6i&^LVV;keF035J0Dta4>%dr)|}@BEU4P_1p*VpSM=D5_?UfR&)8!%|UPU7%v!A zGJ1P-jJD?aIKcN19P)gYP8f-zE^KciPb4y!#9Wir0)zySRal^U2wN zo|&0RuSW;&6I7N*O;#Jq(BAHtiQ^>Lto6eM_(Zqx*3{{ncqV3jtgPOzNZ8u0c{L7o zr-g>pL(mrvn7Eh7qZAL1+#d!`U#d7s4?a>Bg_*;bNC8zCXRNgi@}+UA?!9=}u;fel zQqI4Zr7=9tL&wcifx_aVVl1WE^!GAa5GB=Q?O9J;o)!EM?7>0QQrxdsedVV6p*Rmm zT7g`iKOSR$zAr88zjrbydltgs2UtQ%=k}n>wdn0&@1o=hc-i>NN}w%*7!U9j53HOn zctzGSv0-WaD>X*wrBb6#u)ND6fV6GK{y}MYVKFh{3jv31o}Pz8;vJxE()Bf+avcTg zFlvb|Unko2q6ndGy0q=YpPP6he>JWm5%CQx?I!bF`oUdaN3P!T$us7GKF!L|+T!@^ zin zMA#_ylZPjr(wGaA0Uq#4K<2NNe|PLWDyw8g^R`14o8pwZ98bmyiQ21ouW)O}15|W7 zcf3r-MgOv^t^QYunFZ^V&3v50VkXC%>0dwMX^w7FhUAGp?`VUuWf?)FfD+JdX7?yc zK4|#HjdUuykWSn4wW}^82}IW`kC^4XI{2+Rw&C(j=d?Rib(Z>ZMdW1X%LJ)=kC&E} zQitn!*)G<#Tu164QM-bDpM~z4D#wb5NW;p<%d3(Fg|!WgV@Wae^=h$TF=&`Llmkk?mOI1g^nDCKB;8d!9RV$Z|*+UgK>NG zWs*i3-1`RO+SNpI%eH)a-hZ`fm=(rloSG~0=qT{Mvd+?S0f)to0xk*Q=VQa;X7Jt zdYS>;4&6jdlHGqfJCPm!#x~K9FDGOK-Hm_OXZ(AB|K`zpmVx?9t}314PTh29S+ZVG z3@FcnRy=5OIfyd;hwbJ5+q^+LIY?YJv}`L`i`eukp>FqeqTe@f+z>(f!QIOLJaF@A zp*Vs~`|0bMl#rhrN(V|`u0QdZH+b)OJ5j_wGc>fJrhhm4BL) z`%UR3F34DszYz%6ll2%OC?RE$@BG&HYW4aBzdIKfr2m#!Cx{eH07dSZFci#)z%ev08kAiXM`h7(P!Esf?N|eFM={Z4bZOZ=Bb}ykva`_OTrG z@tV^0Mii zEE3h7&q)n=5DE1d&J!Zcb~o}ec?g5`W_1i=hO~3*ZF$hmy77Hyyl<7m_lV*!R6q#g zWr{)(ZSoWW4kVBKH3977ctbcSZ6fkj{hC?d&i6 z=KlFN)g+bWwwuX0Ko4^J2zyyy9F>&&s0}G_^zuD}eBCJpThNz^6&9YH(2dsDpZv0IqbVt zSo5Okcsa}61|?}o8^%)>1J329pFcTUeq~K7E7D(WZ|%8S%t4g%3-P79joGY?`U9~rgk~!CI zG}pB=oRJ>)?o}dG-xwDca6+x4!CYJoZ&~Cttx~9pev>U~@Cz8q>1HZTORJ}ZWTIH~ z7ftF~Z$5Z~X3$VuQsRuttAd6Gj$_V9&H-VIY7NQtZ&G^?>hVHSHMAR(wP%COSk@m7 z7abKfF7VWE`92dsdP!^U4cGUZZK#0)bak8qzvpoR|Cw%K3kYLEN!@~E6sIq@x8I^l zE|oA0`Y)p=;5@mnbo`Vw6WQq^UK`(yP<Z7;P6+AgA zz3`0Mf?OLaerbynT1@f$Hp;-`w@Pt7{gv&rH?kVG z>qMWw1XE_Zv@fT&vfO`WII>zw)>AdECb1{*4pa?h6IuLx9BXaCHAbhjRO!548Embo zI~?U8_f-B%Euz&8`*mY%SRVc4EOPlua=mH(IeQYK1cm+s-%@Mgb}35M>t;Bh6xXK*+2xMqP%4r8mLmq zJUy++xr$ztlqpI+XgAsZKEYx0S?)SUFUnsV7JRxSKS?F?V?n@3oy$4>OlinZLpIiW z%WO|BrJKIc{z;|`GXYjDkoG@RViSl>s5q@+E_SB`!-b_28=!6c0=#RC`e~|Ps!c=k zlW*#Q9T$~osoELqq8Ek9ku;v&=lc8Z3s2}Q&LJ`Sl|cDd{K^qK>!`MX$c;BCaWnT86OC@cSV=!lI9FlE#}`hdhL285OaDvf zfzFhLlb2ZYynp#8@%lVWPJjb8ygF%mT3Y%E$M4TOeq_l8jjg+iBe|{T6wby$sr}uu zuaR9k&ZpKSE}agQI{^;e1g*E|L;R(hhFFd^GnaFY*QdFS4YBpcK6;Q#WiVQ&0_HL= zrS|^9^yE~$lDC?h?g69G%wGkh)^{vl@HGc-SYD={IWAo0>wR+*@EgDfB17h~g}T4~ zkhCBRLS7lkYjvP6;DvJAe%gtJ@I^(QX3cw(9ZufPbf4~8`9|SWp}*?s z^O^Ri`;kMY6K8Po8vnf{kFNBBXj0R^ViNa#6e2B|>1$}iQTyYven{NP45C+f%ghm} zUTV`e&I^(gcC0!mcYQG^dz3TR@ueZtx#iw7x6>GXFnJ96j^}fJV9xL*nU#Q~sOR?SXPwYjdHopL)ejq2 zMsPzE2H)s+)Ngy9JBk zeJmGU0@3cnv;u)^BOO1wB~e*#Dt!bmu2@=$t|w6xTbmey*2D_RQSS~miqcC`w^t+> zkf4D&6u&;crz$Q+T>#nE%b-tp&V}sa^r%>BM`09aelmCOo;?33Ct0i? z{LcU24x7_IGXX1GHZ}QpS8Au90atkB##nQItXHFy$532k29d-w^*nRa#LK600g3D{ z4Mi=;zs@^-=kTtq^Z(p5Ju6%9-#q^&27#EmWb@Zq@LfD5*wi3d5wQ&-%ne+#u^D}X z%K4b{v=yBkmiB_V=YNsf=o;RFSIvPwS2>!iLFYXd)(j2u&2(Xt2G82}QUaaNDo>}u z>eij~39N1p8^HDP(DOJi`3KH>P$KjGYiwAbR5w+V1RIb&K3xbDD9&n!@HE%VJgCBe zB0rH)`Xr9BVIorn@drzxah5Cd z2u92~y42%Trv^tNv1Q7sZp;MR691f&!q@E-^VmANcJ>|R@k#s~o<{S5t%9WX7lBux z0CCw;80>LI<{48Bd^<|iulQWQAt@g;T>mXJd3u)XA3lBJr3;6I#iG5Dv%vg;_E~+R z`eE187beua->)&=7PpPJFQ)f@;A)dvE%2Jn6P3L-E^e-HLcW9*e)9AL1l{_NCgzmB zHc=99F{tE8vt1}Q-&PYnxbNxs?yukJ`R3NxRJcYr?u$Y>mr=oKABltc^{cvWr{I{v2fmm<*>8~`z1>YYpA1=tI zm>!;_<#;)yt1~FdUp_>`sji$l{`gb7NKuQ)mp4)oO@%GIN}CJ+u<_||wpl|i*4hxv zjb5G5;cAc-C5z?OU!PWIV+>~jN3rzQvny}6XtfPLar7UY&rNX~y6P`?@(MUXi*$0v z9+Y*B1+#O@Y%*qRj`t(1P}qx^;}P6=cuh2z_MfwQwGR?v=d!&*Gfr^$>(F{eA0K-p zfvdzyGugr&Bds*?nq|F!lKIBu8s+b-t4_D{i#EQ2&usrmtTof-X2GUb9Q61=C&jat zrWB9ae(^sgjG!;fuR(j7gx;6)Ax5@Talwj>I9Xp^383zBS$j0GPlj=}JDJ*Ys0I52 z06Ni1OseVrQfmF?0yp9@f>Rl$Pph;o%cFCb{2;D?^T3mUTOcMbgAF||TOZ!J+Gn5q zS5DpewA}-Ylq~l(Z@*s8=X7i7Jg71(YZ3syJnfdb`6b(mSO0EW?B{s2*PqX(M^X|s zE#)Qkm(_!Z0r%6K{QUfeEE`hXX0$!rTK86*bLcxAH>GkAMigBObBB&>!<$lT21_Is zUu-A4B-ITC=qaU+C-sG%>;DInC1O(q67x|NwF=tLWUR{7~UAqW+U|#J{xPsdve=wX~!lrSK}btGy1qb~n(U zUXl2;1Qm5mXb_MBW3hF!NM3N5f1oqQS0J&akMmVwwF2DwcW;GYuZiIzv&&`XOk4Uv ztO`@(F^J;q=!{Ni~6dB6z9U`)T*`IS;0(;EwGKD`ZuGh~Y5? zBmietPe4BihTs2QxCB)}T4f5NX8;&|`=lLCcKyj7u)$$W&&eUQ{bc){1f&d1F@&qW zl+gFx3}AZ=4gi94N50f~JO#%XG@Kp!Q7eNd-Xi;QSoQ)}Iz>ElB1YD-WV z$^MR6AcRRr9p_lOJwo91cfI`#t*_tnmc=+6mNG*_|J}e0v}|I) zFrps!b{iee)8x^5Lro6DV4bB^vL&@I6mq{q7_!GkN6wJ%#->`Ak=~r*O^RJ_xu>tH zb}N#{TTC5(mm*2=$tIQn!l>ULuZe(EqKO!8bL;4(d`{Dxb><$|DQ5eb0lH*M{zde4 z-8f$OO+$+Ufy>kvn~dS0$0tz|o^V-F6R-{Ha((T47u> zGqFRTFfKs7ID68vgx7=A+q7LF(b)d4{@^vqlvWm&IU-*cjOn2NM9!hmQ!qSWB}dNv zTVVH`fC5G5!~0gdQhP!&KYd2;_%h&&exqzcq0goE%ncVTtC)8&^H{U*>g$a-dLxGc zUoOqk9{)4LQuAKGw|e1B3UtR#kL%Lcn~Glz-^2l;-=|ijy2tQvbSEaYpFbK2&TXF< zew5D{ofZBNb^TnIb_%=u{Xu|Ew)O()!?h0D3f-1!k@D<0B1}%2zEm(knPf3HC?YyB)e1 zjN9q?Z$PD2mc3-^{YD}P37d+??0)KYIerrJCO+~4I0xT2`%@ME_+cwVUAA$>!5<*a zyiaMc6(7tu;x59SHoUb1^0GT-&hobf&XQzLE6TTg$P-UqV3V{vp`v9=Bx>7RQ&Tt> z=bLh^Qsk+JklE13+m2#oOV31G;$cBMVbcS!rth)tg+)h~V{fo$SoP9xUkJ(TF@f+* zy+|bLWlMwh_5S&0hmzeV-Y+<2vZgYIP*3dsUg0iJEGSxZv?;d!RIFcAtUALBNf-TW zDt!-oAprQb#0s%ke-G{cmlW*F-Lm!$5%Vt85o3oW;`NfCvCt*Z_ak{rTOVHP!up`T z(x9muj95P3XLJPnwW4;c`T|xiu_`@EW(9rvF>eaxeV1CPq}wTC<|DHge=Uo>y5MTN zh?-`0&hno)o~7N_$g6n%34vJrx_g#;*{SYmg+#ppxYLWe)JdQp!bQWd&Pb4oX zqdGNYD=MpmZ5pTMjU;7*ts3T);SYH|4+<%5<^zDyBIzf!GXoU*b2E3%jtQS5*Qciu z)^{FM3|Ue|(uNytKS(&zz1xUy_c^POh59p2LsmP>0|E|JT5aI{GtG>TW9*?hu;^lv z0v2N1PdX!{B}vp;Rtr}TZG;eoAlq8deV(x6Ni1w=lsU-LG(ERU}Ri`{vzL1+=bfy}rV=-ule2zp_bGxBXl zF(qKi+|xqmIAziN`>j(6aZFrDZgzHxZZ*l@T{i#boVXy1wV=~N)?$(ihA_QhL3J)g zVX;O&-xF!-eD}Hl-ne_q_>pWi8m(`Nt^;{?u4CB(NBdXa*;d>&gV6%OdRCkrYqNyg zc`39cnGpe+w=dK~5wUkX54b+gYQ3D1(bqlHeE%={PBW$4d&zeu2ZIZ{ztNZeySvWZ zMOEzm+)}K-7fw>uM119hMrY%UVy^Pfa~)X0Ns?Hv?U@Il31fo1%V6Cm89wjyc|dO< zXs(^%18|M5gg*Q0{iuj`+;I2W!@0O#!dn8v@_v~I0-C(HCCzf9i|(bnG%PtPBD zhEPp=^-Ar3gr4XcJvRgk`BOveu^-q12T9;I>m>!gJ)_ovXUIv>LBx6*(&g8;>)z+X z{cgvp*e+=UuP+yLt`~pyOHIRPWk!&o?qXy84irO2+`WchCbWSpN`DSLIzB zm=}YZ|K3u^>hTE}v;ae>$$fol{Fk+jyaQjR9A0GLZymgU(r6N@IIEr3X(O~S&7>q#Y`N3Tlgb5m2`=rk$UP^pAhLb$?F~P z0Xc@Thr~~rIp@iA&~ZNN4S7o&O490TvC^b*aI_dI5>=G3HOR@&5Qm~H;yghVo$ zb#BfLFkY0`J)BJY+(1eEGd5`#Im~il5Etx{sp=e|aX(-1;hlv0Q2%9R7(buaQ`lX| zzt+!+j)6r=1vRuCrY^u!=r1>2rQAEQ*B^AJcW!g^Y&!R(&Od+6FI%Vo9(>l3f)Uf)#S~@PT>rTrql_1sPi+zOUyhJ6bdmrr*m4yTh`*--RLBS?2yXOiaO^v;IrHYp%a#kHpjeFX#*gasJo9akihCnc4Ayh>Fr^ zCse~+nP75CY4`KI$2Big!(GR5DOjf-W$w)F8WkFSw(hg|v2Mojk7qRWn9jo!nh!=w zHd`jAE#kUu=5JA z;JXv{Zx}OzD~e0m6em$rljanW#TA*6mG-hZ!Nfaa>g6w))iR;mwJ9ofN z`r6vgj#b)*)sCaOrRU`+uR;uF!(+5@wHZ@^^773wL5dOhNka7Mjm>O%pSLQoO*K$xWO8zd?)xqOZvANYOZ^vg9D&Jz!hIr!5hSi~ zKwC^t$K_O18L0C8#)^$uH6?|84bgh-oDz<|7{Dkmk#(;=lGD-Nio(K^>A03Z!w6fYlN zH*Lc;Igy|EaiQgRQy*A<-T%UWl++iy6P2f;h>`Id6mCvs2QJC%?!h zc>*8@KVw~2=?fPzmOPHsp(dMY)AQb3=}=_`$O~y@z|UBIdg_{ynb{kGIc~%ESy2M- zKag9A{Gb`BAz=>#Aa{n~LD>GNA-LFI@w**2dM3pHfVIlY1zw7iJ|C{c9i5O|qmh1R zrmPzFRrZ?Tmd^`$UH5IDAs9J{q31p6b@osAD4P%CRekU~>Gt5qj=#Ad%{g8<{4D8v z9P8OHdi}IA<$irtb_bpAgYeScoQR!h+Wq3ZNOxIgjq5fyog5LjR9AR1jx98f_OlH1 z8IkEgn((IMJtfgQan~W!sksI1)ZnOKyP<|1-`o4(%um!jPD7@5Es*7px_OJ^XMr9tQTLA`;c`}dSj_s< zmvF5FY%*{Nck!SZK(VMI_h-CxKE!6qB*zr2zL0YaKhFFhP` zyRB{P{t zxTuNAO12V}o3-vX{Lo^?_AqLtHVWT^@_W2jTRVgk{shQL@A4~c&=lv=9>kJ(iH_La z0nw|BFqKeyOYIb9QA}}GW8k-{>MZl-=W1`;!r#a>`sU0Z0wHs>}UTB0T;J)(<6iP`U7HeudK86)AIYHG$(wyQp(z?_s|(PmQ#%8 zpS7wo6Q8y-G=_ven_)rX8KXj8);+{|i29Ss8h_(U;yE4mnGZ(gH`jVb-$seq$5Y2F zaaZ0O=6k_8w61sWSwteWeXJ(;He)lsu6SaKb{P3IutRcqVo+d-t<^DSdcI#GVq$)r zSGw%X4{^{&{pL)^Lo4V9(P~@Mwb-^irxy*hu~u4&A2+uypHuigz0bhwn(E`B@Onpdc0w$YX5X~M7s4-XQ?AAmdpz&>>~-Jk zrLBY2bAn0K#O+_hIu48>9|@KHL$G+r2CRujuReGT?Da1E$G6em&1xHUgqqxLK#24% zQ>36A-+#YtxI7WK&p6t+pAvXFH0w+gEDCe^JHELM`-F|W*kD>72 z1tt(ZCTZoc1dMe*n$qs8dIa=J|3GvqswLf|WRj)x$N-uK8NRUN$EImcf;>DJ0E4AZ z?T%x0d&M8d`sp7eVN923VHgR{kH4nf=4J7|`?SB^Zk5)+k4I~a^t5ypQvtP8nG|s` z*g>m_456An#cudKqJ7Mq=fQjOcOsMvHlG#OwIPK>W}-8u$HEkD~K|{&;))S9aS$<%c7fBZNQcPtz_#v39|I`WhR1+eR~?U10)iIP|Qq4ZYWYB0Ue5 zcp`$RP4ZdKZ2=BEEn&~E^^RX}ruk+NDVvoI5^+c6ut;?+G___c?Rms7Oy1w$17o8k zQ($c5J`@@PTN+G+zl^UfCSL+3;f;&#t%vn<}XjaodP#tz@-pD|p$Yt;GN zXfAI2C?lJ@D%oi6z~P!gr^nd%4O;r!T&;yhF++TbN_;(&?U&RLp0UY)aX9rK>&To6x3Woj)SkLLy@Y8YtP&f z(KYjvrV!1ZLn$aDL{&{KUQKQCo*?@|uAIB^;Ppp{Detc_A&n@ljrQxD>C)D-P~*UP zgz_c5FWRzzZb}RnY+LuL#O-%cqSx(g?5|FvYGBd;n6J>h)bvR}XXiR#U3%1~BnG4CubwaPSRKj7SE$J2${M4-SxYu~;zNYhOC<@4U6r{}L(fLSL`pS0$OjLRzio>X;YpjODi^01^C1Q*vYE$sZpqqF#$11h z_;t~lca%1Mdp%wejB4KRG?;BiirMU0V(k_FE$v<5aB}+3F~?qz@-MzxsPh))i|5GK zXzg+ErW?JqoyUD6U8|km+hphWj6}2XSM50PmU0cdT5Z0%R$Ur*pz0`b=~Ih*&M9(ndl_l$;j>+FPaa9;3pg~LtnWsCEh@EZFw!QLw7!d)1Oc*YGsSOfl zL5jjdirD&9ic+|LLS zc{#6F3zqRDZeYb{D>kMh=gRfv_Z)0@*}SHM#$9{j`rya*i%P9{2eL8sBRL*9=(>VI zOr@vnOPAg(CAk#*9^c1KcEWu6hw`W>@pi+d#Z8c9|6$_Vws-3C1sIxhCD#gjW2uN^ zuaBoImMu#qJqu#u?MmJf0@+%98T@@tg}+NN!oQTc?ayJ|`p^Jra>ddi2~VjE#?#k5 z6IAPKKkT3KP#m^!_&TG8FB|qw9zQeRj?DLML)~&6q_gY5fuYP!9_Q$PHU6yl5&FU) zp%+{C+&}=lvF)SAOaYHD-j<3BG2z6qNTGBx?)_?roQ#z%vQJ|Q>{^QK{4 z$i*>wQtoOrv=j1fMo=hUbud)Nszv25p!$^6wwAnv$DIJ(On%%u=up)F3GlZW$|ib@ zy7n$6+fWudF3NB>GXpB#!WMVI%^%4fuqXs9Zn|-iRcHYW`m3qdXVs-hHMI!sq4U2aeN;H&ntI;WggzNxzkIKNG~H@kpC%bDx&KXfSWFl#*GUWpWd}z^M=vBz1QY3DqE2=QD2h zjA0Ppn2cr68pH9K|7Ft*xFNF5!aXWKiGPLDQ#-VHrW63bp23BnWkq0WMH=CW_1Af< z6d`NDpC>}Ybv?%JQCdX(w2voJ&A1=;ETD4xP)9Kr_rCUg$!?`55l2qFN{2 zS$v53Uuxk)Lbj%E+b&woRjYKzGf3N81L|6t^z|UD8

-d2uBqEesvdR=S*T`>DSY zIo%K1)?JDoB$-@g=hF0w1s?!W05Kv{6$7n|<20POoVZ)YjAQ)YM!BDI4P>FHpgq*;aKx zG5nJG*;Q;iAl|B?pGNFb=Hjg|v@ytH9_=;|RwOcr9C~Nha-=)0k04NkwjS3oN`lrV zA~zEMxqTCq9Z9XZQC^OwuX?JN!$6&Y)QPFq6mdQY@pg~o$ygGWVVr{7(em4n%X9LD zbtm%C&+%&=f4ngK)a2AQ!ce{`k>_o#L`bHM41s$y_hS!Er=bYh<{qnbFEi6vY7~xz zZR8Yvvh9{xIo8VK-EUhRhi$uMG#5iM>4)22lpY#pnpmw*=KFuQ{|#7LdZP*M=>8hh z)ZW_78!>J+s_ZYRD7=^(&JNmQ9AEz1Pf4yb|6QtdGR0_A-XIk7xXEq9W4 zhv)1@!y@InI3h`6xU;4ATit!rg1CF3Q@N^~8sfU@Uw-DPBt3o$TR-<3vKLQ=bz2Xe zh1DRV&vlIn$zD+72ZI{<%C>G7De6|H-fuTo(`N&IYUgd1Z0kVxVkJh(hpBD;OYMK$ zw|-=^j|AEs(+okd6z3c81}nSP`TePAKVHT4+2Dtf z{oS2m-oH{W(TK7t1DgunuTp!rq8c8%nuFPZ2?3h0l{ERiRQ)4)AFIt0Rsz@w`NO)I ztBJa$uzZ?!TbSm z`lA#wz26cQJNq(UH9d(bm6^^_(uyS?wD^aFHqi<82}gmq7$^ralan1<^rQ0iMP-Qr zHwYoL`3~=RuXZZU^cjt~S5j~%t%lkW`uYg?%67rvZJ zc8iVifgyO{JuLk(VL3&qzcj5HN?wAy;_O=6Dml4D<$JnQS^+EUa294z>PtiTKW+&f|J~BxQ z!42$yn46ntPw&2MTLOT28J|TNZMn@-lN;yWViOs>apz@)>qH^LnjD1g_rd~YP>L;p z$n%UIw-*iW6G`f`>7T^;HinY&tVp=g$1Q5;Q*4vgt@53(p+jSc6%@2lN zB)_pIFL@FTw^o<#@(CpJ(@8Tq&f}Pd*>QG`@25Y)IrNzx2TQRduJWMpWju1!cO=}^ z+^*GC3VVBY2QGGmB>HI z=!(HkPx6R%`^WFk(vS-1(3DW&i=gv3m6Rj}W{+bLe@kTJ5LGqj?drV}{Oa61uM1Z) zh89y8L#D(HUxqqPJ|+*_Nj9XvY9QWp8x7cPA@^P9aX2HS;Ev#Q{+p>Z{u%e#_z^hO zp=c0%YEfM6-A3J#$uE;%Ow2#WBBT!DYkzHs{g*?5*r%^*@mIxe%*@`N_HR|38NVCC(vYq*Kx$@NILy9ezdm2x)`XNIZ)EsZ8Ob>I_I<&_ z#hdz)mp@E|%Yf9XWioDgYC`GGl*W7a(dAw*nx*kyeK9}ej?*>b+&`j^;F7wcP*L5> zy7YLbCrNgNLnR?U&&{!mZ}Rm|pG__Erv6N%dRD}&>`rhb;^(&S_4 zkG|AU?cK6W>)?ZS#fJHN(?jq4+VVW!k5+me@6m=Mzo|0QHs-LT4HQE>Esz^!wZ?uK z1;uuC^Im&1+~8xekxW1A5X~Oe++k?O0SpJ0T0E!E`jS?D|CW4ws`vv$@PUDk35oLu0xmYO)$EX?6RtwaUl8dTK?WJzwe31+<)`60+znW z&Tek%z3nVKP8N3g_qJ}wCcS?@QW35Nzx?vtZvHf|n?TX21APtO421?{fSD{LOnE_u7FGl7>~5thLECgUQ~yY0pw#=qmW^zb|m?OI#% zNKwCKv@@-wgf66c;0^19sV2GHTo8?!am-FI=ba7z7pcEh7M1rAYg0}4!ds=&&AM@D z21YCnIv)&xBJ66?{p{#%>Yq?Pf%kO1&o_v00@2jfq|4Ohf!C6x))Q{07NIfiSBEWc zq4|c_P9(Kwh0{)mq+9!~gX`t2X4D6A#%B+TrYUkEYotW4WbFf@!^S$^fku2`FhK#@O5LGDZ5- z+N6{8-IroqS8=l=^_>tLD zR+d8MH^)hfpXc&7m&6Ap z?86LfY32xMcNZhN9A1)pY{qjJ;CJ#=vw#2Hpgi@F>Wmyec!+!zB=;l)EsM55REm=w z!2+Ce=0p;SS^Q$DJxB&pA=Eowg|GL__&OOX60ZgE*4*}H{DG|q-cc(^)%#x?j$s*JFjw=@wDHx+@tM#82Q_EgX{G?P#1ZxH)5}lKQN%o7uG?Nup4+*5-S|0u zc*qrTg@A3gX!MX9B;*HtoYzlaj5qBAJp;=1==V}gOQ&;a5Zl(vjYe$~BO{}qt==)3 z;V9~|+QJv4tK7FV*Gn3$|Nbtm2J!d67+-hyXQIm2j$+$FmGH@=?!G39hX2s`2eyW^ zvc2*Xa9O(_3Jp8qy4>`C--kecsxJAg`(DXAVRcyjCjtK(roTIkIPIi({r>Qk_q9L4*4xo_Y_PhO zYHDR)H8v-ACh7HCX1Tx6rH{_MFshr+XOPWfeavU^m`d2M&rEhWg-lO=#IwUwkpg40 z^W!a71jhS(4Rz;T3a5j%o>&j;KXK;sO+N6FI36JoPW%nj}z z0&j1C0)%qBF0*^Ej3`gQfUDBv}CH8Cvp0(BOS$0&y^Yy(!cW$EnLH&5qVbk&EQ06Yj{PDwzw|#6I zcVF+zfq8>%QhOXo^%6+{>!pB=~mV?@j3MsT({rpuVA;L+vkL=P#c)7%e|O0fa1#Xrb;~!T3}w zNdlP@-!)pJI=t9rrOdyO3=sw162rx@FV`WU=6Zu$tMc)+@g}8?mD)$1z#n`BW6=sj zIFPKf3*vu<_AAh{+NH&`<`wLqwTAIbEXePvFzuZx4N{+bjevj*{P@Sh3>QL{i4Qug z1bW1VOK+#0b1c0(NOh>B~2T_sG z`w>1JNG0OxKFa_?^T#aqp3C#PX4S&#vP@`~y6$8}M$eG%F`~|EEBZ`)7*%3p(J)_p zv~%lY@RfR_#&Vnq7!Wry6$4ji0v<@0U_T)h~X0oXFZDo_WjoHV=;y2 z?zOLGTYM#8e zvX?rLYxrmFH}%qP^K=)|FqtbL@Y39Hy*}SRijMLMvTNGs|FK$Jb@9Bs?amXxG$Ltk z2#n^hfCMz z_p4JbA{{7yo21@W70dbJlN~y1!g^;ch;f=Q1Q%{wLesP|U7ubaW?pF$?%~34xzK9r z;qq_7sImD<^Mcx(bh4$xa!$4AxNeGuJ_sEb^Q!@-FilUKR6vP}Z^|34C zo5{+?hiG2rKD>22JRC02K=|#B^!t50wAdxPQ-xpk7`#W$^hzo3|fMwZ=0_ zWxx4tmCszNyRTeGU3KIVNM)%>4x!W2iEIKThd#foWy(~aGl=A1t=BJHFCQ(6`mV@f zI!RY267j5hx*zP_#@2h^C0Mo{qEc;eE8tzFy?FYdA6%zh)~K&1d8h)%&&5~hxm#wG zSg9Lsb)@gXjg)t}_HK*1Z63}gbO5RNUJ=DN6Fa3?4TCB55}hcXf1m@g?(rey{n$I< zxVlN%kdPvsjTPSpeU+b6nHOJ%eUKzW4UKt^nfyQpG9HCk_t2LWnlF0!cZ%JOXmry< zAGQtRWl8LcI@;+|vaB=AlgXi4%8`CPINI_e09`Er6R?#{e(%haOF*C(G^_y|O@x^s6bu6(|;F zum8eOq2AMrA3yAhwHfTQTCp}ghjV0+Aa{uQNh8G$FgSlR5E5_PVCisFk=b1fX$E7N zhjRNh9{$PPhGo_p%*lTfKXS25otg_ROfD#nKdSTt<_XVNCz;RuB|Ltum!ntobv{^n ziD;~ej8|~?R$2SnrBkT8fa&u5?n{t0(f)CWLr*8<-H+ypY!RMCBFVaaROL-VERszMlUaY3V zR>McjvR8AcE%CGE=zBNsjW1OWWu zy3HAuz`PwrpM!n)gC8RIC^{$V=heCbedOkH*DSnhax&0kHdur7$ zsjePp(ubJRyXpx~DX8{+8E?nD>)z{p3fY;Y-N89*fp_bblsNW~_szH#euPucC!vU7 zNC$HLW*4oCl9C(-*&SkmvRX(Z9o$3S&Ck4ilG`tzv37LfCjPaGZR8O@{ zwI^VyRxPEj2u8=1B?>M4vPn%GR8}zkiM=&WbC^7@jdqt}ResFf{_u?rqIs4|%(JH8 zr6hiUe2j_0g$Z$eFN8BR?4+6Cuie6)cdMOP&(H0jG#XrWj0}z{kkc!zr)L60A*}r| zp!q-qdE@y<{@%%tJIZ^7l3(B*M85kow8@D5Gxuvd*DfcuJ{y#G0O|FTW>karkh|4& z$w_VEjS>e-ha$R5S{5c*VAJUu8Dsra|4wGK@ciJw0 zqW$El$o$aK==Z~~F(}xSxgmfnbTs#gK9AS!)5D--6Dbp@gC^AniMD$JT5ZTG7I#p1 zIzOckWzfyyj>FDIQDaT4DqPrGKvnVf8$XT? z^iLTBPWzTG`$BdgkvYeNwB8ugL*u>Te#sPuP|p6b?(c5zqNvZfzmBGL#%~;NKiX2% zdDY%;Ce!TZNAzBLH2nDjKpAvN7HkM5La(q@N2~QPn%@~@u(X{KVYlJuzne)J9lpmq zp6l$1T`P6ppVF?HnnLHUJkc4qN)*sHyL*9+av=(9FdfD*`Y0}b+n|kD@X&!HIT2@) zn`tcV&q7@#^DxQivgL4+b(I51Dw9e|Dv+gi?hW+yxT27*_7`9O(-R$UY-o~Qp@1ZfdL?&?nb&L{?*kOG}^9yAH0+VE_o;^ zU%_Q%-xE2}p@Lu%VqX(CgTThAD+Lc1t>wzuA50%oV(qmrGN5x)zy=DYA{Wh;^xNpy zsfPsK?nk;UuS2WAopRrxH(GzD1^*Jct$&j9I0owL9RS8CUP($G7Ov#`a-w;Tt7BZ4 zxwk$`G0@dL1$}H_T_8b;@BQciWLxA5U**0R9!S*uoK=L{BJR2BpK42sji#4EziCSTp1(z zSiWt@6SUGa4^JDnGCiYzd7ZP_5;%;gp@JxEb=Wye;o-k~2_uPLJ`rWU&E*uGrq_Es zu$AP1SC7%opx8c+<%TU$vC+kR+1Tb>h(rym>W~>4Y%_hYqh{`(eJ|-u4Cf%2m1`D; zkh}Fcak!D$-X=dTRyT)uAO80JL_pmx7)Gx|@eBR@(EM%6P@(g*N}i>!-c9A_ZdNm?`O_i3VXI z#=}-c2U#x$R5UzQ)ueyX=8(+4#&b4ClHU6YwTj7kx=1U#F>vmd{#pA{rWV5hjH+_TMBP4dOCV*imDY&- z7gg+0_@NfU%R>X!i|p6F$Ht31G`Bqc7P1{X!dg6-G|c^qEC1nvByf(j=%qO8D!3qO z+G8TlY*A6nVI^#b=J0OeOS30olxBj49s2llcb7^=xWHv6u)6ghuu^_<_M7avb(Z_C zV@Tl#C~vC%l`-ykVg_4D@7==jaV{F$&X0VEFf>kPpin+%K`u)?wDrOVIi^uH*^H_U zXbMWgTIhZlA?BK|N@-i3?+EL5y9=5nC=~kzwYlX!Eh2OXHzqTT%G|GI7~Kb1k`$)H zpcA%z%wMh^`?~ov?j`C#n5Y3^8P1FLa#hpTt9Bdbi!O-|uyXa+2YF;q>=tfGLs$mZ z1>MSOL8B+pwAhhOOwf0iB2MKQH!aU9u{{}yeWvr>Cv>;_^_I4ie;DSk5#}X|i^iGG zs|l-~LD-^PjgkuLdYAg?aN)i6JGmyqwX!IiG3;}ZI(H75^z$U*+Ewl6$q%Z^ zL? zhJAfri6=R7ma3FZd_HL7k@c7M*15qiCp!*Rx&x)XS=5u7r3|uP^!2D^AY8Vnp;sly zU(FuctC}`(eT(nJ3ut^!mXnWmXrCO`PRYBU6(zW8MLFdkm;fv{CgZ<{wHq6=0S?k; z#>lT}Mc9TY%9it%-pz?&0mwi*TKY?sC>9?T2rkSvw z%f=s=pWcuC7qCJBX_oKBIvrmt7t^{5Dc#W^ZVQpTZI@!t8q5k)3pN^y|3F6H{f(6!HR z2#3`D=w)Ms|I*T4Fu9-|P551TqFolJT|1W>G1?p8{|vH=s&4Im7!M;&WR5(UP9uYR zZyj6~Y_2Rn`KF&5FqQv&SlCKM5J4VD92r%;`qdn~pfR~+>ufh@JzPRyx_M-DTiG$u ze9H}p{%jO~bDKe6XqlO|kyd8rI(?IRxlYzBnKBLWb0D*8OEVw9+Dg{7d@2kd!KlQ6 z9)^l$yM^zuqapiDgz4DY3Y`~PwT=n3RsDVo=Rtj zyeEkUWgT$ZDlHl7As>9(@)%O%d)&b3)HI|mP+RF>T+l>wpCo>?Mo+mW8Lu+NI;dp@ z)Lp>$#cKpRQFy9oy_mpr_pU3Hq_Ddb?)>!_ebQP^3c8gh1!-SS&*jEOifTYr1Fu62 zmP8A=yzeG}K2MaO?bDSMfz!udNQ4M9Tdf zGvqCNwN}Z+Mo&tQ#NtwB>tU2d@BH^81)BHW*zlk841HoUS30FEb6=zpHV zGATcd6)j#kC&h9_FHRwB4cv$3J*arsn3Fw!UVlA3$Fb}DmSz#F5hdobnMR@%98&PN zRDdkaESUl_VdDX+72(YhSQIb>03-FYuEn?aVLbODSj*cx?UP^Hhw)C*gdfK zu{>X`S(E1#fElS^!K085>O9&i&81FPE)+ADk~lO zWL!>YxaV=2lLH7c+2h-O+}M)T(GN#o>pa1F&nKsqzz=;U^S~Zb6h}9MoY8Od9ye$V z`*mAtIXGKlrrLBBy?Os(m&EN3<~y{|&li0@CHxUHL}5?N59^Ke!1rfA88IJc&0z2l zzdVnOj`kM~V8+3pz+EtvKE@Aya?O$#MnANXaJ_Wg+bdxGa~P6Z-iw%t=x)AZ@IK37 z`O-mDR{Pm3fD%@q{%`!1D&6M`VO0)`3s0?j6mL^g2) zaDdTlWo*abC-!Hj)=>!u{)ciZ@f6z;*z6A9~2N>GbrBYt_WsoI!K!Y$$8Eg^qaeyW{QbPPj zuxR~V6q@u-Fhg+1ed{;vzF#KyFL+%uj;GX3hF709bOVmxHy?{*9qU;%v=^^)Q4iSA zD2BKEJJ2fV-dLe&R?^GMVf>h)PVy&863x-bK$~D;;M8w&!}Vhm{6}sJNTLE_A&1R) z0xw6;k_`(V?~$~)oI&HJ9i)kChQrna9?5?wj<{JMwihT@=x zLv+zfoUznv>E`xsN&4_1t|9f6*!0y7`jPlnses3sKD^g5rTi6~I`wE5v^Ia%hJPYwNWSj$F{?rHA`UC^JAH0Ca#g60hQO8sb65LPh4t;&oGNk7Jk4R6%bzHMS|{ z`w?+Xg(jUHOBgM=!h#-N@;01X+)o^L7~BaM6R7<-dHKM^VeYTAso9;u1mnQW59gWD zK-HsWR1yOoA<>3MB$Q#AJaNGY2=5>xUOPh)_V+jWhrt8ZAz5HtQf8*NKZR=V(NQQ4 z(G!TLnZ(IN2ffJQTOza+B|G zGGzJ1qP)@F(76(@qWD?DWpSw?J8T!r(j^}yijD2vhAe&0zG^g83n;a;dd6^bF~g{@ zjfEX=jtgJG5jErtOvk$rKPaZZ0W)2R7>*f})UXhl--eRg5R;a&*p1pZ<*GENq2RR= zZac9cTP=R+QjcB8E=7PrX`(pZ2o~Wgj3`l~do->UbL#%s2#X%cqwLz^2fFb8bX_UQj7Y%H$AJur2xJ;_id~nzsXw?n zhCr@HnI)`R9hOVE;X~O{&v|zyTTr`0rErs2;>{of9P;Dv*o(6tVha9Coe9F%C*!GQ zeH#senjO*ano-n5Vmu&RG1EnboDn_GbcY;GX-Br4G019KwU|iNAZRbv*|5);vIIJG z-{@MfRMsoYS^qb>_>UCn(Wtf)$x)z2J!zEBqbl2EogrA>TT)>FDAMih;(T!no(c1v-(y^2+xj#;sbp zdc1y0t#_=Sh8OTfnITW=La83MV7y8H_Zaf4q@?(Gr_gw?OGuU)%eS)I zJZKvj(-jp_%klt?IU$G(;`if4uc_Ae!lCSi!KjkaW=PAc#oVR$6Tf_aEnFx~62?62 z5;EKnRx)wcV)%E-Xle(6fJ>zPKNvKR;o@3r%5JC}L0^0oa`pCbjhTUk%&+!_bs_zM`>dEb%n^y4yKvqpPLIx_Ex z169m)$Qs_x4^fhw&zdoeaLA)A9nOpEcTqQ85ds_@)S0#0GpGHFU8!{o3Q3(EhA+yf z@gQ;B-ym;GBR5}^n|lWq*&FzDsjn-TJ^5ex3GMo4kE?A3 zXtKaac~EIX2_SndI0aHT$#8dK<;>bKZ_R4jL53P9^KAkuLPH$C=afdO zG0YipZTTt|eqRP;@9i z$%&_g?Y?X-Pii#tfq3sgE6^(3Jds(h1s;FzPk9*|KL zJJJ+q3ECNeJ-oCw**nC)O|0&bwfc4aKL+iLw}oQ^2z^~5;AGQD9=gaCWx_m31S~0i zG>>ypz3m)+)Eg9nCg^-Q@M1Lr|>s7! z*86bwF3#u81+F2e~Gli)hK;!FOcGUqxZ!4{{qy!kYgYnx_+FDjt z#UD2pl0-{I?Cx|?H|cEMYmtne42N6`q}p;57p( zGK=4A*g;)4dUQ$bx;AOw@yikeB5V)&sn*lPYPUw zDFD>o8%3jW>yvqPEB;j4AN*1%I;Z{g#XfQ?|`R8qmtEHA}ZuP>sQ_fw-b^egLNKKPALE*WxFH3 zqLd)4nKE8#&`<$iHNoh;{PwwjU9CaOaoFZX&X&6Ppgv}9B zM~*=ZLd=R9&^)O7KQj-~_N$|v{$zLHP2%T-|4z(TCYluQ(*roZKR-|Xw$OMp_O2&N z{j+%$-arXQc+DnQ24PB5+PLd_D=mR%?`SaH5ta)P zec$3TY|5xY$*>Fwyr1nvl-4Eyr$h(@uy>!?D1(XzLXw3lik=aQ z@{F_hAL8c9)=;^V2@fyIr1bjN7v+20wJ}IB7O?irt`Kvt^xMC{I&pM&0tZy}kF(jI zh3e5Msn`%jD6iLeeA_{_^Ox*@Ps?f+*MQ?44W%lSK@4uy{gTL$wSSDKdbnz!+eS(1 zLa@9+UqIiRF*f|-qE?VzU-Vf+u(s8YlNUM3>E@nyGn6#G|3lMRM@990ZTym=qO>3& z5+k8>N+S$i5<^LdG^2nZARrAA64KHj9Rm_WNlJ-ygERs|cjtS)zqQ`A^bc8s40rB5 zXP>>F=krLNA|T?OUQvu##4l%{J_J|#xjrBd^|XTZ7WPWszQGIiuw?t>0`?>Y)KhuG z3~Sk|4SCIFS_lMrbIRW>7u7GnJ%q$(sYaH8T`*x>I<*P780SF{E0Ni2#fi6;Lw6^D zj)v?&Cn=$@(80@#E~wR%!<$-=b2Y`^uKJ4slJ6OkivKm%cpNKi$Vl-UI`)5{M3_ue?5H z5v3dr*KUWqlpT-Z{La6;#d&$V2`w%_XD4fR+*N)5I?7;Evg_V5PecF*_HR)e4-qz8 zNkx+ex2moLhjXIcY~t@9b>GX0K~m8$sy<4g76^g@)&!ebucCq$9f}>+Nr+zId<$3r z!X$iku|3>2)6={^Fr3CjR+bcZLJ$iU!y^~+ZSXbsfC17XjARBU6;sO@Dh=rDAqqG? zQR!V+FFr8=tQ_rqK;$!Px&`G9uZ@)2pyC2{FRmJaDHya2gB6&*+kM{tx9gcVoT*ck z1E}?2yWR>qTkI1i}S%M#4l)HjmM zkaud@GB_7bs75N-vw)};Y%H+b?LM4RoXyj=Xu`;VFhYpROyy0O;y2-_@gaTz&^Ur+ z^^~5w0#8lXK|Q`pu#d5Mgjoh8 zck5l)?ZYbIHLe^h6zh+3QfmozeA#1Y_33W2D4m)HGIzI^z`SNW(zyXd9>yKb zruHkBp5!GE=UZ}9jnET8%meypc}Xh5j%H&>65msC0O`dA5Zi{4NRZBqaVt3x8}Ac# z>;sP&F@2mIk8Lc0y7GEY;un@&H=?-poI zR`(Z}v_0S2_pF|>i24|Qw4J3nz|-LIUZVcQc*pZYdZYbB*)_;dqlr3l7rC2{c+&LZRd7_>OTOr<$%770XRYRDM z!dJ(Z@t>?mH$Z><%TVUWE$sD{z1?!lz*4oDs+-{tm9FEUi~BH9Bl-053`r&K-cLa1 z!&>}=fwnY_YFgr;SN?u?O7}Ur?lzP%{ZdtV{ZyZ3at-H#`VMC?+ANdX=Y7A%dcoF) zs|iN1zkac@beWv+VanNGnVYz}Rx;A39ed1Ak8~vq^-CL$793c+IGyoN{)=;uwd}g( z#w4?=n#?~pc&70y8xALYE}*C?<@#3G&PYmPWqi3m$@Dai6f@>@oitk)FmD!q!QQRF zs8J^L3W2!ij=hRNJfsTjM!vLK$!70{;qRRa?0DYW#l9?O3-+>P#`4@81S|e6{}!tG zPCBo=;X$xg6h?x~4xs50AX#(yiIS;o`JF499amHsttq~hG8~=B2@z%K3=R>5h&{Nn zndJ(cw7mZ=%54PMkedSERTxWu9*VZ;j&~;Nk}=cb+K_qai(^J8xz|Pp0xk5}+B>M! z;nRnImxHAbj)0+m_LFe$DzH)1hq-J<>O?;k~2Q3WneGTqzs@6z3#p((w9 zvcgBR9WD!2gv5|VQ#J`dHL`>*R}n<7{iO$42_Niy<53+J5q)mn|K`lkspJsTd$VzG z-H-6Y%|id$RnQ4TRM77t!i6`TJpwf{1 zVSWcZu``+KNRDK+&-C@unUX(wa<{QrMnE(m`{WVS3^t0isgGt9@9KOK-#@1vOO`%+ zD)sO?8Jq<#IV>zWabr6QYl(sn__-`Cd%0;<4kUPrs@~GVl;{VWo3EG{Biy!lCffdP zV!c+|m^3p+GOMFWJ6}(uX@bgj4;7s?MQ(%0ZVGEU{I!clZWeI z>GAg2zx}^6JJ{jRT&0q}pK)vzW&Du;kt`W3MlDKt40r4_Gl_WNS=%9nBw279Q|r&2 z)2uS()TF%IsTldb6SS)SI9=oX>ktd8obaZv-J0zW*zo(IH%9jpQYAcouOELRu}#>4 z(kVLTXK~orSVyJ*;S@6d{Yzj3QqSn+FUj+=&vzftqy6XbiI5rIHd|US-Z3J1*(<9j z?Hf~blq-@MTZ!efKO5=mKJR{ygbgLCpImZD8Ebcr0dQimubvOEVWN>b*{0nBv2u8&?+3Ny*{o6(PYx4wb>I7AyP# z^IAKe)CYUB9%uTC4eEiVLBv%-8n=zEM0--6V}_o;u+L#qBn8or9_i09ngphwc0B*? zoM=%6{v}f+4ItUdXx&j@HOBEdo<-6Nja~%hM@v0Z>^8sM&9yc|%rd}{SMJJOB_01M z#YxL)3u3vrt+1^&{Z%1_5b~+H1&{els=V{u;ivoIM0K8c35BZZdYaQ1&BK@f%w|fz zwX&$GoC{#4%WLoT|2=${>f`Cm#qK?P*DGFht$Pe}scI%@Qn%B;(DoWCg4}y>)ZOze zalYo&t<>4%8K_BT=WdjF&?L+iiwN}w)UJFI%#j!Rm1O#nM-d-Y7@GY_>zp@V<8~k; zqd>Cp-mmz^-ALk*Bs@{#qX_M-kKKkFK@wv;rI+pSbSDYEyq**}DJ~xgl2yDV7T*TQ zi|N9Pa5s7KY)?+AF~Nx~hZKb_D0~WR6{trS9#rqoZ$mI8w&ez)p5m0ETo1{_4+O1Q zno0rTpz-=eliE_h1MAW)$K9otLaU+CAr4}3vTs|A@ZH-`W%<6~pt2sR@p#?I59pE#Pt_Bhf0zvq)8fs40wuwA`dA}R`4(bd4(AhFzEQswaa9>^^XG9T-^rhJPUf^!WThO)GYJX)Qx0G2 z_Q|?${d82+HM?@-1e!k#5P9j$-`C)#wf{YRe`V@P!FukLRgKRsQiiYlcK^8L42DH^Tvw;<{6K^Mob!d-2Q58r_*p*Y+pE`FdXtBE*rc1dWAYySIKu5o+N?||3Jcv zH!N_P9A~!`y^=C)8(@W`zWvJ@K0=I&mmyGms|bUezd@(Bd3pTmNnTMTmXQyBlr{7S z3d@yD!tma{r|egIwvxQillZRJpC+Q5UAVhEys8MC*^CIzH|I&3vd|m~tPq56Q1#g3 zbmj*Z+)li`wWv(EY+3xcYuBh}^|MiFb90V_=e6fy@tHkFm7hM5VqvAhWTTIwGsZ*x z(`T00@i+Vwlf)!QN@kz;d=x%+3DrM-7A7-#>L+EWoqTp4T-cSM=Q{ku_m1tnXiKV9`xM&Zu`?n}8tFu>{ITD3;8+?OK>KwMoC?xj_ zhET_W+~X>TQO)g9e7~Y3e~|`1A8RstRwm<5#1yx?+QcAd?90gb=wee~sU%h@>BlA9 zPe^X-uX)+-OV%9v0EomdXyr3Zk@Q2KY0)S)_1d8m0Tv`z;+*Wk&Sz#B1^v&C(O|su zeeUk0UZ2&NXVD&1x7EyXeLgc45P(hZKYo&aZsX+WjL4|7*?Nx>NEi2bP&f0AFZZH6 zfr7FX4ip4r&4~b&DR!StlnxlqUFiys1Bd zMvlwAO9vP#q!tm;{F{))uJA0Uk~I1xX+b+LFJ=T&r(&5$-OsBp_8*y8rvQ!J>Tb9^pUSj2_RTsE zZym<$$RbM??COp_m$m(Wbsfv975*`@JncubZBuG4y<>kiF;&I zcB`7<_-OD(^CWaluvcNgu;%o46jMUnbn<9YmZ@7#=MbTJ+%GsbrUUkp>_{(t!gayM z^lr@0FeVfwV^wx6DJ;(|HJ`oV*!jnDfc8l6WF~HfOvvAZ4nawKDwS)fW&VpqF`et> z(q6N_vALR7@$2@6FeWh~;&CS(M|?eeb}Le7V60M<`grDbbgB@w zxNAel@ex$mfGAq%iYvS43qcxg5oR9d(a(k6F}@pq!=yf|9hy@0KHJ)WEd73#$xq%6 z!w=rJ%pZp`igai8#or!PJ%57@&D&lNZZ@1;MG|j)V^Q!tf{`@yMSeLX66X{xBO_+b zaht}KdvS10)A>P8@#;yxghJ}^yWpM-UtfZ+ zJZ?6HBP|R?=btE-@}*+HjE1x}(*RjkSQxd^sMO?G6oIq^NbSvf1sRNN$ltphH4mXn z&5V7Lj{Pp;eU^}0c}h(mLU%8fXp;@TgyBK|D87d^>;=ES4`m4S?F`v^sr$`%Qj3ni z84}58rjt@|u^&TMMrFK=GuSw%CRLC)7vpZON%Mc(6V6kg`0}ziTS8d_)iw8Zqo`$$ zcwCHPRAgiEyKvrP7OYrJrMObj!=`=1x`N|wq#T7>vgFSbj6=4cJa}Ulz!x*NKW*?WOzu z>ZNO{JEba3Y?|@j>Mb36?6&Jk(lH#IPZJj$iY@YoDvMadZHIznjo7ojyIdPM3xV2n zz{5laNeY}SsctQHone+vD(bIw-MUu#k`jHRlyRqHQzabB^E4DkC_Y~jas>y5y*NdMJ^!Wz10Ls|Njrt}jR$3sQZUR?XI7q|@toNft^Ej6B15DZ|ENiLw4YN6(cM0X$4 zxZkDNpXs1DUumA9oIUhM!ip;B8$D}Q>^9>!&L8WH>%#B~nlyZ`zLA#_x3J~lp)`ue zv&uiQQk~3R*6$J~5$I@;18{+mT}q})2m|+JwsOX;#E{M*LX1qy3CLb% zlJjXU$RYbh%G3`jZ;au5E#nSc88a@X!OC}3h>tj-24$h=5eE51>Yelx6!Gk#V1(G!9v z+BQjr`Eq$A8trVjIdZmMp@|emO&fLVZntKCc<$V*aC2DGo%hv>47H9%$5)P_F9k{7 zYmn1Q&#UFNK6~~I7=G8Sh)u$`L>9R^CoV6(5f4M(ZE$OdU-e5OJ!I(bI-){U$TRhhkWsvv-$R)rl)rztOcU+5wjiu*clP_ zanu$)0#sNc7~2?PpFIic<`o)R{v9UO@%$CmuBA^k!A2_SAvrm{q9R7Rn~pWVw7%B9 z0n)9Rl9*cU%@~6rfI)rUg_szUvtb$|rB4#HBBZSveSBdHeKZi~BK{G!|3pz!cZ;;* z0~-XnY)=cno8Ac}?Pr$(0E~>|ojDWTjW^8X3}*(r3WZJrykmn5xHD1@VIPfx2gF-roa3F`xCPoQqBR-phuh21BtAJ|!%( z*_e-Yp9#&n$E-6~KMg0ur>eBn=JxxHw#0`GgvLqBp>9L^;-9wv>7Bph;ipHge9@KM zkxz=yem`3kf9q(L28DL%v%#cPjTQ2%f=+0hMM3EIm!LOk%T2}VyY%IIGl=#mvn?f? zUfQsi^%LD74ZxpK1$}+w0hs@GY5tCO3YMSJ)>7g@tH! zI)_i@PLQ-HGxXRCqaX243MNK>-}uIA0{8{W;u{_}W2td?Z@9A3CMAzG%S|=*!1w9g zQQBU#v1||FQKiZ>9@1ReGKbscO%$;}*&FO^CC|Mc6YRa*a!@j>KUn=^=7vP`M01AYhsVUEfH;y#Gm@|(a~5mrAp$5(HHG69Yk z@Xv7Phw|c|;JwbHc7#|=eDs-va6&=@GJ2EzzmHOdSo&rvjO?qMTo#fGr_!&6YM2Cr z^;p~rrsV_kN;pKaRP#WsEz3BgqR<#MU0u8$W~V{f5-F<@*1P{_rN@Ja0rx(`52DuL z;q;?@>3^3_=CpUH8(dK6#Z^+~o>K*-`rj4$Un6_PO7zPHY3km_!xW*gZqJp`D{mPo zb-P{-D7g~L)&9Tch$bsbC&l_*c#<|DMYNn-GR$^ zr%#x-BkaXq2NeLSjhMHVQtDbwl!^%ol?g3;G)=XAjqPVS8gWOj&;>=II4ZG@jy&J0 z8Sy6Uzc==nb2h9Mzs+IFcjs>ZUuU1-N}gP`^;r)bCXTmz=_L$jFvSnF8XEpBQvH5Q z%g$p;+sO#uKS7F(c4AH1-<(J37L@M~OpUbJX`cuyu|0fTjN;E3PlI*oX;QKpe~k=3 zoct&JPG=DV%;9@5Y{$j6kn;@%g<|oFa31n4ZT%3Fs;9~rwVMQ0k=&v(HR6-V0&7$1 z1=Hv|ngir(7fRBU{6$^z!XQk0&UxI3(o$+%k)7tzyJYhgA%;^h;tJqqA+Fafw7Y2! zFlKS3N?f&`n3~a=@tPsxvuiNO3-CIe-eEbB*b|0!dp5sK@>SR$PWX={RgP&RD3;y& zK&SlV;;3O2$mJaAQEVii)tX6bdjRdnRrV&8IZm2@f5#%^7_3d5)100m1Wci^@ zPmz|cdl=1a!9v8N#Jr%XSeUeXpEW0)Y{%?q8DQTR*6Pf>gN9HTg;HuBw@Cxr=?P&yo3rh4K0l>fIE;j2zN>Pkxo5xp}t4_*; z()wkN*S*se#ZylL4SFT5BphxYxAn%18$@0`8?8H$&_nv81!0QP21vExSfFhIurJ<@ zT?Ccag)~o}%VOdK%A-lHYyU3_AGC^G!f};I*kEyC=NrKq2h>pmucdPQ&xR5sGxB=l z#8W9y=H5qjl$Qhi3UpBPN`IWDC22HeeEs3nm+vnjnw@H#;?(KnxVEX;KchC&(qJub_~-|f>%_2+dt3t6Me_NX>0z=KmTt5X!%Cp^04 z!bMtW^K0*wAzJ+&k^_kn?&eh*j*W(8iuD7EVDu76jK|kbx09$F1^&welvoMZ2|b-x z$p>|@`;Z!P3#*xoz{WbK z`(Q&(0>LB`jYY5A->3BUxJw<@mKxvux(UaWV+=bSjf`Wri?6=)-}q_%!I3g55Q_N; zJNg*Ou!geFHb{S>b;qS1g{*kkgw-Z5&HHs|Q@j8EqkR6=K91^U> zOjyOAgj*Nhyr;>aG)g6%AK%R+x$`SA-7ME>>V1!iT1#{L+2!hv4eAk8Gcku+Ff|K{ zOlAj@wf%kGCyLTVMMVSo%(bJod%ifgN=_SjQKk2}CH@Ku3FQH7pCWZCEJU!w8e^C` zg6EfDD?V!#O)R}=>^L)iAaGDxKV&xJfLk);5phF%e;Q(@|EQ1oi0a0F8f&4b82vIS zw=&B1s*tsJtbHsBvp5`i^q1w~K6Y0Tn!yb%CRWf-C{g{S(|xcE=QR026Iq(~yiQq0 zY+=J$iws-~5eKvs{1;mQFL-s#oLDkxKgZ6S$~uJ-=;rMCm_sg9bZi;va5c!b5eKPvgjNj0o`?swmHhKT(Lr%-p@I2S6N*tPn1Nd<8zyc9VDL)B+A30 zXw1Z*=VoD6mgzv1!BdQGp^_=LSwC_IJe=F}Lxo30Wp3~FLp-Tzn=%WHWQ@=i5rQ$& z*+}Vq5$Sy;JRM>wB(HkP1?_P+Sxo8ACz%7<)pNU+v!ljRaI-MQBv_qglaaf52i3c< z!CtQmcXJV+$wdJgRh^gsF65S;`bTO$V?r8ha^K+J!+&y_UEm)6pU;eJ#VTR0QNQ2n zY)Qk(NsaisUiRvI7Q2e0n}aQ}jJ7VhD@p1ogaDZp3QeBF+eIZa8@c`75$El-^0yP+ z?#P=3$FqeU&b1}c#F@Qk;>TR$uXF1&hJc#0 z#g^C2*j@d-z3-GwJV8`EdMprj)Ya$?TN)b{;;Chko=0r)KQs1fef6T?Z3oX=_tl)) zpiOa;^RM)b#N&D;Hj_1^QR>k!U>dj3*NnGd=yw8QvdXdPwGXUSKLoW=CV>k=TvcjV zWKr^6Mv+gQsYup>6Ez;%lCH@q)?;-&D}J28ozc?lW8U~-C2L;VyE~$mlergHfmB+Z~c;@M0k4pf9OLkKOir6PEcu)dMvlJ}meyBn3PxsiLm? zsOnjfM3s)lrj$na820KPKYT!O4j6uw8F@sS|C zTQC3Zt}M+L^lscq*u-UiQgHvJiGn$~d51)dhvEy-@={h~*VXhO;%NP=W1EAmD5@+2 zR6M}SE1hpeXD{LZ(7$r=xjRsH7?4M@3cT3Tln+kuu#FsW&vL6oi~pY8n;_(F~;`sqh&vw)^;cf5y7ca&21Bbo&StZZL4z}&Ra?&N= zYa+L#2>`2y;SD&=r#O}ONd!oh)n)5xjID-hM?p+f*Ui2-m!E~|7s|K2kw>FMfREbi z2By#XsZO?8p3cEu$IA=JO>xH`jO!Jciw`a5goR}1EgEhw4Em~RVbh}@UBTsIA4 zmSxZD`sgtOvunw(KY3hEiI#9jRpq%|!!X`&nyBv6*D-KiMBIbt#&B=uR}ae>LNSfC zL3b$0NLh*iOicz5f^z-!Y zEY77xfkp@($UvrF$o%(QhYI(4Rd;mM876@I>(81+VFu2e~!@a*k| z(kK=)6;Ouncq$B!cq`C2Z?=t{)+m5-JZR}8JXF}0hkr(1l^AsGG(?-t0jb>grlTb9<#hCcL9nQ8qP>0a z7*&pT1C2fNN%--U&{Jc++KN=z09M!%jRl7NB@l+78x|`iE(jvL5BZYCJ-;R)O(=?7 zqS|QrCP~_u0x|&GXH-JDu)6DOlP2R#<s05l> z*cz*JhuZum9CmM`P7>1 zM#EnGWW)?J>!0p^I&84PbLtt*M;hXkS@_gedN);#h2XB&BZ6yNbmP7E?NzAf<%+Zy z#KfT4`;hgo10yf=k06?;n84Qu>)Q)9nc%S3RM5T56Q(Q|Y$<$m83N&>UL5sVGLu_a zP|S(vHsv30_Y1BT!Ef|GG&pYll%C$c2ugRq3t0ExB11?>ZbNz>3eaPQ2ns8GX6jMU zFamx()^1W4fH4M`EgB9jChBaC05(d=#ka}h0OR&R;pJ;H%(SfM@o7C{A?bfMZCs{x z8G?Gp`^}!Wn`i6wk$H%d<=fj{ky`5FzD$qT41(qiin5wMd@W23ejd;as-T}UIwa>E zR~IMaKQQi9HAvJbzF+41gR~l+!L{MMQ4nEdZDAqn{L@Hjm>lBN`=^7zvq_TH%9}P& zp7jV-vVPHL!j@xdPDvY_Uv=N*aLKGC)h#9Xx^2GCXw1;#_j({Dt91he`sO_c?)b8+ zBp8$YUw2Jy>!FYrer^B!Mu+!oouAu)nmxLzm(dk@#Ou z%CloWt3Ht4a0j&NFgiuDiqX5~=vnP#WJk{7D2uFhTPS+ew%~u7H?dK)W?`E0EvU6e z@!tjfn#06nDzaQaRLH4){ElJoPOrqr%@fm+6)L74EU7Ev?;OxajG@ACY%w|(BYbq> z*;gKxHFu66xVDMlVCpC7eba@+_c!|`AOMrhnY&LIC*rkI`rOqm;4@eWHfz21L*%_k zaNZGN6~t|F8K3wGwFJ_6-0M}3e$6O48~jl<4dY(aj)Vkft;Vy)@Pmkdd(6>#W=S=u zzZ(ke(%8^(JlNRti;^`$DLc02-=zn8)`=Jcy51T7o*|!fMp$ zzP;B`!R3|Y0GH&2jO_CxJ9Ug?+e>l6sWze7&DZpc`vG^K$v+i2+qhbEY$Jy5rfDSHS}C3=B)qS3r?hDgcWjB(ef|ev}@bpRUqFGnHPybh&Ra zZb$o%=gw!u=IVI;Pn8MSXS9w1$K$bSY)|LPXeQ5ldgL_iyO`|R5B5LFA6$-3)J?>; zN!*KWT1`YM(8+%VhrN4423Iau+Sk<%j?P_F|5BZ1skC-jk0{eVy_Bpx6rIA;8QSja zF0!vVOO_!x+NP%VJhp5S5BR~cC@?ID-K#%inJ(UUpou`xE(;=s*eAn@u9&rml`nk1Y&+R@7pAGTrL8b zurX= zU5kjvX`z8D#YtAI6r1F3jy8$a@Lk5I!TInuUe#e~q*0qd0dd)oK>{$M!aqRse@%83$r}cpv ztLDICV`;A1g`(E$K<|2ioxWIl$2FG69xTV6k%rRW+H;V4!&Z(?}T5kGl zcq+AS(Glv)v(Jl91PQyI$*Csc+P&=Bj>?968Nn<{h;4s9`P1$ z++TpqR+##%#~VvhXHJv=kJIjl6>_cj4>=XT zdI(AN2@e=J{hV20hDp|1g27O`9>u(6%RbEI_;PAd-RMsEzH!ErDa`xI7${jDVPs_Ti)`YEqJ*jH6ltCE8F}4 zg8Xb-Wn=I+scNKg`{ACS2ds|87YF1CpQ$WIV;1xmuQl71m3t6a&=FP63Ek@tnoA8q z!K7uHp_OCAow&#+ZNap7JL1Yk1SFoH?&2_>e*<#4mk2~36_`l6X(SxX0s*46vvb_k z*73x29qcGkca7S-cIAX-tLRw{09(p60>r!8wgwH;paG4g+ArTgoa?h&v$%Jv?Qm-! z627K0JolcT=;C@Y?Lcj2n8Lk_K!BFuy4w-IswdD0OB3kFYouW)k48mP`$ihUA`Dz) z!=x9*6H-l&Zu{oUmE42K*zW%zzdnwN{7ekV9X0uBl;$0u-e<_rR7yOVIeB*Y&cvC+ zb;$pfrv#(1nR-d1EQ(zHq1l9oI`_KK7a`YoQY0Y=DIjykt2E#M)qCAf|9A)DTY^?)aZW$AGP!B--9CnA3m{@&WwjU(3v{mMb37f*}NWRK8+rLD%PBIXmbkf%b6NDFB&;?$_QSiF4wlGSgQ14G6g>5^xI% zI6OS~X@Jj&!|xclI{e6rAuS7=YU_Tm5yff9KL)WgZd`~iasRd098YHY%4gcLR34(c zXU4hgxfzaVJckVWF51N>0Z~m1xT-ozT`TFp7V$h@?iUsVBWPN`gvBFy`&7o0E@d@v zktl#+|GQQ7EYvR{A%RVG7~BQmwpUpPC+4)|WG3JF$Dejz7#kV}*o>YRBW1>{8ydm= z05)K>4qMKD3}GY+s~LpJMgGC|*_$0liK%I?o19Homk(|UM3`yGq;5SfJNdMR^L)L? z1Rf949=6N6D}xS4r?x=aaP+SQ&_f06T@(9Ctdir=^zDg}nFVbHx-re1VKL9fR432P zvJ+=%R@uRB1JPXGCkJuRy!P7NgK?rpGS3Nq-#D}%$~fQHW0gg(EHF>89^W#*R8=Vx z8#=u3ObhszTw=}`_*AiRC&Dw<7eBeylE8Xp^PmxDF^scKM@~zPFMz&c3+(p=E7kEH zX~mP4$J2R7Qy^UV_G{d3K+(=qPhWv4){JjxXppxEQ|^o9=@e0jq((&k`5-~soU~j2 zEc90kL3}B3nbL4&s6+i-29O+(XJg>aab=kkds!T2LK&=gl9i*&b>;5H?KF7lk)s_2 zQ%r;@+JwD|1JL|}OnWGwIjz)I!Zn~@8D1Q#ne*d%dE%R})ruh-qIFZLV93LSM56%B zSs9`>+Hr3cwcpS5gyE1AvnLc;o-5PkY zMn#rJ^M+q_yb26$K_SNYaB8y%2l|a!v^BX}i&PErw0v?hSk%5WyIO6+KX+ecWpm!{ zXufuNrQTdSy3j(@OftWb{^;K`mZK~6YfAdr_*uq&3!#M4+O40tA>+S;K7ulde)cQu z3<}e|RCSwFd@doK!@pRJS1|prsgZ!c#;Rgm#T0W)ZvROF`c18Rl=gskrt+Rf^%Q~u z*AVQ+viZqz^W$r!V^=PU_rHAk0!s$TZ>t4)X^d+>h)gUjO!-s1MdPTg zFk^Job3iPDb#=n@6|oOzm3JC!C1N!#2r>_6br}LycK*oOyRXX#-s)}Ry6y2s>t)l} z60%z^yR3^fIA0|?J6hhUg0vPFyne)hk|AKI{iPCuICH_}r;#m68FFw-`?=ttSDN~j zyr}RF0uku)^U?WLV?Op67>s2kj&S7|G?9}e>9279rkQNV1fqKX1};Ww%{h4*fP<<_IUH?Aqu3sL0PU%An(luM5B0Z-l2!(eCIDK) z?8<&dCMtQb)EZN09OKmT&oLEb<*0dYW=0moV0LChosu3@v>}-#f7hrk3iO7;S4x~) z9r+`S1DQo7jzu@J`!dG+xLZw(S`uE(ZH&b@~Nc>A<4Y1^JqNKPQ%{rDf!W{_zB6OBa*@R3kHiD>rf4W{O&1ca` z$7P^La%3-+WzUiuCdtP0-5alBGp{Woz8t1{B{%XdaoS3;j}(h6C4cs0{Bi$5N>X&{ z`ye&!ZlO%Z8v4<-$}!G{i`lv6gERkE&cE4gs*@^r3oA5`8BUY!fE~O6;)FmLg`K1X*{-3=Wlm9O&m%b;w|DGWQg^hr? zK91@gs5O1|R0ngkcQ&-QKdlaA7GyagxHTBN`?t(T_ZTfvpWJgw7*MMl{V$Vd;AyIJ z!#kJN&h&G$qppAHwxI)3GRHN7oYZT0xRR#rPtAn~eIv&&5arW++*Luolfhr2f69#o z7we}=-s}ajNp$`&}04m{gLnJ zs5>c((G1ilr^_zL>nBgbLgf!5nY zDY~VFN|dsu+T@uw%pa@|N0%>l&nfFE3|?`SJn=0$8$84zx=c%Bl$Ie|;rwM3Y%aXO zIkLj3>pY)+=G*Ua(sWINr({2RS0$nu2qv*ubELlQlYguIF6pr2brYi*sQSzBX{gwe zTN-PQN>Z*O0-+cU3vuG)>CnTZj2gVMtXhcotgh9aKIF?7srt=Zm~%a6>AhcT651dW z6nxbCpreSMDITo(}g#q#g+XBeVmeZA1GBoD0vK=yn> zLRJ9k6a4Kg?tRApYXM-2Z@SAX!Ow-q@>bwMMX^elVcqNEj?DqfQc8c(3WHCFH}q5` z*gjGXlryU+bO}3H^8tCgyFH2~-9rDzShN#o@P>g?2kq+sLzUT&iz4r=t6UzKKfbv? zdwpDO()JC%2AaZ#ek;VD(EZm{MIbVrO4RP}|E#SQCYJ^~flJ+8hJ2Tw_uv6h8bo6T z50R~`>;64q;GY(e`yQ4Z&*L%y#pE|FTu@w%cln<=8^8CMUgQ_5{d;(FC51|Ie{I8Y zAqXV^mb5a$2V+0O0vr(tT!)tKW&>qFAcEt{{!Rx)ax@HV$Y#^t|#_G zJ*iYK|CFR2`F1HhvZ1>F_v^V&v!eWHhSgh zMOr!GIXO&k%vV)4{Ou6CQ$2dMu#mL#neWnulK7vrXw9eE*GnE%ZyJcB8$^c^E{XZ3 zYAnsf@Z7W!aj&%x0M=Iz8K=FCKokHK0oe6H^ijH`xAD$w!z&Ihu4EuY($Uo&9U6)T zqpOdAliSN8f4+n5aOffZ$qcxE~y5=o`9%| zNeVUuFG3&ypcJ4HOu^>`z!@6gIV~t@xaR z!ga<@!53Le?klAtr@tH=Fx4P5elq*D%kjU+1}zkMk(g|NoI)39w5ag8CMvA+8DHCK zdW*d2#!O(15tm}&JzeG6Ja28fpzY}$Z4z-_kNw-=Ayisi48XlPIz@O81n!x_JA@3Z zv@?5Ai5uRD53_1+bPzdV zJh%`5VPHWyHq?L0M>@U@_^fEFnVhOvmUu#gv*nW;IX|ut|Lt?=9m#_r2HekgD+Vc3 zX&C)9@9c|p*3<&nN=Ay)(Y^esEos2u5%)OWovg6hKtJmy9p-=Jp{BT9@wBdMNutO- z;pBzgTW|o!^BI&=AyozAmG*Z_t}%#DrQ@x{*zP-SrlwdS1kwb0h`6Nm^jk=dK;j=W zc4n8tWF&vG3ZK5Mp7KqMyJV-6WLDJdug|l28YdA%ymVrQ@VFGm4x1iWGJJ&^n=lZ@ zn3rQia&fgZHcMIrSe0WS>ad($AE^pSbx`fjIz_|CrRRZAv3zU@(6k^30J>fJc$yVB z)C!##7Z)59An3m#w)q>Jw>3()^q2~Snwn@ysA*N*M$Cn+zy0KP!oFBJj^(O3_P*7| zA*0aght)&be|ewIWAO!*jn9aA?Pmhj8T>j@66zYIcn`Tiu_+0V@%{|BH7|l;B@;*}$$p0rCxLB|cF_(h55cCUJ6dzR4T*U2q77Gkw^f zu5|*ii?X>LCX!6_gYNR!d&Jac+yNP}ngoyn9H?%C75FN!=R3(7Frx&zE3Oh8{4Qzo zDnvXboID5LoNWU>Vv+b}o!)@}Is%W^rO)?-ZkRt%tRFxinqPA_gCyzyqQFK+5sC&7 z^g7J9uyDYG2wVe`{pf^d(DvEAzSt=>soL|YZo1k!J+5wgl$eO;p8h~Sg4UNwKBAds zb{GG@_fLqA^Yw&5Rm*KhZkpDYyozqEw-Kb$aXa&XXzFD!hsZxb%PPgz%$TtD1lCAS;j)ec!-kzJsfvOoR_aN z9G{qkj3m~g%Tbkyk;*I|;FuF%As>?9FiPhQ--fpVIYF)r6!GK!$k{v=UlHv7_kglGd4u~5i|>q|Ev+fh#w6V9E#<$x}|R*B%) zDN~m-s=ejd$m+e*^7sm!mqa`P!$F+4%4z_xu-#^C_(z&oNHPtVHNVK zJ-L(hWbX&Df2#h`mg#=tx$sxNA}5W9YroiJknw-V{xA?hfELQo&`?{`nf`m%fgz0+0 z{CL2;zx3>@09mlm_q($OG=IurYd^p61O{8Dh2ojP*m$bB?w1hMcozfskmvom> z(lK;OcMsj&-F4sZckg{3`AeQ*&N=VdvG&?)jm1rk06FQ0U1tj98XM3_9E{E;rI1o! zp-Evd8EYmn_Yp`yqhkEzCtnw9Tm~oWKDU~G^esgrcj6QmX*${5U=@DU2G)}!ktRQ0 zsQrzfx2vCzV}I3qDo88ykJ|GITeLinlcMvSZI`6SKXB!Z){DaZ3!zvnU%T=qKu z0KMYc&oE2ugSl!Nx9yVPs;doYjf42~+KNBfpKQk&{P6zfY)8;ufV8Silor^4NRnv( zz|avjXPA|%TcUo-o#wj3P=!ETqyl={A0;nW=twnA%xtKf>=9&jvieTG*#26VyW#|R z{u-oyp_b5#-uL^04#D%vo!RGhs-M5P4eWml0XtF-v?Cxwtv-GlXlDuXunxr9mYt_lb%igDue^_1VbFDxyyhI^`E=D z;`#$E^~hkCI-^pc&vibLJMTuD55&_|RiFA?X1OVSpH>K%x4d0MnRPf6RjRGM-HJ%0 zSECG2USSDi=i+-#%>V}m(0F&Wnu@%y<7MOOlg86Y%ialHn7pPI&uEVRgTrQ3gT$7T zrgjNTgkOOYuomg3NpoZCmZbN#3Hu$7-ksdkJRi};K5qlX=5|TyBi;FEauc5L!>|y( zlTl#PK2YL0n@5sr>;(qLIk~8IVfWK@i?3vU@@6jzpYqbV?!Vs6gLi6>qC!4KH(q>b zf2IW+>gQkT)l}MipjED4tl?tHajx3O^qPyOd~{A5WL@oU#ca5IUCPu>{@Wg>5N;N# z3|SJ#nED2fu@48hM{qlbfeC5+8aM&{<%M+kK$gDu^d%^JnAFm0K%oPHfFptq>6bqW zq#4Dqj1d)?4nX%#LPuhgr2}u)+ke37<~d}zw>S6+1ndN8p$zi*ZOOft0J-I>r)OHK z{nX(l)x|RDfA8dnF``(N6xyd!7!+a{vhHh!ToF`$Nt#3b8bqja>#tmJ&#ya-a3pA( zf7j5p^z**NQHBk4l7NE1K%w8a)q8a#ggU>X>Tb`0-%;}WK78`u@oHBW9+1BT0qB#x z&}0bq5e@gadOA^NkjHsl*8=T8kpEAWZ+`}C=2y-S5FU>NRSfx@Y{|E;9#!wJdS%d# z@Lfx80T0%?=v;#K;$IfBUUV$^+B#YAVxHmb#CMbSD)l{x&CXUay(i^@&9R~z87=qM zstllpAR8rt8B-X;!6EXDF!USAc2sU)!rN>WG5HXlg$JCiKa0AY+SBEh#26Pv}y#QQTZ}t12;rKqPF^oK@%c}0{JPC;Cbca{JF&KL16lCZO`Q5 z*=g7cR}ZDv#XDXHU$Z7^9?2gXt%hyI&_0g*IUr*^F7E=8!R8>6{M;N_>Dp(5$j?`j z%KCA}YccD!-=wn>TPk<1;9!&Tfr`eY@^^m{d{yz`TSAm1V5t zIryM=^QrM9T14+>Z0?H7glc_5iA>a$nb*!w=Iut@z`T`#l#ncp1vie)VSP4$W0@DZ zu#xD4k{;BiI8^#`f}&8XWzXga5G4JO(Qyi&4$x#J#m!CT6YZvRrC){%9C!m>*5CE@ z^&4EUY6c>!`u?ctA{Y#QR{e?Js`6w&POtGVqbiZ4(CR_sWEmr9fWFbWW)n$qP)lXK zBs2WTfNJ~C=p=jPP4k7nr;w0qT(KZU69R$`@4JkKdWY^+RIjs-1`x}gkUsGr&v>J z4}s;(0$p(*S8xZx>J*S~atDi>fG%WFl>PVbPVGe=|MN$gS6wIwi&JbPVp=+E1DuosG90uPVm2{kGPiCd7tCMIA7@ zhv#F+0qHJ#hvTb#+DR!%q9OC~s(N0h)fVvY3WPJMSko97qG0f)^_^OV0J!4bbz^?< zlT13@6TX-c;=G+W`SchzEm9T>^N-w1AJV81XK0^FOz;A+6}2FN>w_skPXX8!&Aubf#q>J~7b)4)@klsO>3 z$Ff~j?)pU|9n%mG;sqdQ0{d+DwO`UpU@(R!*0Nh%uegz`3S`dy{*6IswJV?5@XCXA zKYVKLsHyvIG<8zL7}`@>nW&yM6bQh>WRh~s0gXnRo$c57I@Qp~9LD>Rf+zaeg&M`memN6!3d!XjR8IlEv+P1A!}%2iF91_;UrC;Lhx{VTr3Wi z8La4RB02{ntbRR7yA9i|DlmlOO@huzkF=*~36}bI3j8D!d?hqqT&E3P{qf&apMZIQ^$EX>yKJGZyb6Ng)6+?XUfGt~wiFHQ0bkgnThk zY`m=M5vI#3{L2UnE$bwi{RSVUm0^a^0(8(wGp;9v0e2@ctso67(&YV|)l;NLmh#x>#fODu>xK%n$F^N~XtrM*Y4X7BDA zbTu?u0HaBN?t31{kjZ50S}=;PY55c!neWi$NDUYvb$MWd%OR&pF^_~6tN>m`h5BqGtx+WzhL<}LwzmQxM0m069&aGq=DoOqCbaTiMSi#~wVPR!$0|c(J zx6hutK;THDm5x6c$g|`$c5l>AI@ZkgwWy(VN%a^6)ZJZwFtDk~7A6*C^z7S`tL1vh zAnz$eZWkx+b6=S;TFWZa^rnn{dVx>2ENC%4x6X+2c*#^HTt=8OwEypx1)0Uy#Ln7P zFJ0IpiDuV{xi+NVCJ%by~i{Ug(l z)&=p{%5d$Coa+8;)*HI)nDd2PS%#26O$;i-jnA;uZ$*|#Ir*P2ZA8af{P9K;?%qLY zeOp^_(0oCwJoq-dAKd<)(>d@!>w;N>#X!zeMEzXBBmITC+21s>Yz8Jzm&NF#1&F$hfJis;aOTMXRG4OM3>s zz}svN(f2DeGAC6MCRQx>f7K8Bo0b>%`gPC4=Tj#iPKpsCH@NmaeNB^jS?^Wb8}@)`nbq_RqbsBX$^@ zL+uRHX`eG*lfMFLvz>^&hM3(YS+Uf852(P&QhIQ0AMF`Sx*k=$6q-98#esEp7TXD5sOF-Lsyu z%v12UPSN ztXh9pXui$(@3jhCU~}hzTxn`m(IWir`Xt(G$>r+!ogOcW@dVf6w1VyhvX-fU7=}uI zu0#y~rizK;x*N4@UwOX)$BWEVzraE`cNs#9y1YLHOcl~LO#s?!Ry2Xok~soAi0GdC zwVvqjU=$`Ny9E2S1){S;Gf0kBU`8;GEBe+_%R%Q0}fWM>$M5qA0N zcln%TxFtu4mDJ#my5s5bfuTYK|5Ga3b)Hu@uaf$j3@XB18e8U4dl$U+)R+I6+RLA2 zUgP1D!7PE!zl5Jjc?piqS6>%Z^oK)h3v&aWJQ4T9h&#R9k|lc?%o@0e5PuaEAU@#D~16|9AcGWSE2x8RFb@cjaYZ6JgypDw?&?>?C}D<25Op zcK=0YO(yCO_$LvAubdMj8>^BC=ay_&^NZe<#-LId8-Gtbjr4wW+o4~d?L#O#e;JMsv zOKz(J_e;<_xjfqN`->>tR=v`c^o~93umv`;@WJeWh|@66cxpT|-U|tW^GZ-deP3ZY zO)dx!g~z(>V2Sk@nu-K2gkNC<`at{TYG=2Z?hEH*T_4{;AHTX%?e#9YSNJJoJn?UK z6Xr}gWlov6zH(;3D_O|Ez-}?lyVeQIcpf^xSm@~n)KR~F zmzyB;+W6~ea?p#g@vJjG0I&0d zOf*lp#S2|S9pS(Cl#(M)~1=o}Q-->X$uS1^&R_3d5dN0=cy_iLixeDui>uB zaz#Z26Cr=&{|@%|27Zsfz3;x1Y9x(Kgi9Jb%ef5oM8l<|8c0c%=57TqYh#1gQshRt zYM3?YWd5!4Zn)SiHn`ZUm#v8XrpWvB2vxOCp|IGJZ5G8tp-L6;tWB*%FCN!jNr?|- zUxzBlrJNEN7RvLyKS0YTDi156!16qMp(Zi8AdF{uT}i~`8SF!%xiw2Ob;ODtAo4&p zSX+uXF|ijrmEuzPgzx_~Cp@=sK6WF%GH(9;{G%sT1HZ>bARUd3GgRwhnu}b`f-T7?u?I?kgTrhR~NDlIvkO>Z|7Mfr^_7gRa7M~JcJn9(%@DV z%+e_>{fk*seY9^>u;Z3L`Hf3%Ut5`obY=GR&H5KjO;W=o_uJI^rtX~RFUrxPj z&o&`-r$+wE6t5n$>!L%-f-jfSu}9^Lm>qvF?TAw<#xJE$TGJ_))Ehrxv=))S^&9L6 z$FhHGf7y5Jf~1qCwnJnew7#)2VcwYU7|Ce-*)x}q$f082w=T>`2572DD+l{z7tgx; zQl{Mbf8R7Cmn&a&?pEDH~cwfYgXby_OQ6^)~oV%r6zj4`a~KRo*`LzV-6ZRgG{!o6RQD zYxWefe{&>1wscv`>X3fwZv3*#;(TXfPGQz?;+tw@jl3*FCE^Ri8^+jR5)u+T+m``8 zm=ajK=dQGVfxMffB8pvyR!*{zkKn2My~V~wDQR?-+_rrDT6uQBs`jI=TBhkFmz0^J z{}eya-t$v$CekEXXLgLHl7J7t(3Tgs)f_KOAl&q@W)Ks<56+&s?Cb06Ze|vkZQg7C zjobrq_sXOBY>=eS4C*oe{P8K%$R34Wj{d||;#QiDmx2MGSzCTRAEv)>^H&nG_&tCQ z2E(-mqBO$qP-glw%x-TyK8gsegd$&9y>WTG{h2U1tW$t{pd!0-+25k`GDVQ~;$G%fz;y7K_I;N_fs>gN;7O9Z6@3dCl? zWz*RGaB1l^IwT{i6p=(PLyeA(jtW6BPeS`j!p$iu{VvjOUZ5!oUPYT7%8ScLC2|Rm zUHW^86JXtJ4t3q!e`DJkKuhT&fLxX}#Y63!5n4jJ6yMaRiLf)2H?iHd-)B-|9ptFDk~bTr^ctui*y+`dUx&<~d~%gNn7So375j~^>{z#4WwrBl!7t}C z<8-aO*<9Z_(j9X+C(aZSacA|AvF@txr!>}!YbT2;2ZrPBiio4OPnTyq8X?>zJ(!Vo zi5?D2Jp#zd#5VK;KNczFc%-#p*pP3G9#;iu1&ccqH_B|pg~9DPdS5h~E>>f0`n111 zZKBO)uHPguE-RL_l<-^ZkKgx#nW}oSJ`ws&~8{4zClkN}O=OSEMp0_0tej>+- zBS$kLlvpJ-d~3U&ilsj9h7B>zTLV1BxY0SvTCibRb`3lR+^f?_8Aaa3pDt=X5|Zuk zZb9eXV2K~J+a*55_CTXhhzrsgcmw0voh*F#xe)4vq#r0H>~wUxBC$_9*yiW|-lK^Q zT6?}5zch5hOXJh1%{<;f7n~(8FYR8YSAKHn#Ce)jpMHnw^!M1IB;35VA7*wdT(enm z@#`1c_*ki7i0<=J=Kul6Tyu3KM!QIC6ZcRR9`v>1Bj5|8{o zh+R#rJt~HSX+Vxa?oSN*p^2<4=}yl5-wat968{F3d?Ru77?o-7xM+H%L9(r=eL1G1 z{+oNg&6GBP&S(|oK^1@SP$oq^ApjvGoEB+E|}*pAn-i zyR>K|cn#>H`Ra$jtA6U`E?(<>VwQMcO+uK&8*UmznA%~3S#pp({4uT=j`JsGfPBwK z|6`;1n6ztc)7~{0kO=ZMVM5|M{Bnj0n#)&0Q7^3MRg^clhW%O5ARWwdZ4~t)nE7dY zJ*_OiT@)62`g{Z`nRRH>eeqjf{+3dxmTE9)(Hy z@?mNp@VbkZi0TtcDx2_&XB_;+@zJL#kopa?#%-^A>`u^tyBE~f=!Zr;W8(GUSBO1* z^ha@!Y}_yaZw}Nlk$wr;bQujaYJ1=2Bz_)XTk1ObX&v?VKBTfto!|&Jw<9UVPz;l@~2p2R&uP`nrT&>_eyf zl^(q_r@QEE_J+{KbIwj97KiI(T30i9vgjW1YRy8A+!wo(47^N5xYsU+dYYb-hd9zD zkLIvzHrPyoR3Hfw#7BS>j`HURLd%p#dEG8imGL<@6x#k4Hq@+^8^w-lP65%XI4>(> zXX`9oUjCZl!}6KEWy24y>Hij~P?v|GalJ1TwU1lOxu;B?t!&uy9E577sDN z+QZG025*=@Ia(qmr}E_8w(0OE4iDSBh&bsMArvBB+8uOj6!JQ24ABhfKp`Uxz}qiqPT~6zq?pT?WcX z(b4ZV-s?J8jMW|e!>mZZH8xux_#Cfd2YZ*EmKLW7qe?>Ds}u(=JbXoS*Hqn?M455m zfel(q1DOdZQq$PtSm4ahP8E5x?zDKi<&jE$oBu+@fNW3FFZT1gQ{m9i^R3_@5+TR4 zq3Mt=91|UZw5MTk#F_$lE#R13ncJs3CH=gsoKD_9kM~_p$*3gI6xZ#huiOQYJ~jQ3 zf5WQcitfDk@De)yOZO!ca%cbguBWPA={Lg-3$6ecZ0xDmO{wh;!izX;$On)_7wj4? zSSIJmu6n_Q1r3i(1cx)hII1Wc<`Su4K06&M#F6n~Fr9v5y?I-eY57a5W~qtfby51W z_8I%1cq%Z8sHWCKJ*V9im(+OKY-Sj`*|VnZ(i}Mu1lQJRbCZjq3NHDdR{}p|q-iEn zQ`CFNhJN@-q$vht2I{6^mcO#NdocG{vL~RfDSl zA(yOGXPW8aHPtIkBdtRl{PqF#Tvp`mj;n+I^v6q#F} zcy5YXirha??MyHRUe0gx<;74gm`14H=t=oiVSB%UD()-y18z3%?Vd7OU2f~ftLhgp zT~1!!?wQ0%2$a>;)2S8+ZNyDlbyeRQwA*e?o6;T{w`Xi*h!KZ)9at$_q7|88?7X5Qqs~?;j4S6 z_RBwC5R^KgUb~wpS?YRv@j%|=p@d4UVU|;ogG2GokoLvd>ux9mPuVd2epp z>YeVh@x;ij4U!iJD)0!&$PPI42+6!Xt30c^G;Mqmf;ti=D_3U)5=trqw_{YaYOXs2 z^EyIUoALGpZk})bvPH)6gGDLOe6f}1%o+29XZ;3+Zhsz&ZVtKRHzNNt%< zG^l**3`dybp~TeYN(nxG5Sl-=l@J;UaZF(%34AWTyz8ken`mr~&{}p&MHg*}QK1f| zmRkR=H!yDoD%rtAU3yH-zYc&D%btR4h~KbgsW;WMdC_ z9G;T=Ik*j4L8m%+%q5+9oDib!+K zQ13G8Vzj>Khn0`MHa>KqA`puNKFS+h%0$cVR~HQlEVu_Q5s)XBQop~xR_8x!0sh~y zUjx#LwhtexemW?XAj-8dgwJvy2up*|AgF>d9?B2MLjGt4hf7jU)@R1!28tbbn()=C z?Az8>QHYtz!B-NMMP~#u4x}(qwKol}`Hs6X^`_w4$(8Q_J~HQYHr~IwlX_IMxW(UZ zd$r2kUy2p?rCJZp=2Z|KCvp)a05qzLB}nq{`}2^ zdhr(-Qden0vh=~M00cjt7}PqWZ`s>*7L^ip&<)|zk}mS#e0Pj2kgqZYBTVvauv;la zcJl5x-QVwr%^dGXGPzt2_0K?W5TB~c$JN|y3o*G$sA3O6&Uhet_iSZ$Q#LM59PwtBJV=eLF_4qc+fW6xEk3drIXCqKGnJ7Q|K}jM>Qe4GHPJaGp zkbz$XaxRvP9n#9}TmG#>Q$WX@O2hs!gPuR)Cz{xeg!tj(M}_;o$BdCCvA{SB9a;12 z7&QzZF^odBg6Ylg?(TxCllR+x`?^5zm1WS^Qf2Sc8zqA*^ocDG*M(cpJVtFGlerZYkSZXq%ihFsBcP}!x{2{(A{<@ z#&ye(7?wMbAO5veje`O2mkfhXxiNYngw4=*W)R1bJyR&cA=s`qw73J5ru|xSs(u?y z8T?x9uor|Ee%!fDYLjllY>Do>G-WPMxX^%TqkRoAjDnbQPXS`%1QppoSQR>?!jq=h z5QWY5YaHjEWN?%@KsA)EsHY9fz6lyQtSDf#-kM-6*Py_5-n*emkfGCxIhvO@!x+D% zgWeyl7NRFOh?7F1~am9Ov3@o~GkodlwOy#2&}L@R4ub`dk0m_~)Bp%C4L1 zS$uixLic<9mUo!4kQOuQMC5Dc5VQoOb9YjT3`^E}%BxmfPdp^84ku6|utCT7vcLce z3(~SWk?gjypIt?-6oM{-`lJ)B02ey`pshH5@X*n-*27j+sE3XY}^1Hg4PS z)il3xtf#+>Xv=;&;FNr)IaSC%p@X{Uf_N`J?V8p}txEy<(|9t+G@etIzT2w8-8Lm5 zeAaK8S;Y(92=&9{;WOWrLbMC3vf;1no?hIVgHAhu$kV|$IU?lN)T_kpbiR{tcC)Ox z!R3(o#M^tW2NYIglJY#TeT=#K{PmvpPOXA@38An+{_xep$<&#r`AIo7MAY9Vb+hxZ($Q(YiCD%L zjnynGx~)Vsrj|Sn+gzI*^rJgvX^BPty}irxfM$dE&G0?2wTVWLc!<&q$wZG9U*(!8TPDLqZuDH;hg9Xb%)CDEi+%euxRn&pPw@?3e)>RFHEBERHa*_MrxdN zZQ)^HV9?s8GYWk!T!K@fErkq;>}Ho=gs(Thf9tlf)rFf{7a&sk=(*_EdDx#A@f7=b z=S&l23mk#f=a4-}2stsRdtI7@SaWF9xmK{h`deG$gyg@OSkg;-e95VHzNQi1+JKfJ zw1@*4#+l2XeT{oCZu@@UFQ%5TrJkd~E-~;~8{7HKJZDmyP;QWm`J>TE3uXIFi-^`Z zeEo|$EH@n)0`0^L6sv%H(B)B*>sNi6arfcJG+cb~(Kj?y5}F;A7AJA&^yTa5&Y#_As^SI z9PV&KTHyrQBQcDWf;S;Q-luY0H#`kf30_w)3sk2kOj7*8M|Kd^bbF%LzI?K=t}*G< zx_fLtGVj*3l01B++IpQd{4q+5NBX}r0%;KQrqEw*GuYrLp%QWM(!iQms8^YmkGO53 zQ98XR)Y}hpR48!4UK?*Nd_qy)FC9XuOj84gL)s4Grua0hBATtgI|_CZk^nm}@>!VTqTq$>!T6 z!^eL5T<11|ozDF8D&?G4`Ed&+lfAp?FIbQ_NwV+l%Sf$B->^=Sez)W?H@(iV)pae_^WvOu1!>#zT#OYe?`S4#+OKy6swdL_v5ztp3l(qO>hiO$PDGPReH9ttHb>z#KbTp^~5>l`XQ8>zfCe+Yq}jJdYOBi{cL@jy3GF_b+bDWgME1qK4PlJ$d$;ahr~LZ8QWOgBCU-FP?gc8T zAp(`7v#@pM)6bU;A(16@EhL5{h9IzQq?kJOjWcA$P)G6@39g~&CTfg&s5uZxc8+Lw z@+g_d8>?K+-GuQhV0b=lq9{?!STL`V;~^v??}=(M`5&lHJz1_D_#*t?_xs(_szZgu zvnzLWMG}9~*b$!0?Jlv^=cs!SIi8Z^cb^2XLwwX$14%i9pq7E?7xTTLsUGKg;R$UG zojTpb7N8n&)4;0P>p8T~)vH8y9$Fs)>tngOx$MDNh0NAPTq*Xu_T@1^3#~|7y^Vwu zp%oH{&^aqK`kfs7Mamc67-)t!!Vi%Ik`;sRTvBt*lZ?m20xdX5v8T2=@jqG2*F8s+ z=%wE);Guk&EtvR5S~|AN))_fGw~y`t<5E0$XNQeKSsTc1f;U29SXl4{@BUAW3K~9k zK3w%w0a{%56=OVBB~G>zwA+yz|9F&os*RAKLsX9`y{9`46*3u$Z94w`{u=dQN$<&y z{SIy1@571ncrOz4tT4%9!|Ema94|ai*rJF7M`kA2$*LI&1c=_5A^UMKs7=?oN-|YQ z=XE}baC>~{@ac(fKWMAI{Ht1Eu50fS;)4BMP=NVgL#MM!U&uCu812A{T!STEA&Qn8 zOPnT~_CQsR0bG`rZ2nI?DTeIixjJ}EHsR9iEK~@Q`_>)x8_SX zVU1IDRo91p3X)Fq@S{v>s8;XtYf}z!QFt}{!cZ4^7@@R4dCA{L)vuGm8T_Ax>vZ>* z=4UI)FA*f-6?HnOlS!n@De#BMP|Ii#?Zq%g1glUHJZHx{6T#6tH3mhc@&k>9 z=JXu86Jya3z0=`B7#N#;cof%EZ`AGD-ZnqV%^)?jAd+mq2B*z23D+>w^BH@p5RTY z&QIqGW;bQy-#eZNxc++7c{O+1W>A+ndF5U|gzsBV$TRSjopGjYmuc_w>b5RLiM8%( z{HxP!m&FGEn^^&X3RZa>9thS{BVYXoe5;Fw182%&XvDcIh41T9+n2vjv8xXZ0y;^^ z{WI57#=>HL_~zq8#%IS7wq z6T{d?&@r=phvHg^dlPE~SUP9!TC;jR~{-IYs z9W=Gr=l;8K7ZdT+X0Tw*&}0K0R$D0UV0BJp0uBUP!Ti7UM>Qc-CVf5t)6a>eCmj0~ z*$skJYa`*}fE(v91kTr%hS@sG>_8x1^uKuiQd`eQ2z)lsT^5HoFqPeOHf4?PZ#wg-v-g_stGI1v4}>w9pbI5=zQ|pP*+%x}P8~d8U8p^nF-wPh(%=s_mH7TXH^n^-GouwvSsBZ6X*P#Ig)kf3jF?qHsQ37?{D1K!Ut3cKr73 z83sn)OQjsG5nN?GQzQiD6p}_ z%3l0@q1#=xZbeXGn7;c@mM01V5ydllj#L+P1RNq5f6%1~VLVCAL%w~sziZ0OjJjzZ zr84t2n4?TLDMz6-4M8G_uSyIkmKpG>n4&TE@o!uLe0)J5f9kp)cYyx{<5>+oq(l21 z$bN^NGEt_rSTy>%Q=87ol43eCtVn*rar<`PZ2jaP0#>|UNY5(eEOc#b6DufTu{?gy zl6;*oJX|~4>6e4MbZ-`<4iLr4=58l~v2}`x?gly$W`7Rn#N_zB^ZRd2r%Q_0|Bm;s zCw0N%6vkxE;mqAvv)@k!^{!I*g*i)(Z)X(%U|s8>yjJ@WlE6iJuv1Xd2^wZ`aq+}R z8w-nm#I9rEm}nk-laFo73-NfWar}kmr9VRTh%J9IFCeOf$=r0rq)!=+Bfd^qs_V zmnatJurPMBB1zc0C(wyoh&Q-jA8+-Na$aXcWf^w=Vv%%}ITAgIlYK+(PZigx;f?I_SBp4z0|nV@=4T{5=q}ZPA4vV>_*GxrKZwD9)6BcZ1+eH|eEY zN*un56}H>a4t}aYU-m^r+sm=50Bs71-}lyi0CwVD57G|tD!F4zC@f|rW%sDbLyxd) zS7dL(HmNL=Qm%OVt|W|y8BI|C^4iG|>oTBYZ2$%)-5BlFZgFW?88kJf_XpPqmYXC< zKVit%DB4hat2VZNdChJyz$zs{M$$WF)l*kdAYTmr9od20Q zcGSKs19NA1IPwjW4vGIC_V=4}ad1>JLuT&V?l3qpg+~Tg8lwZouO;z#*Dld#9yUcm zp;pj5)Zy4g?VF?R@9s&|tWl?Yj^3oY^Dp`aOlvSTJF7?!2tF_*Z$A8gAiuCX`QKnG zMB%Fa>cvub&(m&fp%VqOyyTY4vGjT3Nv-dh#h z*=!aMiHcKfPp~Iqc6xGK>mnEdP?QpFv>^XK=cgDu%Nytw8QN& zvK{DdGi5_{y#2$5K2%))6Z zwAi>5b$ruM40%|Gd9q-2uPc$fgkS$~bai2*Ax9;@veFU``rCI*!XIk(N_wih{=O2t znzPi8>)Lf!>u+n2VtDftj~e5N;}apOYh&me_t(JHoX8o z3k%Q3J%&fMIGgo^h6-*I|C^q1es8E_m&!S;y+i&O#QhvDY>%35u@`(We|sqw*#C=w zKVdl1M4BP?ct?&sbKBQdz`W6}#9N4pe@z5%)$&^!@Ub4i=(y<%{z4wIohfy5flaPbQ_ChD1VVwZ-wE$SJtHu*4D1!`b&;#A8)kQopx zv$nbCB=tOwxts=$1cJXL7ysH?JsC{(g6MXzC=HGHx<0-z7aK!A@^lDOe^ZLgoMKIX zn)C)ML|F`@gVJ?F*z;^0Sx8_o#Ra=E5hBg#l5S0J0|cd4XYU^_xZl~lH1TzF@(hcJ zX!}LODes2|oI~EtMyiy*#(+TH!@`zW9uz!1DnIH=o9*S;ac`!)M1(Rm!*+D&xde|F z!5IN9NN31Um#mX;8E_Jy&E;O1&QDsdd^zo@{IhkxTFte5*sei8mI(sE`$a_^t@4EW zzmLYRNG^Si@g49r7TQ2tEpOp`v?Thcm3K(!@@2r65TmAwf0sUbwRUeVJ(fIlQ!Rc4 zsngrUtC%QPwG^?mv0M5uZ^7?{lsf1Hm2g5yAz@k%rCYfG?&d9 zx7#JQqKdhfYQXZpJ2EoZAQj-eSC={g<^zuMuJ=dS7w=x^%nvqndVwj~(8QvmX1#N! z6ePhI{acZ7%*e=TOAACox&5UXn`xk!{y#sw7QW3;_Cd|skDfwYU1@76V<>zDF&zJ} zxv8vDZ+bvF!xCr8ZU;Kg#_Ph(3qet4gj?}@`Hch_=HJDa6xY2bhpc>Gzy6rpi+8*? z^^sLrxwLW5j6u*DdH)5qUGM1j{nNHc<%xeJZJ-Cs&?;I11ISk(p5@hv+YWF|_PbL2 z-5IVGE3$+@ns6Ibf`MlMwsTMX{5+rFr!d9<Zl%Z!2R`<#wP!dPLbO2aHjZ&&DfYxm5{^&>PRNtjcuz8e$))z zw+5DPW$o^t2PVX>q?Rc=MN371j>im2rctCO3LCh)oS8KGF7&Wvx(izVdG~Xx`<*%R z6R`$<2ucrjycbHZXr^l@h}Oc6UfY?bhgPOys~qRybWj#PjY=?Gx*1{7od9zPnvool?k`kx43F$)Lcr7|3Gf_dwTPOCY`_A#)eCO29o1b^o zWHX0KFsY8fH79;cvR!eg8teQ_r7r; zx2D;ILMe$)ud7pcz0*mute)iEd)SGxL$7-)EWm%{Pd%BXUFyp5Y5~4Gl;QgnJAY9i zaX2!)X{Z3Xk}K2v_U7KAk#c`U6&Iv_ip7KE$$ljD z5dJrTg|S|r-<6WoePqmjvI&1TGhltF7Bz$$Ow|&vk`+TBvn=0Y6}k+*tR}1?R6(|< z5Kfx#k(hPrV`ht0XA<5(5YugkrQ5XGy^TV`!I`ltEnZo{qY zyuyiK{nz*4meg{mbkp3>d8CGol;m;wJ!TWfq*hIHIg&VJf?+B^h!9Q6>DTJZj+rBA zD}r0->qBBx+>QRg^Qf~Wn*Sp6H6;)Jx*M+otP_*auh#?(hbak%M_~O=uj%0#+xm%FP5HqWMPnkWw=PTE*Rv*mQSh z`cXpu%-aO11T$sV)Gx1mRwzT9fQ%pI{?NRAcO(t525)zqr3KG(cOuC-)>eVVpAC){ z5C}mRn)EsO&?EMeJaILe&XZPuH=O&Y0$M`PDE=F4y)YEx+yyG;5vUTBQ##B)t?3`& zv!w~#?^rb>3K~v>M7%X9cPGk{6bwa7S+u*mB5puBxkW{dfRh$jeh-{Bjs@Ggh$YEB%f zUE*pAz;sMfvkT5eQ@KUC%g^qgT%TJgxwq;NNxq}wUCUQ0a%!&_QwW43A_MB-2uAW; z;?+hujYLiS;Iaa|U-pBwm+~1n5KeaiRf9k)nK9^?0i-|2Vk;-Y6|ubwI_kI_hFo&l zBCetMrR{0sol)T+ThK79y-h z&@XC#OVX~N?i=Yw|5rEj8-`}qJEvPuYQZGN8{*QUB7`4ZObT~;@NMbNBP?zLwNy2? zPxo97MoHT8X_Yi@mzMOMTCM2+AVYXvPK++#2r%f?V!1gJFvJ3fpM)k!#*9#c#PFXM z)03*5UTWNVeZy+F8j`n^sbU-O&IEiMP@;%iT7^j=12E;kNh0xnyP~EV7o}%v)_lhl zWs>+N;ql(Vuk(@HB5R|()qwI(9d*OUtxOa{3t|x;7!uk2$8M!#p7{tI?^UMqhHJj; z+5@3WvkIu?{Z1C|MF1ht&p+tH(0%yfRir$@6X=&`H%wln0U<>@4w&2%Qxppon_h#H zegN0dq=N#+?uLTdhQM4l$V&-KH!TMpU*5Rfc!K0DxM)>0VWcbGW-uqXkyz+)_{+on zv0dFw)uHWU;qaucYqXCEW(r&lGzppmQI}45D5OLAF)N;k;ur(-B)jG{eqrH3q$C=i zZFnfVg^f+**w00+zP!i8?^*;yTuj9&H))CbzCRULIc#>GPF7gm?@jh!wf!diV@zEO zDq0Y9ReEBoV%4jVnIE!t)gfaon6ubD647CXgEn;y<}E(5<&eNtSKx#UJEb z9pJ!;U8{)W>7D9Z=kVc&Ko{+sC7O-rHMq}N-2u(GbZ+@$|aZEEQ@qb1Qr&5 zDeJc^o!Yt`J6<_&>IVtGayQ(xEQJt~sR!#tK2<0Q&!sHs-$Hg{`9CyWWmHvN*FBV= zw6vsvG+auM4haQmr9(;S?hcVgT3T8Jq(R^kN_StnySwY#&pXEVM+bu;Ue4Kj#awgE zN!(LgOHK^X_K$$;b6Elt;7TW!{JEKR=X$(yCJSc8fy0&~JEfP>0JXF$z%(0GsAkUP z={V%Xa<9`hy(&)c*@bvM>KBbqTI!Edr0yHcY7}cCb&#raB=Lx21khMIo>WK<2y94{ zIiR}P`NVWm?6e9+awU_9_zU{G&r2q1lYhZ`B`S&omC(TByOIt8r9(eZ>Z{b=8|KR7 z!+DxSHb=7vtuJ43Xt!6Scge*o6}T5S^dIjtgug#ZbNp1Y){up zrz&2|G*u@8y7$lO{y{`FLKp*?BX89yZmYrxFp46$vJkkX{5l9PKct;VKqX_jybsUR z;Q;Kqyz40svBam|A8iRv)@A^@2u5N@ItC7|ms)R2|C?VJpPed~MvWI!*FE($Jv9k1EgS7=*QLaSOWn2W^RX)UYrw~O(nznumb$*IfhK!fw!;o zo{e!v9QGFpGxqS1j(<*BYnS2?`dc=aQcXG%a&OZ-)x*&JiZkbIJyE{f)1Fq7*i)PU z#-(PtA)0cHBD>RGg|lna6JqHXcTw`9Q31Gw?r=&Jq&6M`gEddwy}%bKLr%~3M__+1 za(-^2-29_m`H%!g;5M4?9-W#`gq&+2ajrC*1-rKTGv-JFET^ zs&BI>!G1h-%f~;h7-cYMC`vM~C@kd7p4Y~Sbp$qu*$Eb)lo#$SodkpXX1o19=W0r9 zK3`0~eninYO2&h`^Z(Veq|K?}|F!vQiQ-}~QX!S^>IBV=>e74?Z|)E%3y=m+)qKI5 z^%p8gjp*>Kxn;l!A`cTr*!*R%z?H$>Yj(_H;FZ9e1f!;v)FBEHkE;J_{0bTBNg=7) zSop)8SD$4peYsC>IPU&^87Z=>fT**wsQu<3^hrJXw1T1t>{%ef#Rh^|Us#qLR=SLy zMsIYG{;pnEAsj|~HfLa8Y`5TZrN;lU$D%U@!JV_oo=Vg3%>x zU72c+@JI{syPDyHSH2?SOE^LQlJ4!bYTy7}GX*tZ3R}vrxn*Mu>xp+%0?I{axQK1r z&($5ik^aPL^&y4to@J_qTeG0SkYg5o^=eYpQacd)R{S99yf$xk{>i=S{3_ z_GbyVQ~LQAKd)^sN0ob)Z8^ccI^%qw=zn1!ES$k%-~}_B_eCG9%p^y%3>vBLG#yU; z8|B%+blglo4&AjL15Zr$wUJ+b%j2xeoI&p->I`_TS*P|B1mi)|s@N!6{NISLtgTLzR*_2fRF87~G2Dmv)L$3TJ>E`9GdTu7rGKR} zD$E)C9Q&$Lh_k=N%gc+xD~6yYduCQUTQ3;U;vm27?zec7A9IGgYy`XX`I5@%Hf9+- zepzT;|BH3)3y;-wO~{cq9cBpW+RRt7>_i$}F9K?fs|>~WtzD28sI%lp&Ec(hZwY}pID9xVX- zoZ_0m{;=)&cl(Gj$K)Zl_iPjYUH#2(ei3Ke`xjPNQc@k$n15<)=AP)(+O*F#xVE;n z1s#N2M^lOP0InGrhU1C#|KsEZHXD^imZp3!ng7jQq-k|zdtS_^z&Cot{FG1IyjpEY z?_AfRzR1tY{J!puUM-FESiH!{+K64Cn>5#en@6oTHDgn60uKX z7ayn!iZtj1&hZC-$6J(tcjl)ehKg06gv!u-q7;0%Y_w zc8`)F%>eWEpLOB=z|Q6YD))W-=KxUs+@Z-AMJD`0nD$w;MlA{o3POdcvdsbV*1xmD zt=XGD@!R4@Zu#K1i@az@MN~KPUiO9_;<|h zU+^L*i_$SNUtNAVjof&^Ii!Lcq`f_n(tE_o!f z^Pwt4b~Uk=59P<28Qqw2=N*KVs6b=K<>jkl-8ybdPr3|BsBHN2$HMm&2yF|`9Pio) zuGDFg3#^uQ>_>3jKB@{P!&Lp5vcX%wdDx6oCY>$vzS-38^l#=RQ7qOvD z_~ZVSgUd7iqB4iPwOj7Re|o1{y#iI~_CeOJwR7k$y-_A29a{e1pg{YNZj6(%O{18Q zAbEiGOb61u2Rn3+#p#91`AV!|m*;TX;rqC9}9FpO#OyY-1vGr6#J8Yn6SFP+dOExC_+Ya%ofOx&u%*H^J*h)RWH&0GGLB{ zltKm`il(}SGyfwj=udnsh^PdAzY}a$GcD7VA3gn8+``B3PW5J4R5gmg@8$<-Cs$&x ziIbMF9CHkJ{?U;=DPR-V))Ccu_Sf+L0Z{bR&=6jSec!RLXPs^h*vrGh#(us*G0NLc zgYk{a6sd(z0Sh0gh4z_=wNdF}!oU2qFAlrE>ZdRM^dfYGSLW&@d{8UdOpze4r(3^J zo8rvxT?`QDhAm5+O!r=C+klsJVmf2xeMD^IjBWfbF^{pQ#4Mq%3K!XQ69!&{HYNn{ zt%ehYhXu=DbUU`MI~GJQiqa+C3N*4}@FRJi7+KATGzarH?+lODD;01})|5sg;fiAH z_BW$`9Ay1mSp-eqARXQ*Q;K%m)ZN%ZYa~ZNm{DWs90~G6*-7$DeD)uM)vO-wjxCbr zAfz_$FyQRA&{SGZa2Al>F8Gxa1IA@3BYQh-{Q-I4zpaK6BW-{Z zQYA!~57qTw-Fh$$F#qXipD%KbUA=OC+Mj2hqE%a;3Ip@C$74#0w}8E7EY$8bGaq7x z4q*heTnjhEk9_9u7$+GjByF_-|n^9r=^qM559Gi zU3$zS5Wi}H$`B@;5%oz0D286be|E%03E46?&g5Ts$`Yi=E*vfSI$N~Y;SS)A4Q{&8 zao$+hSa(kOP+;P?>@?C@%|t07VP>ENSwqT%KR1jBAs@=`K4EheD}$3Yo(PiaPdJlw z6ZsnAPAl+f>~Q-*E#Di^i>McU01&+~*Oa0DYg{`ZO`Vu<>g=|WF<7bDI2-sHjcUjK zXr!Cj%A?M#Rg_{O<8kio!*g-;&-#D91_xIp*3L?c^>PMJa-uCugJ)*S{(=6X;_E` z0>ZboWM?p0JfxggkWWwdj`V9cy@*{00Q%)v9|(#N@67D63QI!82|ETd1ho*@2foCN%ZM?PjJg4mo;`Rw2OkFsCp z93~c!jULFMC%tJTq^*#fkk|G;1Plyx%xk-&J ze+k_P^d>OyH(}Uly99IGyR<*fVITn~E`Xp7$T`3^pire$C}Am(=EphH{>5v|=cG`X zs@)Qi^2aHnzwchG=h;Ua@XvoENkw^!70`mPs3umnHlouR+ppf;);+Hn8{D7ibr^`T zQH@9)%|KH;U~xc4Y07TbM+{D$oL4wyT*}D!bY#HVQTjw{Z;R8@!!Un~uV!cAB<;`L zbq;j|b=+tnrW5(I-0kPu@wtzFo6L2N5@Go!c%Nr_Bs882Pu4WRg3Y~hyS+1!{O#D8 z?wM}JqWC#n2)sYSUj0W(Blz!re2Os1e_8j5OYXllh@1TtStXG&EA&rR31ZjFa5K-^ zUPNKr6Nuf!t8c2yBe|gr5%#T=ZCb{KvHqx-4xp|3X;U&Yj5l4@`! zY)~|*u{g83cCvT*eU@;;DvHK&GM;1zn`15Iu8B8xFz)$j8f?(@2`C0$OH+kYznhV< zTNuskFsBSWiP8M|xPQrU;a=NqEi49&SMJM*k(peX^#vS_a0ykREU7$)t~s7K96fO~1vwLZN_z=1a=#hRr3`B{HL)jq%50IZP?ZlcwXC z(g!+XiLl9oc~54Vn@3RE*1r~r^xoB_ckV!|OYF?wJ5+^!LD8BAbf3&7;id3+)wu6b zlqtf`c0IP_v4#kpg|Q@BjRr+lPln`}X=t7+gLOL*uPDbTr=xuCVpdnjXS)()88G1BwGsI8$ZOKaXJE*GcoDh(Fr@93kP7eXbeP`Oo5rXZd%!?~9-= z)L-Aocb9__83v2g9%nF-3*6t$*~z@jBcZ$;+nNu|2E~;U>%-7_O~d zaLfS=&7R*yPRP$W%)U=yl&-=<_U0^5g=a2hZAfrvmGf0RvQ)axv(U(vDREw}9UyIe z6{W*aub`+nP|s}HppI5sr&6^tbyvfWEZMvlxoc8L5j~*K_mTkZqB5!G4Vm;+4Znw2 zE2r@)r5GpYe^uz>dmBcJ;HG@*5$qoif~QS&7dT`_d~VxaD9U(l6=Uxnx$a$ybQ@bl zbhCW2o>mY#-ahpKm;&L1=&f%)v{xHGS37PLxIg-*LD;P@>{q$ zZ=!cEEReXz|DOwRpwFM#ypM9jEz8fP2MEVtTN~_h(BRIuGuAs!7@VltKY#Ms$Kjd_ z*4jTi6|c&^rs9_zelj*j2=zfiXRreE9&iQy($?YOKBn(pKTjs4=+Oy#_2`L7l-OSZ zew6sVbvTe*snI(G=N_&X5>isjmMu9jR;+<>I0~cCSOSOEc{q@_HLUo`+$^uV* zVzP~Zzs=U#vo6u1Wh8`{_@mW;FLdRy0PoNiD*8(70OVeo+&c%9US~(KpS_yA&$-~~ zFjWxC!Ag?L2OS&+7PI4jvtDFl8>ifF8)FTMQ$i+gh{_o3wT^JomDafnn|psh!5VZI z&wm2BE7>ccckXQU$ZJ00I!~W4-`SsIhphY1Qool{bd!SYFQn1-&OmGWn=(OpP#J6O;tEsvN=)1~=lAbD4+MV>1+wMw*gV>Y~QD=`0v^t5lq}g zk2aD^quz{(XrLHTi_G1W=Zc@lwank9I^K~Ty!N!`GT_pihv$@`~NE2JnRE`QdZE`F&ECr)?)qq~U%*CDaMUN?Fc)>)&qA9(#$kb<@VAQ(5oj zBp+Wz`!5@=xq>sNcTiHZiq__L^=XT&n>Xa?W-~hco?6ROC$xec-#>V4chg>IRQxT1 zTQ#CBJ{~IJd66yZ1g2x(Q&M^cs9D-K&>VfDMK@+!VzynADh_U??i%uJMecAH{RNp9 zk;Ks?zS-{rN>%F6s{0veNV=4)ZfYCum*rzmcAy`2SqtVN>B`I0f^$MDQe|RIJjhiK z*pP>j0vvwSU^O#G;(8OPVX?4gj@kCR)o@xdK*;No^SaeAfCe(^EB?fVa4!bue%7)I zu2^=_rLQY=o3#GV(Z^XOKWMx|aVG7(3Dg2O;?>uGFiY3cj7ro46IeA2tF>S73#O%{ z1b{F8fhsQ7Jf&YBmLOL={Fzf~6+p|@HmFZd*(Q}iP|@^uXfo11x%KdQ$0~l3Zw1`Z zr1zKMU^EK|S6YcXGrh;jT)(x%gv=iY;b}37w^H~B$G5*E=OoUcMl;Hp&hR3GDlUdY zX#h3}e!lVIKFh03md9AoP%~Ht`C*L{S3XPL6&OMcu|b*_)&A5}m-@%kFCSx2vAcB| zIsfrG7|nc*JC-%hDoK}(1X)LL<*B}H7<~O`J5QB)WgPG?(Y_b943i@EGTkm3%g$h> z$eJgWEt5OYWCGN?|E3e^N7t6?U|`VBQM0blhebXmgLlW#P|JEitspj5Gg3|)7HVr3oj*MS8`^O`NmPKz!*|=8e@v9qT$mxC0g@5DMVVkGA6rFw8;rNz_;=cf& zqoAOu`t8&oOV0&C@0U@bZ>roSFHt30s%)~FIN=9dzKSxeNizuvMI`mUyLpA^dWjRr z`y4raJ$a`Wk{H6y+k}6(?Gy8Gv9Xc#CcD3PRK{2{FYwLe8@Fj{Zhqx>2@{jBHb8Yt z@2CnuNx20FR2_CRfu!B}2bp)z}`Da&;0-wT5_hh6d^9syi+^r><% z%{G4B!oE=3s{`O$Olnls9eLTGuw>sJMx^DQ;pgq<_Fem;LKQBAD?t0?b4GO9%MsM4 zcNADbNgSWQR$Ct)h&GSE8_%cwnxXI+#a5fVa4Cl=`$j(PM5v@hg`>pRWE`xAGPx7=+MUP3iI zrQNvUVCnb<%!N^ALbrNc0YD!<{ugbps@nea^0L(@HQIU_3@oejd~BKXC_&w`gz)}L zp;s1a;QS#N-t|iw-yk-X1O4M)+QfQmnn~?notb9}=3d$o7@xXj5~V(4u1zGJ&|>Sk zxjdsE>()n*h+KcNtDkfbHn1m3SOWasi==lUw@og7>Mw-*&Cov|?{d%$OkZw#)0WeH zhzi0B&P>t&JVRb_2lHiiJKqeaj}J`yU_~1IBwdd!bZz>qh@f;ou>L`E4~_vPl8xEc zS+a88ew0W}eH45E5HPnF%8&bp+z6oePo{`lef`As!!rNepSU?{C=Vjr!iN|8CmsmA zj_U!SW($dPRf>|{yf5(Q^8RR$|9vNLw);OeoD-0~2;T~zQ8rJpsK`Wv+DYY|8|N{a zZu%I%|GoCQNP2myRuj{)nO5`DJB&>u{Y`I&eZ(hH(^l16zPwwsv`c5k3>2dXyD7>_ zghPkssEm39ku_a|e9pPGF^@^LSbl=zJa<0P57y?UVlIP>Icnw60eyrUow;|Xh+bJ^ z@gj-_XUETy=aos$(Zrrw2CfoOK~lb#!VN+LeIKF+L=G4#-(muxhxsqNtYX@C&Ht?x zp9XeO^ zEL*s_egvJfwp(F~1%u}#1K&#TBsp7vLNej|m@T``kaAG@B>Bggs7&*VaM3cDk<*Ut zMe{|wQ*K4x{W)M4G^0heP-^Q{s^0G&q3jm6`UY`|$*Z_z-*fucXO>(3r&kG(=Co zMPQw3mqxls#AdM6ZITS8X??z@9j3EI@p7adH|1@4-Ap z6*K#c=qOhm*F{Mfb9!KBxhH>I?JuR+EkTE752^g$$E!fh;>|aprI|b_!@xUk@sfc3 z8ZP)@dL3oEH=(3bXTKgFYJNYo&c=C*cDvee!2H?MOosG|6;jr|4nC|sjGOTF*qT9V zQMw(g^FFES%M%v%YnFr8tq6YCI2q7A**MNv@nmneQO734@8a!D2=cR9_ ztcD%2jqdJsP5ArfQ{w`zk|uuP59D4x=`AN%A&JiYO5eeAkk7l+?TA8Xk7*Xs<^py| zpi0?3OLL|F1}IVqORLwb5K^PXn&rq0jEt4!e=VxzBn5j@)y~1@1wuhEmt09|%uBm} z>b#>$fNZw;fMMvH2G@)rPk{9T2Q&#ID$8qbQPTIF8L8zV0N7HO&)Q8-uGQkAf@C3Kv2CzT_DmtFC30X>&TL0zJwTQr00s1A5Eq8OT^k zd26LxxPHEktJqq%)wj{tE%SkzPZs6};Q5q)8dOT3QGCVtz1oE(-ySvBJYM3|{cNjQ zIbZRIqBk6MTQN65&uh!j%6cb=AK9yeRJDUa`)iPKK5s}D8Z}G2!9>lyaro!Hx_lN3hdK~}A{ z+xD5!sn$kg`Ag7F6I5ng`i{&cC122Oc~Jx_D~J47Ve1f45Hm^!HGV%^s8Z+uhT7 zF9qGM`>Jr7OALrYZ-kF@w(H)`bLv5bdeW0ner@LA;e4J~Fm^|f;C9~|M$27JsEqlC zFg%w{KCz4TMQ@dkx@CQT`3sI%cqI1VW#5*IXFdB(RY6INRqYEM`X|!ey%g?yRJENh zo|L8IH9AJg#zZemVoBJo*@?~L>E+mB*kY@H{DKIdc146-%%@Y6!SIsb5c>6rBYhxR z5ODWoz`oI z@`f}C-Hz`_g$q6FG^wwTyB*91Gx`rgBRj@xBgP6cCvi8TkpE=mJ{JoSBKA@K{dfH( z@7*L41{H-B;T2tSy)BJIuCv&Z$btjXH;Fjv&Y{V(l6Ddn!{&fZ#`*d1S#MldYR8Lk zH4yWe79^fyzPfGeRyw|Ff2i7SEomV1K2C1F&|CGQjZy9S^67iSVjztjD2g51C$GO? zlKk8ZhSiw&b1xNs%yY#U4Z-*df8e97E`VcVB~7Y5OwQ$3i`%KP&7gR6PK0xfjjSW6 z)xCX6`FK#8jt`J471Is`_cS z@ciiLz*T$5;KRr_-@sw{1=hH@Jm=t96`HdW(sw2tXt?kGkhdxjG@~ubqeLzZ#ZVgH z-w<`kbkFIaYg-<5J0;Ow05TYNQXW43s71BIPFtMU9xU_L*&>fpFNKLKQ=+0`(_Mbf zmN?8I1-PUY#Sey6@7`Afas=amyW~MssnEtNW&T7Kx*aAT20qO2_SJGj?qm{iBtO$i zX3-{niX5T0dvdVFxy|v8Y9?4wd~APL?=v-Z`B(j1pQGjWDC0UR%KP8ns}-Bwa&f{Q48-MrQDqg-4A*uGG0I!vRE;h^ zsziLbmzuv>FN5qjwR|C(b

S{^=ylAeKm3j;wyrfln?BSkocP68^2LGWXzgA5<+Zl8 zwn&Ytl`);Y%MWl;$|Eg@4KGY=)4F>T1q_xC&)*!(tfd+ zII-hg5FcyUSwmZB`xP@IKiZPl<&MkGSAFE$pyVb}a=mL)?vV?{rkF4>(rJHSq~SxU zgK4Ei1lujXpG1n=9#W_6p%RPX!XsT%q|I+!dp5*s^cUG{`#ZDY2+x>Bof7r!5@K(g zE!ETZQCr3slc(InYOve9LBaFR%W|)+=!Z05()YP!?cW#7!?Ojdm6a94lDw>}EZy(< zWj{$O^OBPV7PWu=X=2tII>VcBRC35tu#|{rupQmjL$qJkZx81aP0nA|cgig9l5x3I z*`GPz=;hghI25Xu>tQ!DH!_YDoczImc8atWkP?ckw>I+&@2 zDGi(=E1>NNHrM98V17D!F3!6whCzMTDfW8Z!Im%e>W&)q?=MfGuxvP5QSBH^AI{W% zNHWBu^?O5l@~J912H}Gs>H>ITl^@;3^XG3>->&Sv>nrq)`WwG4%BY6xlU=-Jg=&59 z`0o5;VDaZpON(x5Ea4)3(&4Sd2+v6I)rx*YP9B~W=ZSF4U?IiF_$v*J&F z61(#!(shoV2n-}>Dw_?Vea?X}t$YhMs7440@ZUG=XvoTV{lJAk`|&i0u43o0dEW6q zk}zw~VJS*E1lU$<|JE-RO4@3bRay1QyizMr%u+Af%e}1sN+Ilq*BMPcc#vS2=524U z@{cn4Jv**|2zlbF6GKBnL#hxIom@cA_|eDkTnwM?!+I5~)?x*_7A&w~(~K(h+lBBeow{XLhFqcf`Cj&e$~E#x84fWaUS4C%>Xfs6_l-0# zh~rf#aaFjMy)!DvP#mqIo7XHF-vyg{V0}CG&PjX63m;W|77%}#6YGG@L(Vt)cEq%> z{It%_eZjvsbw|!@qFV2svUYqAKRVO5*1i+C+R?qG>PcIX8CD>)?C!lj_*i*d(Ys#9 z*c+ep;%9k?ZKHxmSMT*#n5W~wFfap(j*49f z{gvGgukGFf^YuKQd;JSsUjs9_$Qq#H!Ta0iakfdAp$@ga)rgzwHc?)8}xI`oJ+>u#BkzvXICT(;oUS)9md!KIkQwwa>trv2xi zH{k3i(T7q3+F{(zt>I>Bw;LCZQ3Uv!yS247U%f~RmXlm33EqlV#t-N9zGOICx6aoN z(h=?6{kaC9O0$}~-~P6~a#zTswWaArE0D_QA@~Jq04H)K-ec zNeEwBrPB)>74aDh7{d^e;VwAIF)}$;?o*t9jx588aN$vKkd^37p~+fX>MBI6In8D9 zsjfTMjHb4)fz5f-c~C}vAtktZkut6BM`Q*g2!-u?_-`jik`y1{{cz9Iqh{o#p|i9r z_;>2W)euiwG$uNcKe_2J#y^Uo9{p#Cx9mreqm=5dxlYvZx6a_FfNnP_-`pnME%pL4 z-FIxqc}Fj94l}bh(V{v9GeG>db+8}SA)dO}_~=hk%o(PKz5j*Q=TpU5wG z#}#7K+#OCohps&LZm&*Mi^g?xhV6ib<6zuQ{lU(%$lk#YxT8R}T0XYTg`l4C7?Xr! z^@X*#P<~T#l(oqM?rGPGEi{Y|tyOUnUun5t-Wzb36c?dM8VC&?y_=EWUA}*$siR_# z@-yVlqGhd%@^knkxP-1t|Ijq5<}oq9pV_>%?Z5fTc(VTm)+^%z{_CVlvq3r1VB{)- z*Z`WYHStI;pxe;i-frmS%}zE2e-JD>iZwA#%5*|=sx{wBjL|Dquq@r(U{%;AXZD;4 zffx5oA6(0-bA2@O{5|X8@@qkYa9kbEP5B~fGx5LH$#rjfyj+0IhQj+;M}oeCi2wI| zz~H|(l(@d71?Coa9W4tJ;Ji`(c5TjLW$3Y%btLgv-IT!a#%NJ?4;+~>zur6;S?X+# z%NKh;|3~QAalJo|>vfoEtLy80Dmd!Lxks{=xPCoE&2e^hUkuqDGQWSfliu-map8+@ z^u(MOdlngNS*?wLMS#-IcYk4pqzO4oXd!Vv_$uV{U%u*2s6)9o#S-D@BnhcDfy-9{q0&td3we z1K!u)+eO?vTVdI_?a6H4bSF7Pl#a?zfifl246DTA zY7!<{eekk(T|V6Ty7*4XPl`2nvqt0 zb6RB|p3)yQ^Hr{z_{~zf%ek}#XNd6+@xHr04x4l(<$Jvk9XtFP9#+xP)$NN8&wjJ~ zDj!%!6HKou-P;!JlPWFyES;c&oCPEo-sBAbFs)3E_U>h`?HU;NOWkjhWOw^oOOLqD13qG#mz=OX#?SI-RMaod*W@5W z^$+^QWKW?+D9z2yO{+rqJj#e=n+a+Gen8B0?jO@VpJ_6ioDMd;^%h|jdH6BH?_QFL z{Bvw*Ozzr^424hcZKZKWpgl(59FsqG! z^C8%3>3K8ctaFgD*obC8&#p8%x9Ov#K}!a52vDS}lSYF;B#|Wz)-9b_O6v_x4f#=R zN^QX2ftWF|X^_)vE3Pszu0-X+q)Cb?8MkmZIM6q-k!Ee2?BDB(p}V>iYST9OqFusZ zPk{-sbW9<&#J#HUa5-qV8xY8QuecwYcBLDHg!s$BDP1e=aX>|PVm3@%bo4fko|Zxy zKc%0cF2Lm$FndOL+jn=_;#DaT9teEJj*gDBg)X;CPZzq2s%HHb3rTc@YollUL4cSj z^0KSdsAw$Gl?45@(AMF~!&l+k7HaEGdb#${BXS8FNHJ%lC$*2}O(x|}U+k6tQm6l9 z3o`AT{e_`nLUi*Dsn@W@*4g1f;kX4iAK&`z&7I-)TS^GH3r3O{c*TGc=q|etkU+DU zXsHbbV{?y5EvbOA63@f|+llszbFZ%v#W2Sc?uw?`i?yEFFhly8xzja=%?usaw8r7j zZ}3nDJej;+_>pXPJK$PTnbn%<6TTfxcqRR7YsR255nf!K2($^L~h*YG)(uWTAc5LYGIi=4n$u#l7I2OO= ztH4>D=jT}){zy&?EaBc8%MKjw(b<+%pLGtX=D04;o~63Ex!!MX{+x9j3`?pR{ybDU zC>ow>+e8LTqB}@?2sf%B;@z)R@ZMBU7Ep(|3Pm=<36>e@HuP5XR zz_PTz#Uyw%ax~p4ShD-Xh=Oqyct0+=g*y@25YC2im_xkD-`*Yli~0}q@ym@`w{P78m9*sGX zJAe>;<9ecEO7HB9`tS8dG9rkn`L_>QdWsDh^h6ve5D}fa`55pzEmw% z4SQ{%lLjk!E4OB z_~-A5LO>L?n4+}%6tEY(WOD~z;y0E{Yii!1zOHHBQ^FUHME_(bOyG;8GN%k40it>KM5B3Ra&7HH$( zop@l7-XJm|B)hgqh(l zJzMbM$4_u=4%Op5|5B>_yeY%l>)4o!+5nwK0`HP99a8Vfs+VQA_R)#Z-@n9;Z>*y- zu^p(-V@&R)bIBi`2K!)PUJHvHU-||ro2Q@4p)7g&+1_ILWzOsuT9NW9(;CX>GsKOo zb2CX1UoYe;H}-@z%azmeI+!fZ9e(j}BRpG5cZ}~2b_t0yHhjT?b)KlZj_~RUDQ`43 zuA7@5WzN%8Z_emU|F5Udb~5Jzu%B-ZdBL8{@XCXnUM?}o7WQM7FO4t&CT`k z4Z;LAI@WL{#y zWR0tu{0&)-(yj8uZL>)!zz(AY=d_y+x%U3TtXfaV@TmrtyLe%%1s4%p=ufOF`I;`iKKJeGz8F?E zKe8sQ*O_eZ(eunlo6JxF=bOfpjzht;#=|J~`-loVY^~iuE8bjn{F|2;TmF$$Va3v$ zAWC1Z0$h6wp<|2ojeyou^1@oX(PTi+T07m5MYXmG=S96L+LrkWN1v($AF-dNCFKx< ztHJhqH1p4j5_k3|t4(p`>$kT8*9(O|{>W;vYAkdl)aSaE=z9F>d&`YGw^zA**Q#Cg zUCaF-%Gg@Bp?4k##Z8~Fy%?|OaV{gi*tlQIZ!L1vzxvf@$LJVc>C zcYCo)kaK)^=i1wP;oB(ewP3lrbYt7PnTP-FMi6iQ@gkQMnndU=ssc4k#n-TiCh%}- zpq~HpkE{6aeeXZX8Z}Bs)=T!Z3w|=fdhs?^=ffvbk4QJk^>TH&|E$jNubwiZiHBlX zQn5~8A0%cv46NBW!``j<$}VNbC$~=%!3qY64iAo|CcuT|6%=G4t4k7?8{rfZk_XWc zrth)!0$H4ZfZ$N@o&=_!3qtreL`ndSA8sfokBUwMwYZLsJ~P?|g_M-nmJX}?QTGpZ zeOs#h%^LB&shu*rM-V~G;5SD6PbDuq?fW`Nqq0MIRAp20HwV_BW97%nG#Bab#_q)D zeUzRos!ipf?;Cjc2{EQZqNyT2q50H}k8_)FTcV*!gORaw{}pPa!_gO!wbDNj5c)xx zU0@K(q@=y{E>S%}dlxKwUYi9`3S(zi`HNi&bUi?-xFWTvC2!h`qU3mq)cL2b04|+^ zF8~-#_|JP0w)|%)|cE$ETFFliV^viK2Eq8q7N06n3@A(CXLeS~w>!JLH zZka~?jl8@UM5st8KRB_%O|0Fq8vI+aKWkpK| zMRJW;@g;BpQzBK<^ag+y_Q4714PsUbc^m9-$T4y z1eo*0StA{o6x56nUSB<@yN=aTToTkh^2&Cq`)=_|B{$ezCieUH*G#-CUYKmO+f&Hn zp)P;1@S6>+`sJ{sT{+z=Y1;iDtU!Ik`i%mKb93DTH>4S}#THkzfj!`dfOx2;=KA|b zU$M9|!zNjau`}(xcS>rPK}X!z$AZ-g_el@=p3IE(8hoPNhI*4kvT%%vKpi=DM*_JF zdrf_r#K+C^_4|)eG|jmzOY$PH=B`dQy0ux`FP*sDEel#0IgnX5kXGjj2jsBdGPkP` z+Nb2#(L^w+Rq418^M4Aesm8+huO>08;)tG14&G;=Rgek}dB5(Up+d+!VYAU=PvKai zexmNFqMsPa<<5Qs>R+e26;>;V+j)WH^Ytdbza3V~4|Wg6^0-h+(iS4v%M{VyCfoXz z_nxKD8=2>K9IsXJZ_c7P_=Ww(kIuj=+fR(4BqPgu74@ma#33 zq#8Q+N1ibZSwM6&W!ihOQM67jw#~#bE@JFQbw2pFPg;lA+1Y`+FX*j+q_3mnUgB7L zP(%8YX04;g5uivKv#9>5U+ReXofOGs6``WV=ka?kipT*FwWz+L`{fHc)5gwFPEXi> z#2eGh#euWcz`U3n_^TWTj8n1O`+(xx0G}#Y#Z7mt0<{o8Nt9xL&K{+Ls@OLsU+ffO zx@7Z{5d6^?njgI%Q+VSVC8>kY)_>oPhsxW5w2Rf~mNj=r{f?+yV^dt#OT_WQp*G?_ zEHx=2_JSK)UG>ULs|HC@!%Ia=JY1V{xWeDdJlTTBQAbx=%0|xS|jW!*) zwxzbd{yHZXaC&EFf6OCKS|eg0-RsQ=Mp?MHxEmZ+)H?hfZiAuEC@I(2vQ$(Wxa55z zZ|UUOa$UNXReRC8HAsgwl3p(O*|=HDD~i0f&Z33Eii)d6I~3)Zi8{-zGv_Vbr@nka zd$h=xjcbs_Z@g{2VSYXNfEC*;^U&Xf!s(6fx4>d=@gm?^AmyNEnOX?t;b!-Vj%fh&VUQ z<1yD-^FHmv+MwX7v=%er2c6>gWSx@4-T6ix7r|stC(I$px(JaJ@%%=g8@MQjxO#fZ z>lK*)x^oSxX_axmbHRVU!r?9Yo*)muVR^VA-I03tSK`M!LUN;cE*T^{BO@btRaNe{ z7*Ck{6flfB28v-qLAt+Q-E=%xyYP;{p}u2>#D*?t6z4-I<#*l8f8-=zB=Sacmz6%e zUTX)Jqq#ogP@z+-hKQ#41o*L0l*5BiY2w*r*n0fWb<)^(b^#p)l(GoSuUQ7dPk8mbfwT| zzSKG^%bMX4gtoMlAf5Xcmj>m$YIXAz7FyN49{%=Fp^J891$arZ0Qa~)8tQ8)#M78= z3_aF7ES^-*T)lnD-Ej!QcX71^P&EW=WAel(dy%Fbf0AIH)^hEVM((4hd+ zN;1A@k)Pe&1%Q0#@ba?ZY8qx~uq+-bWi%&ND;Oq)yn$$FX!VN5t3psekv;;xa8kL+ zT2~8!G(&yG&?XH={6Uk96h-Pr2Em`Ft^$Nu=&u->oi8r5jtPSxZ z7GF%`(fTQ6LUx>1IK&0H4A{rg3v+WXgVkX$yPunz=Pqijn7l#jrha{x?oCCxboxaj zi`}}RlGA=g{*~i=)}7b_`e!q|hPWhbC%D~OSm{tl*6Xi!z;7NZnyE6i*O43L9V{MT z6KALG>zi(9Yy7{Ct~(Iw|BZjFTr%!Z$n3skZ`s+hv&uLjWOepsuS=3uHrb<)tcF^!dw=%E&e+xaJM+hQ?=*0T& z_qH@;7)8IHblCM$dnE3<*FusNs@V){duL>de^SX9ZN8q)rK^x&h}MJdF-GXBH9mKX zy(|_+Q$0>nj-y2k4oun1_bWwpRonsX3!RbG-HfaeHf<}_cs_JFEka5{LJeT3fc%Yt zZBF6($5y?Y{Hn6U*Qd9qf17&l>vfjsV=t}9{C4|9&FSNRa+{Y`A%MC=FPM7!j~L;b z;_?{Dx&>J=pKT?Sr&>+d5k2*@w-@Fpy5Ayn-Ta!j$&0n5{2*j95?Scq0=}b|n6D7* zwRsk1w4&K60k=r$S}0cs)kaR}(oM?};G|D$@Jo-qt)yB{Y64p8j19{)4i?ecyqB;7 zl}h$%m64kEeV8f6H`$ns^iKmQ8X_ko1#17Zqe>gDR))6Ig7{XO6mHisO7pX4Sd?aC>)3L4te2ij(afGamO7Xa-HA3(Riel^7v& zYSQtg=yfc;09yZXTbT}tW>hb4VJv#JB;e?td-~g)9B!APdP3pk0c9?0F4qIp zqv$aFR15xJMe{~Mac)QkHs#+g$dshL7Bm+VH`$AarK-MB-}DKh?vUE|UnA91tg>xi#potvu>`@56|cI%?tf>87*wBAsjcDg5I1d=}4S%ptB#tK);aI!GstDq(L zjdw&}Zpq$&YkBOGIZ%t6Vm5AVg{PRWO44;#4auy_r5%N=sV$V@3UETS$76RXj}B6U z*+Xic#dgWSh-ncipJ%;qn!U-w%&=Axfue|ym}@#3biR_c)C<_Y_*M06sIlF~Av-vt zFOlPZxyf%3i*CA#D%5|vASwVjvp(IN#&GQ#evjRB<4`Z`!|*}2u-t?#_tA@w#|4e< z(ALN5qMDVsTm>tV5%eXqR0R^sM1RxyjPSV1S?_Vn+7BO;6ih5UK4DVvWnwy(WXgHj z7;SWU7N&{q=Y#jmR-6is0|i8IGjy=7Ol7)M_j0U=z?8jv(ctb7QGCJY88-cBw?p(( z%9hVV=Cn2=T>9yE3W-ZQregk zx7>RPy<6hU=yGsoTELkB@m=XyfrQ?q4B^jTSx}+9`Dd#}32iA892s-wOY=tgILBRd zx#roKPQR25a}?{(pxfcA!R*3&&UwgvirfF1L7m5bCAp!B5v%r>!wDAY)rnecfZ)XU<)(wLdh_Q)F2RqDOyLo47Yh=HXY({$foznQh(NO z9~E!}dmYCwIfa_el+H6Rz0>tEMI?OTboAbDa&TCe(yH>G-*fVNk<=z0YdYv9VRX{| z-rnleC>3IYCu|qoQd6_q;(-yPW9I>b{zcLT#CL}sPf6T-eCj6XyMJdK301N<#lLcw ztN)a#lS52)Ex2@bL@Gr#cTiMn)yWZUvvAjrwWG-g$aM%=u46W$|wwV4V4 zVW~2$t5jz?sfn5Vo@|BS9;u_8TOo=#L}dUqi^6^|w#_^5)74OlcLMtqW>q0Au`U@! z_e#e=#f1y93cQ#+(L8i-4clTeO>fybfG7ixx^G(F9u`Tyd7h;_ryDJfQKKjR;AD}R z5h;L}6xf}PjwE?lLo3ynBj+aNjX0;nO4ldq2A7*{SbEjmtNnRJJJ_F>1$R&>p{VZ`K$J*cP{@l_I_!2oe3srx6_vk;?gDhiDzx!3O2)l5ar?std zo1-V~6B|3Uj|$n*00E-#^ih#(G2$9_CEb+U7o)VTs+q33CI?}+q_Lsm9Z=H5CEFKC zo66@=G*}K(`m)GY74qncAx^D{p7BF0kbiWgm3jQ*{ z5|PjCcb$#R!PKMXr^hF%ppBn0Y5o}%E1MXdxrI>1WxuN-`ES!*sE~hcy6}0{A#_1> zt(#G%Ujk=O3%$7OB%J~>lxHVGF>DaWdoV#}@N9rBBZB}}xb^E75>#{r640FuOW~uH z)fgs-0yh#{M_)2}kJ<2^@cmTLxif3=YwPD3Vm)Oaf`=c^vR3);^AfT^FZdg)G`Y|H z=2|Z+!#$R6ec6@&CA}p53g~Wy6aCdUGRfuxFE!W-_v(lAPtrOX%Pw%w)GED*3t{O{ zT*bh`ycJ33G<34?vVNZ|Af~sawpUaS-T!H&$eZSKCvw`#wU&$v9ee z-FxSLejR(f{`bMWEOu$c^h87{m1@)Ow2@z-w7EE-l{%E>m?ex;OZGv^ed6gQrEmIc zFXr0*k#`hpXAR-=*I%(O9ER#Co|qP{NSB@a?`)FGvGpwWY*_5*^V_x$8T3YOMw%WU zKb$SX`RU%&RvnTVMV*kAwH(E8A7Opd-b@!t` zIERi<`||v46ZXLImyw%G*uZx(a;_}P618q_n?4mWV_`T|lc||R^?oPOCq7)jzBz@p zo{tEwAL8Af@+->CiS)zP*sof@i)`)W^NX35(E!dSk0C?G2v``lh5x&S$$+j}*VCz* z7d#D~fsR)5kFiVJrh&q7+`hBD-R(VBHYll5Ok^6%^ZwJI*9&!GXO*cI%;&q1^my!@ zKm|k*M`CPEo9$`0iUrC0DygJ9MY4|droQO?PT$?^&Kqv{3g$4d-40wnR=bLunvUg# z957k!AD|M_EWEqjhmh_2YoRZxHmT6w`MBW{?%yq?S(>$DSvYZ!g2N*c<;#mP5%q7X#h)k+kf$ss}9ONO<=zK;9y-C~GRHsn>p zXGH*m<@RtC28T(_Z;klQ&!2?0)%x4#0sR+=(k5#V=Rv4%yOH_YRXk{jC)0SMVKdKF zNdLOWS5x>mg&g~138Q+Jt?Xs&P+)1GxVe0_P9(XKqh?9k`(HlTnb0*8gVo>A*>&tV z$rjhM>m7n7B@qk-`=5gL=9oT z_I-bryBtylqKgIq>6^3`B`5ysyx!w^V9}z(hV0Dv^DO!Cy@nz9A7-m;^FJNhm^xPF zFVDgN!16RD4%+*>+Vb}n{D_fN;rNwcdQWAjY~IS7^UHZ9v=MTA#_lUR?{TaV();}! z$KnvV@PP@ejjG_E+-L!=CmYF07EwcBD49gZZG-H*n;!`p zirU}wDZlfjU2JxS!f_185hYfNQp|)Xl+XAew5ak(erI`_&O!;b%a}4ZdWxmF%e@xhOioC2Qy@F3-x6=2HjW51Mzk#MkOkAAg z$#h=pHU0LjCQ_C;SgoIewv(+h^&TVt$)NFU-U&_)7jfmsQH$l?wY= zypr%HuCvdbWNEw1Vsa69TB>XW`bpqNZt!3R7?&1A0vU-Yem@u~m?hF|&xx!g#Dil+vnos~LTEaRgbn-fo17)tI3_4iqGNIcI=QseQ1Ss7RfGAd;tONWQwY zrqTna^e~f5XS&>l_6G-2E3u1A8Os675-t7o766QL@q5nRonMwZ;4M^Y?j&L1U`zs7 zI_Ng}94$--&O|11sn->nrkWFiZqy;&;}<;IGge$K^(DrUv6n?NTxoQOJo%3j^Dc@`O@Md+&`B)P+b>G2TGt%eI*(xStnIl?IU-{6Y zC1Bg}SRvrJ%0fxr>Bp?{)a#}Al0XZIvqPF^%c>23KF2O7?tcjvE{LwO?%A?eIXT#5 zfFcVt!#Lpj%g~3G7D|U}cCq5!nv4;n*D^3eGL9IA_qR{#fB4?KS|Q2UC}CHA3u#+D zn14VVH7otN9Kb_=@<9D{&ggN z=jf7$Z8Nt4F(r00sf0X-)rp=>b8+ZRtf&dcN*vMQ3!|PEFDLBUIdU`WfmCq`a(|UY zY`@^9aL!Cz|9-AjXF{PJWBbZM^PlWU z#=>MnZ6>7luf0NJ!QFvMVlnJVMJJ9@*~?4xXdstF1htx+E-3zEfNQf1_fMflD^Xg1 z>&lfY1<8pbl=hDvan}F5!u&1UW-w0Z9~(A(J*OM;E0*8u*i05nd?SW`Iyz1ZcE}tS zEQc-ho^8Qwf%@egx$b*|;5^4iMP0rS3IUat4Wo9sNk7AP3}GnBw}-zl%k=Y>lY@|eY+zLO6+7fzFQV8Z?0U2V7DjW0P- zxYX-Qv}{h^_Gv59#i+FH|2M=HM|yQ3N>y-pl;I5kAO|LrLAGug$0SbCAsKY677l+I z!38Bc9RExsWU&A9{Jr$Asd|PVrdDQg_~Yo%oxRFuUZsvnH`%Bp@{m-PkX6&)-w!_U z$79^vNf&K6X~l9x`*jWgNfWKjKzYKK@va^6r0z*C*bbk2y=dK&S9EE^Mr5xVKse`UKT^!#*(PBC?&CX_32D0)p`^?fH^W$t?S(D}5N>~8Pp zrP{kMI>FHlKYLERw+b@t?9h@MCNr} zmF(M2$^2m={z^htR@PhK1KBMxF7^uv$w}hOzw;&^gjwa@AKYgZ+$1vt{QS)12w~E% z0OmZhfw~&0`8Js%T}Gli98z(hj?%P1t3s&Nc^j_(=#VT=^CE#7pQ!IgJ8>t(K};MV zNj9lT_1N3E^5r0Y%VE4))zzRY>VxgLl}cAsq@684@s$o(#+7SV2=T7R$wpB)N&6*6 zC2h4T(VO;5W@y)1Jit;e^xu5|)3#v#hyqCq@YZ<%iOhwoSWj2CVRF)3N>ua)ISpH~ zN=YX4!(sz}WiLkKPebkMIqCe1s+vE=##jYNYo;FI-5jDE$8yF7`}g+iCp*~mP2&Ss znU&EK#V1!>JV+P&wy47xINZEiQGfgM!4}gqHTuF&fD{7!8xNqb1azep3iS(MSGUB( zI<n2@GELpz#AOQv0Q-kDJ>NH5FC*oj3E~PcCp$uTNA`69Ayu?h0AxP1rbE zpZHu>enYtZ@?70|&J`v0=M$m)#x!pJ&P1#-1zSg!q0j!ob`wH=4xfQIFMQ5&bLjd^ zvV}vv=cxi`aGGwbYhKwIP?i`!p_79$Kt)cJNnop$sSV?M5lSZ4E4Lvym~=uy@O}V{ zV;DuQUBaP7yPow;yF`h%P+d)ikQ~W_uqmXEfss5^no>63VVJ+cIQf47EpR?w>WZoaO9k54Z{r?^T6Tq#h`3aZF`T*Aa)(41ZNs z2vGy#t$y~Bi$t`3EM$53#=yY9Le)O-MR~F$`St~t-qtgosd1zMk_Ix+2CK)j?3={c z1yw`@ixr(>qzkus2O#5`J#UBd8q8f$@fcVPj9gi1a+4K9i{OI?sIQq)A9X6J8P!f@ zV>$;UPcnfLd%&n(8E!VK+F`L_g}vn3KOGr)IjjRXo`A~O$h`zK7X)T9C*X%^eX^1W zLao;vur7<$X5UTla>|fDFBz*Gu@3kJ3!^j^;l~(m3KBQ>FFSy3@^e z+WLSul_EJ5ia#}mq=?@UnUQX>VB0S>&!!$I91i#lRWVDP&Hw1ww^rU-cS4WTG*JhW z#nUJ+`yRW#Xl4T^;nm0|);NHZ%ld6`wC;`SEc5|uR|433w?^NjW+QDx0>C~Bo!`IV z83lYiV+0^3%5k7TtJ>Sw=7S^JSmbYqvFYeo$nB>^z#5zwddbt8 zrl|7yoKNlU&4AAfg4nd-nOb?W0{y3lzjtP&fIBh z@?JM%+e%Sp!`R~zo@g_4c?&LwGpY{nl~L4WQp!tUp-TX3h%>R*^3+y~Ob?FDK2_ya zPv>gCmTt<~?rnw<^%z?0+R&Ot@iX!}?su_r6LDNWA$;?E~K6|Y*a7FBZE8;Z6>!azr4=L}CtE>rdL?7kB{e^TK#=H1# z_73N2YHDhORi%YptQ=-3wrw%h0=N-NK=i`I%&ZE;JDggNz>{@TtDsulQdAs#X}TE~ zvv!3JsL`zk8zy@<=?N&r>D6#}YGkkTMa7N+TwS?| zP63Y?=!PIDAkYBnYqVPV5{9yqc%s*UjV>ExD8fdwt%3D^+i!)8Dh={GuU}x(X}GE8 z-|Ntv-9|T~_P69DPD79@6q}S5LJwVBbY%#DVqf8j){lG?@63+$iz7AEui*c)p%a%uq%wo{}wJs|5Fs+lLcY*P_1dKM^@*MLBq zNo(f!+>m4E6@)1{9~uPOw+s=1WDq(@4w3~e+%CRf5>iqcH8nMqW$|)Q*M&+;vfCqJ z?hVf`AmjY!4(fA@Mtl`UNxzcI2_zP#Z9bo-lY)R1`?5GgGm&=9 zB=C81Z7*zGz6}d&xdVts>BaS994I zzytsvM>T$QYs=&A6dnbrq9X$R<=dsc8r$w%IkwLg5;(Oqd@AEgNn8^T^iTj$hm;Zq zQjEM-M!9Spq6&JCu9Ybjr%*#_eIW<$G{KU38(fI7$}~0S`s% zbNks*5`mUJjVTI}k`WSmOb~E0$^q|HQb^@j@1YSe1}#T(8$rJ?p@I>ovg79ZQ3i$| z_f2ztp6M4RgXu1A#uW7Wr^$U#S%!w!1IYQnL9&4ZTqK`+%5oeZQ4jQKZJJvh6n(|c z+Bs#nM=a1KKh_mwWt*ah`O(3Ie5dTd2Tf0$Q%c)@h>^=$ZgdpESpPq0syAST(6+a| z$W35uW}YJlNPox-h5Ex-nYqV}T@fmX(0Q zn9qeCq%REuc+6lRz2)9aH2Dgoo}_seZf0YOa~3MG$jR6c&{F>!|Nv4G Date: Mon, 20 Jul 2026 15:55:25 +0200 Subject: [PATCH 15/24] update license date --- LICENSE.TXT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LICENSE.TXT b/LICENSE.TXT index dbafedb51f2..1a701bdf921 100644 --- a/LICENSE.TXT +++ b/LICENSE.TXT @@ -3,7 +3,7 @@ Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany Universitaet Koblenz-Landau, Germany Chalmers University of Technology, Sweden - Copyright (C) 2011-2019 Karlsruhe Institute of Technology, Germany + Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany Technical University Darmstadt, Germany Chalmers University of Technology, Sweden From bbc8cb6ba4ce255ae4732dd8ab3a10e48b0e5a41 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Mon, 20 Jul 2026 16:03:47 +0200 Subject: [PATCH 16/24] updated readme file --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 993387c3307..afefe0b4eff 100644 --- a/README.md +++ b/README.md @@ -2,6 +2,7 @@ [![Tests](https://github.com/KeYProject/key/actions/workflows/tests.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/tests.yml) [![CodeQuality](https://github.com/KeYProject/key/actions/workflows/code_quality.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/code_quality.yml) +![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Fcentral.sonatype.com%2Frepository%2Fmaven-snapshots%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20snapshots) ![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Frepo1.maven.org%2Fmaven2%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20central) @@ -29,7 +30,7 @@ Feel free to use the project templates to get started using KeY: * Hardware: >=2 GB RAM * Operating System: Linux/Unix, MacOSX, Windows -* Java 21 or newer +* Java 17 or newer * Optionally, KeY can make use of the following binaries: * SMT Solvers: * [Z3](https://github.com/Z3Prover/z3#z3) From 15f076660880cda4bbafc883439e0e41baaf4d7f Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Mon, 20 Jul 2026 16:09:21 +0200 Subject: [PATCH 17/24] remove stack trace from log when no proof settings are found --- .../src/main/java/de/uka/ilkd/key/settings/ProofSettings.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index 7c855368250..f4ba250d607 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java @@ -229,7 +229,7 @@ public void loadSettings() { loadSettingsFromJSONStream(in); } } catch (Exception e) { - LOGGER.warn("No proof-settings could be loaded, using defaults", e); + LOGGER.warn("No proof settings could be loaded, using defaults"); } } } From b0413dd83c56a1853190debf3fe97cd6413b966f Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 22 Jul 2026 19:17:15 +0200 Subject: [PATCH 18/24] Sync File and Save dialog (issue #3938) --- .../java/de/uka/ilkd/key/gui/actions/OpenFileAction.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java index e7ff2c091cd..9596dfb2a6d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java @@ -30,6 +30,8 @@ public OpenFileAction(MainWindow mainWindow) { public void actionPerformed(ActionEvent e) { KeYFileChooser fc = new KeYFileChooser(lastSelectedPath); fc.setDialogTitle("Select file to load proof or problem"); + fc.setSelectedFile(KeYFileChooser.getFileChooser("Select file to load proof or problem") + .getSelectedFile()); KeYFileChooserLoadingOptions options = fc.addLoadingOptions(); fc.addBookmarkPanel(); fc.prepare(); @@ -40,7 +42,8 @@ public void actionPerformed(ActionEvent e) { if (result == JFileChooser.APPROVE_OPTION) { Path file = fc.getSelectedFile().toPath(); lastSelectedPath = fc.getSelectedFile(); - + KeYFileChooser.getFileChooser("Select file to load proof or problem") + .setSelectedFile(lastSelectedPath); // special case proof bundles -> allow to select the proof to load if (ProofSelectionDialog.isProofBundle(file)) { Path proofPath = ProofSelectionDialog.chooseProofToLoad(file); From 56b1735155244b3412c83c73493632a4b0dfbe7b Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Thu, 23 Jul 2026 04:52:13 +0200 Subject: [PATCH 19/24] fix #3935 --- .../key/control/InstantiationFileHandler.java | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java b/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java index a19b7ae7be3..00ca6360670 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java @@ -45,18 +45,19 @@ private static Path getStoragePath() { } Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations"); - try { - Files.createDirectories(cur); - try (var files = Files.walk(prev)) { - files.forEach(path -> { - try { - Files.copy(path, cur.resolve(path.relativize(prev))); - } catch (IOException ignore) { - } - }); + if (Files.exists(prev)) { + try { + Files.createDirectories(cur); + try (var files = Files.walk(prev)) { + files.forEach(path -> { + try { + Files.copy(path, cur.resolve(path.relativize(prev))); + } catch (IOException ignore) { + } + }); + } + } catch (IOException ignore) { } - } catch (IOException e) { - throw new RuntimeException(e); } return cur; } From 680a260443a9953422b81c6ca48604813ce108d5 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 23 Jul 2026 09:13:15 +0200 Subject: [PATCH 20/24] Suppress additional contract in FM24 example --- key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java b/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java index 9b7b769942b..15a08b41876 100644 --- a/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java +++ b/key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java @@ -5,7 +5,7 @@ public interface List { //@ public instance invariant \subset(\singleton(this.seq), footprint); //@ public instance invariant \subset(\singleton(this.footprint), footprint); - //@ public accessible \inv: footprint; + //@ accessible \inv: footprint; /*@ public normal_behaviour @ requires 0 <= index && index < seq.length; From 43a8ec46b81373c20312b5d92a3a4c535e176169 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 23 Jul 2026 16:47:31 +0200 Subject: [PATCH 21/24] swap 'Apply' and 'Cancel' in TacletMatchDialog for consistency --- .../java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java index 459e373774e..ba1334da1dc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java @@ -181,8 +181,8 @@ private JComponent createFooter() { ButtonListener listener = new ButtonListener(); cancelButton.addActionListener(listener); applyButton.addActionListener(listener); - buttons.add(cancelButton); buttons.add(applyButton); + buttons.add(cancelButton); footer.add(buttons, BorderLayout.EAST); setStatus(model[current()].getStatusString()); From beca2580fd64aff079d548778845456d5fbd077b Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 23 Jul 2026 17:37:38 +0200 Subject: [PATCH 22/24] follow up of #3935: fix loading of instantiations and copying of old ones --- .../key/control/InstantiationFileHandler.java | 48 ++++++++++++------- 1 file changed, 30 insertions(+), 18 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java b/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java index 00ca6360670..846b2974dc7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java @@ -5,8 +5,7 @@ import java.io.*; import java.nio.charset.StandardCharsets; -import java.nio.file.Files; -import java.nio.file.Path; +import java.nio.file.*; import java.util.*; import de.uka.ilkd.key.control.instantiation_model.TacletFindModel; @@ -33,30 +32,43 @@ public class InstantiationFileHandler { private static Map>> hm; - /// Finds the current place to store used instantiation. If there was a version switch + /// Finds the current place to store used instantiations. If there was a version change /// (the folder does not exist), this method tries to copy previous instantiations to - /// the new directory silently. - /// - /// It is guaranteed, that the folder exists. + /// the new directory silently. However, if both old and new instantiations exist, they are not + /// merge, i.e. only the new ones are used currently. private static Path getStoragePath() { Path cur = PathConfig.currentPaths.keyConfigDir.resolve("instantiations"); if (Files.exists(cur)) { + /* + * At the moment, we do not merge when old and new instantiations are + * present. In the future, we could go one step further and try to merge. + */ return cur; } + // create the directory for storing instantiations + try { + Files.createDirectories(cur); + } catch (IOException e) { + LOGGER.warn("Could not create the instantiations folder {}", cur, e); + } + // Check if instantiations from older key version exist. If so, try to copy them over. Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations"); if (Files.exists(prev)) { - try { - Files.createDirectories(cur); - try (var files = Files.walk(prev)) { - files.forEach(path -> { - try { - Files.copy(path, cur.resolve(path.relativize(prev))); - } catch (IOException ignore) { + try (var files = Files.walk(prev)) { + files.forEach(path -> { + try { + Path target = cur.resolve(prev.relativize(path)); + // Do not overwrite existing file! + if (!Files.exists(target)) { + Files.copy(path, target); } - }); - } - } catch (IOException ignore) { + } catch (IOException inner) { + LOGGER.warn("Could not copy instantiation file {}", path, inner); + } + }); + } catch (IOException e) { + LOGGER.warn("Could not copy instantiation files from {} to {}", prev, cur, e); } } return cur; @@ -83,9 +95,9 @@ private static void createHashMap() { hm = new TreeMap<>(); try (var stream = Files.list(INSTANTIATION_DIR)) { // using a TreeMap here avoids non-determinsm introduce by the file system. - stream.forEach(file -> hm.put(file.toString(), null)); + stream.forEach(file -> hm.put(file.getFileName().toString(), null)); } catch (IOException e) { - LOGGER.warn("Could not read the instantions folder {}", INSTANTIATION_DIR, e); + LOGGER.warn("Could not read the instantiations folder {}", INSTANTIATION_DIR, e); } } From e9c8700091464ddbac4448555c6d3fd922e4a69e Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 23 Jul 2026 17:46:42 +0200 Subject: [PATCH 23/24] shorten text in TacletMatchDialog tabs --- .../java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java index ba1334da1dc..4fae38b9035 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java @@ -162,7 +162,7 @@ private JComponent createInstantiationPanel() { alternatives = new JTabbedPane(); for (int i = 0; i < model.length; i++) { - alternatives.addTab("Match " + (i + 1) + " of " + model.length, buildAlternative(i)); + alternatives.addTab("Match " + (i + 1), buildAlternative(i)); } alternatives.addChangeListener(e -> refreshStatus(current())); return alternatives; From dc85953470a72d6eff7ace3e69e3b90ead6ce865 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 23 Jul 2026 18:03:41 +0200 Subject: [PATCH 24/24] Sync file chooser before opening with last opened location --- .../main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java index 9596dfb2a6d..06465bf2ad8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java @@ -42,8 +42,7 @@ public void actionPerformed(ActionEvent e) { if (result == JFileChooser.APPROVE_OPTION) { Path file = fc.getSelectedFile().toPath(); lastSelectedPath = fc.getSelectedFile(); - KeYFileChooser.getFileChooser("Select file to load proof or problem") - .setSelectedFile(lastSelectedPath); + // special case proof bundles -> allow to select the proof to load if (ProofSelectionDialog.isProofBundle(file)) { Path proofPath = ProofSelectionDialog.chooseProofToLoad(file);