From 13cb6b35e97b79e8e4f415becf916dfaafc5d315 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 24 Apr 2019 02:30:50 -0400 Subject: [PATCH] VAMPIRE: add to #40. I am tired --- .../ide/.VampireLanguageIdeModule.xtendbin | Bin 1685 -> 1685 bytes .../ide/.VampireLanguageIdeSetup.xtendbin | Bin 2500 -> 2500 bytes .../ui/.VampireLanguageUiModule.xtendbin | Bin 2342 -> 2342 bytes .../.VampireLanguageProposalProvider.xtendbin | Bin 1792 -> 1792 bytes ...eLanguageDescriptionLabelProvider.xtendbin | Bin 1965 -> 1965 bytes .../.VampireLanguageLabelProvider.xtendbin | Bin 2405 -> 2405 bytes ...ampireLanguageOutlineTreeProvider.xtendbin | Bin 1819 -> 1819 bytes .../.VampireLanguageQuickfixProvider.xtendbin | Bin 1786 -> 1786 bytes .../.VampireLanguageRuntimeModule.xtendbin | Bin 1706 -> 1706 bytes .../.VampireLanguageStandaloneSetup.xtendbin | Bin 1980 -> 1980 bytes .../.VampireLanguageFormatter.xtendbin | Bin 4130 -> 4130 bytes .../.VampireLanguageGenerator.xtendbin | Bin 2338 -> 2338 bytes .../.VampireLanguageScopeProvider.xtendbin | Bin 1751 -> 1751 bytes .../.VampireLanguageValidator.xtendbin | Bin 1736 -> 1736 bytes .../Logic2VampireLanguageMapperTrace.xtend | 2 + ...pireLanguageMapper_ContainmentMapper.xtend | 60 ++++- ...ic2VampireLanguageMapper_ScopeMapper.xtend | 1 + ...gic2VampireLanguageMapper_TypeMapper.xtend | 23 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2691 -> 2691 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../.Logic2VampireLanguageMapper.xtendbin | Bin 18156 -> 18159 bytes ....Logic2VampireLanguageMapperTrace.xtendbin | Bin 4215 -> 4481 bytes ...pireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...eLanguageMapper_ContainmentMapper.xtendbin | Bin 10674 -> 11150 bytes ...pireLanguageMapper_RelationMapper.xtendbin | Bin 6457 -> 6457 bytes ...VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9839 -> 9839 bytes ...gic2VampireLanguageMapper_Support.xtendbin | Bin 13046 -> 13048 bytes ...2VampireLanguageMapper_TypeMapper.xtendbin | Bin 10792 -> 11070 bytes .../builder/.Vampire2LogicMapper.xtendbin | Bin 1720 -> 1720 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes ...Interpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ..._TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../Logic2VampireLanguageMapperTrace.java | 2 + ...mpireLanguageMapper_ContainmentMapper.java | 64 ++++-- ...ogic2VampireLanguageMapper_TypeMapper.java | 22 +- .../plugin.xml | 111 +++++++++ .../plugin.xml | 211 ++++++++++++++++++ .../dslreasoner/vampire/icse/FAMTest.xtend | 4 +- .../vampire/icse/.EcoreTest.xtendbin | Bin 4545 -> 4545 bytes .../vampire/icse/.FAMTest.xtendbin | Bin 6296 -> 6302 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6618 -> 6618 bytes .../vampire/icse/.GeneralTest.xtendbin | Bin 6456 -> 6456 bytes .../vampire/icse/.YakinduTest.xtendbin | Bin 6040 -> 6040 bytes .../dslreasoner/vampire/icse/FAMTest.java | 4 +- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 47 files changed, 468 insertions(+), 36 deletions(-) diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index 10495630b6a4183ba2a0e1423f20a0dfa105b52e..599f4b117a93d4b705b27b968d06e8acdb8500ec 100644 GIT binary patch delta 64 zcmbQrJC&C=z?+#xgn@&DgW(g?jE%hfOw2%fvpiD~gfWH1kr5;^`39>wm=wm=id_=gGnlc2J%JI#n9R;;4yGMB?ZI?2 Gry~GUe-n%V delta 64 zcmX>id_=gGnlc2J%JI#n9R;;4yGMB?ZI?2 Gry~HmCKp}+ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index 83b00f773b2f5edefb900895865fbf92334a797d..261f76db03c2d68a2d3e5b9efc2bbf40dde0be83 100644 GIT binary patch delta 64 zcmZ1`v`mOMz?+#xgn@&DgW)UFjE%h4nV5m}=I2bjEMUfWwtPkqV{#^kIhbC|VGpLC HaySA2c=#2P delta 64 zcmZ1`v`mOMz?+#xgn@&DgW<#GzKy)snV5m}=I2bjEMUfWwtPkqV{#^kIhbC|VGpLC HaySA2-uM|_ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index f8a7a2f3ea799202d3c8f365ce9f9fde05dc214f..232827239f9d087f54ab383d04a6b48a8830c093 100644 GIT binary patch delta 64 zcmZqRYvAJz@MdNaVc_84VED>3Vk!SsGM FM*u>u6c+#h delta 64 zcmZqRYvAJz@MdNaVc_84VEC}PZzHc46El$B9L2Nk!SsGM FM*yg<7vlf` diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin index 544f58119f5cebee46e79f7ba79c16b2e0d1e9d4..df1b51914e968de3d5d11d2fa5558635d2fb5beb 100644 GIT binary patch delta 64 zcmZ3>zm}gjz?+#xgn@&DgW)UFjE%g#Ow2%f^IRq#W-wz7t0Nzm}gjz?+#xgn@&DgW<#GzKy)SOw2%f^IRq#W-wz7t0N5Oqa9SgXx`Y FjsS#06&U~k delta 64 zcmeyx`-_)1z?+#xgn@&DgW<#GzKy&UOw2%fa|cr%gz=Nbkr5;^*_O>5Oqa9SgXx`Y FjsWUH807!} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin index a24c27951d6a3f6b4221425704807ee61a6ed641..9411e824d71ee7dc85537e53b6ae02a036ca074d 100644 GIT binary patch delta 64 zcmZ3*yNZ`Lz?+#xgn@&DgW)~XjE%g8Ow2%fvm;X~gt3yvkr5;^`7NtCm{w=A2h*8s FjsQU<6MX;x delta 64 zcmZ3*yNZ`Lz?+#xgn@&DgW=8QzKy(wOw2%fvm;X~gt3yvkr5;^`7NtCm{w=A2h*8s FjsU1~7gYcN diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin index b35605ae0aa7ad5e5818014140fb76763e9210c1..bc079ba9771bd3e2624f4aece89862b00d193f0a 100644 GIT binary patch delta 64 zcmdnPzlWbUz?+#xgn@&DgW)~XjE%f9%*;S~vkr4G6PVG&TEz%rO#aVi4yG;H?ZI?4 GyCVQbJrlP8 delta 64 zcmdnPzlWbUz?+#xgn@&DgW=8QzKy&x%*;S~vkr4G6PVG&TEz%rO#aVi4yG;H?ZI?4 GyCVRtix-ao diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin index 5e9cd3bda91d52d72a2f5859be39fcf9c8cec3d5..2f3d05aa6894647cea8e2bd18d0b1319b00973fa 100644 GIT binary patch delta 64 zcmZ3autA{bKu diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index 0001d80f7c02a8dfc99aca62ad06cf37488741d7..62275f93c31240aa31d303cb4d84ddae0a7a821b 100644 GIT binary patch delta 64 zcmZ1^v`C0Iz?+#xgn@&DgW)~XjE%e(nVEs~=7-GlnZS%@w)>1A#^h8Eb1*%h!yZgO H1A#^h8Eb1*%h!yZgO HZ=*F diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin index b189414a13c644c0f057266d385d7b4b97e3bf4c..c5c4ea67bcc3082a60f23882be5f18fbd0c57fc1 100644 GIT binary patch delta 64 zcmcc4d!3gzz?+#xgn@&DgW)~XjE%feOw2%fa~4x3gmI0 delta 64 zcmcc4d!3gzz?+#xgn@&DgW=8QzKy(5Ow2%fa~4x3gmI0 definedElement2String = new HashMap + public val Map type2Predicate = new HashMap; public val Map element2Predicate = new HashMap public val Map type2PossibleNot = new HashMap diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index 8e0e0b11b..c56b54bee 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -14,10 +14,11 @@ import java.util.List import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition class Logic2VampireLanguageMapper_ContainmentMapper { - private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE - private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support val Logic2VampireLanguageMapper base private val VLSVariable variable = createVLSVariable => [it.name = "A"] @@ -34,6 +35,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper { val containmentListCopy = hierarchy.typesOrderedInHierarchy val relationsList = hierarchy.containmentRelations + val toRemove = newArrayList + // STEP 1 // Find root element for (l : relationsList) { @@ -46,16 +49,51 @@ class Logic2VampireLanguageMapper_ContainmentMapper { } } - for (c : containmentListCopy) { - if(c.isIsAbstract) { - containmentListCopy.remove(c) - } - } - +// OLD +// for (c : containmentListCopy) { +// if(c.isIsAbstract) { +// toRemove.add(c) +// } +// } // State that there must exist 1 and only 1 root element - val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString - val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) +// val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString +// val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) + var topTermVar = containmentListCopy.get(0) + for (l : relationsList) { + var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type + if(containmentListCopy.contains(pointingFrom)) { + //The correct topTerm will be identified + topTermVar = pointingFrom + } + } + + val topName = topTermVar.lookup(trace.type2Predicate).constant.toString + val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) + + + + var topLvlIsInInitModel = false + var topLvlString = "" + for ( c : topTermVar.subtypes) { + if (c.class.simpleName.equals("TypeDefinitionImpl") ) { + + for (d : (c as TypeDefinition).elements) { + if (trace.definedElement2String.containsKey(d)) { + topLvlIsInInitModel = true + topLvlString = d.lookup(trace.definedElement2String) + } + } + + } + + + } + val topInIM = topLvlIsInInitModel + val topStr = topLvlString + print(topInIM) + print(topStr) + val contTop = createVLSFofFormula => [ it.name = support.toIDMultiple("containment_topLevel", topName) it.fofRole = "axiom" @@ -67,7 +105,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { it.right = createVLSEquality => [ it.left = support.duplicate(variable) it.right = createVLSConstant => [ - it.name = "o1" + it.name = if (topInIM) topStr else "o1" ] ] ] diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 4a8d28271..c50aa7702 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -30,6 +30,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { // TODO HANDLE // 1. make a list of constants equaling the min number of specified objects //These numbers do not include enums or initial model elements + val GLOBAL_MIN = config.typeScopes.minNewElements val GLOBAL_MAX = config.typeScopes.maxNewElements diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index 2f3af5933..2a121446c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -33,14 +33,24 @@ class Logic2VampireLanguageMapper_TypeMapper { // 1. Each type (class) is a predicate with a single variable as input for (type : types) { val typePred = createVLSFunction => [ - it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) + if(type.name.split(" ").length == 3) { + it.constant = support.toIDMultiple("t", type.name.split(" ").get(0), type.name.split(" ").get(2)) + } + else { + it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) + } it.terms += support.duplicate(variable) ] trace.type2Predicate.put(type, typePred) } // 2. Map each ENUM type definition to fof formula + // This also Handles initial Model stuff for (type : types.filter(TypeDefinition)) { + + //Detect if is an Enum + //Otherwise, it is a defined element (from initial model) + val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract // Create a VLSFunction for each Enum Element val List orElems = newArrayList @@ -104,15 +114,20 @@ class Logic2VampireLanguageMapper_TypeMapper { for (var i = globalCounter; i < globalCounter + type.elements.length; i++) { // Create objects for the enum elements val num = i + 1 + val index = i-globalCounter + val cstTerm = createVLSFunctionAsTerm => [ it.functor = "eo" + num ] + if (isNotEnum) { + trace.definedElement2String.put(type.elements.get(index),cstTerm.functor) + } + val cst = support.toConstant(cstTerm) trace.uniqueInstances.add(cst) - - val index = i-globalCounter + val enumScope = createVLSFofFormula => [ - it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString, + it.name = support.toIDMultiple(if(isNotEnum) "definedType" else "enumScope", type.lookup(trace.type2Predicate).constant.toString, type.elements.get(index).name.split(" ").get(0)) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 1ea7e30a11c94002b34ef9db0ef8deb4ac2adf86..cab2b7ec882f8787a1c9cb7204c4ef73a7f0109f 100644 GIT binary patch delta 63 zcmZn`Z5HJX@MdNaVc_84U@&5yv5|Ks3p0@3yplze8O*rK{*DpEn0$=W97IpzvIldW GxEul0{14&) delta 63 zcmZn`Z5HJX@MdNaVc_84U{Ki7w~==y3p0@3yplze8O*rK{*DpEn0$=W97IpzvIldW GxEuj5rxRcR diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index ee06cb39699c181c4ed71a6d883907eb3604b733..80a74b4cbb47b363fe30ad4a261a937e68feb869 100644 GIT binary patch delta 64 zcmZqCYtiEk@MdNaVc_84V6fnuv61%)4>OS7{Dr534a}$)KFS1QOm-JD2h)vW_F($3 Gm?Hobs}Z{Z delta 64 zcmZqCYtiEk@MdNaVc_84U{Ki7w~_Y=4>OS7{Dr534a}$)KFS1QOm-JD2h)vW_F($3 Gm?HpZTNKj( diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 648d9600262cb4f9337492d0cac7885827ed444f..2dc1ce194361f6e1aa39f44c0a9071cc13f5190b 100644 GIT binary patch delta 13047 zcmVD=jREhC0S!<~0|XQR2nYxO5fYe@4Jv;bWRV1vMeM{#S%k!7yrnFhf#U=- zgDgKg0$DPWoWW?BWv{ZzD5FsJXv-`urIZ%RD$r79DYUGz3zQa0X}@#MTlYOZS=MMj z_~mDwp6>Xc|2gN*bFWTQ`+EZoy9TN_k7x4MY<8e69NxZtdq|BX;sY5qluGx7cVyLM z&(MG0dc&ST7e1_rCsc1^yni5-&Tdp=*?21H^|s{Cx+5Fj(H+gG;jZk?0kw#fVNX-n zYFjm=ym?2Yi z21L7NTmMQmsixyGd{xDJgi{eiv^$|rE3$vM8T00c!}ju~Z5?du?pNFTvsR4UOP&#LKYLJ-R>f$-G_Lernfs6!a8o-$j zaCQ+^RRRulS8XNdBtSC&&>jG2jIgc}fT(?ssq1?Mq09mZ-Aq8&4CuyI2wm0~bd`!O z%Z|BP0NpG=H?AVKwJwz{&9;9aBf*&sa9RP*cwt2a;H*zCDls2{*%QEo0L+AnjF&sq zXqn?>rUb$l27Ge>->wzu%{$ZtHISwC=0;S|X>&W(bbo1WF6MtEKzjqAMF42G zirC)fXgZDy3Z>bek(+=m24HOfZ1-}Ub|9UC^7=#V_+f+gp*W{?D}nIs1NfEzK3+J# zlFKNuXj^}*FP=!Wsj-Y|TSnOy?H`Dz)i(3RX6?nsRAQT&hWSiyyl+q&9BC^mO9A3C zfEW}+JB6`mNUJ1-mDqm>&?{*-b<(~OZDoG(SqQ>%fFKBfVTuqb2ZLc6dzY4tum~c8 zkpRq8VMFO)?4MUeW7$-Cry!MGgoaT@j0#|!=Il9(uV5{j@uCv*X>cM4X9d8SKHZK6 zKZORf@dQky6A5hvG&9!qtya=XENK;#G$WX=q*c+(*0s@rQ8|Bav=UZh32UH)JtpTX zp&h1IP4!#n+ zs&pt3?+!)HOqq}vi>aARDxGO9BCUpFz1QpYZ;vN>V$pPuhYP5fD}%ny*JLnH%;OU_ zP=j>L|7cwoiE4ji6uk*PYb}qkAF|c~Xj&>VleBvLa%Yk*B@try$JLP{v;}ivqsLoE zI|_0ln#piYmTFcfds9NEha1ynBxeePa;kmFXump%dW?AvUk9@qP}4QF{c3-=n$AoW zHhK6ued9t+^yE~t+2gCHuh&urD4h?0Sn=LCWVX;qFU65iTg?SpUt$NK>>@d7P&d)W(DQ19LpY8T4kcf__Wx^eU~IGu zVTM~aYJfG#YK1L4H?oV?Mbm@G7_m?vvt9^?aX#EfV$xL2o;8dbv?i`GJU1-pmLHl^ zBPkI!4rw0~Y9=F7Lu)kU0jX|`lF%9(%GVl#jZ)-#`3_d~*kb)e+xZR7(z zyw@wJT=iIxKaw2mS2ce(=5c#2EwwMeik23aJhWkx)V^BYvNF=y8R=lG(_xWKF@2F+ zZ+3)UG|WCS%$vW?hAG={8}_-C=e$Ck^HqiB4nMPt>CMN+J^)@nhzsgqX@{e3kKjBG z15AH#HREi(zS&rM>#T%AKj*Cqx3~-|u+s^l2c$uB`$yBsc(N}uG5=S9s!823029V| zmKt8bkmPD70EUg(G^DVQ(AQkeHZ2toj!GnXpf}kT&&0dqiFkHrjbl!fYHUx7LMe6WuQW#gfz!Hbd%v~yh0Y3 zpSxg4$J+sI54t`1Q^e>Z_ZU_x&7~OVwHrECZx%ZvEOw)x4OI8WlhK5yPU}Ypkv_fS zz&36h$Ma@(qo)XX>V)moS9q+HJ2jVIA}tb&ijf{&+`<+iVR%VG!5 zaB%{0aiYb=NyNp;`MGFH>%&Qlh;Jbgr+odJ*bWDtw>S;t1h7 zFE_3WLs|y2j(MlIPCarEhOB=H43N0q3!ZiZsFD+IgaSrrfNz4wQ5rA8D#il|;mvLc zb9V?3;Vm|Vx7rcjhE?B=e||vq{}7qc#@51*;CWs?0C(8cGuqUS8MFnOxf7}mM2#1` za2J$VYii_fMkDt)HF7Uv`Z4~w55M{eS3eRb^67X#2)0e7m8f|mwLyQ7`8HFFW}rrs zPP9L@qitf0Nlo_$c;S8|DWT13c;RPIWx&Mw0E6@AcAUb4DB(7Jy*0xNzaSPLf>evN z1i!=#g3e;QCEu^?7WZ%=fRES!{u**On;;%#06yjb__zb$69n){3*c|^0DQ_0@aaMT zpRob_E#wZFAb!UHeAa&f@b?aY&k?}qEr2iN0r;XF;7f%7z6=%dFpT7dKS0h|CV*EM zaDQ}wd({E%H3Ii13*4XcfP38z?u|m=-b8TGWDhUA1v#rt0BbAe`txIEfHWwh-=?2jT8^ zguy}xryzs96iCL4Qz7#t6T>tH-*gAQ84i4V5WblfzUDmmTI~2{6~Z^0G)&QVyx0nv zcQrBW$>0k)@P!@t<`BNQ7QT6T@Xfd5TTlq!UQkh8+zcZ);>Cqfz#b-!y%~&)92gfn zFt!oKeJqSi@?czQ$GEHz#^sYi3>$w%9+)fbFjv`OPO@Mc(H7Q-*e9+=&q?EpwA#aq zYoM%MOi25}m*dRI$Hu{KaIowkjTU*a9q@U@wUA+gBU9`2Cy2$C~l$=RPr&ZJ$=R8evc zpqxgnym+Kp9Tt@yO3n<)nRS(OkdbqnL(c6EId_npJ1sen$|L8|b~%qJO3q_Z&R#uS zmKVPPW$k7{`sPq_9!GK>?<#-i35=X4I^;abA?L{?=eI05Pst3le%B%A6%IMCBss6LIWlcljfvui9t!Rd+TU-?vace|Bp;6B7i40d| z@eNN@mLI0<;Tz`4M5;TQXemSt@sLRkrm^0jzSS5SO!lS{J*YVa8k|^mLps$n7|S-J z^S9=0rQDQUths;N$<~17Cr?wLtHQCpIJQc>#@-{1%eNdZUhBRbE`Hz3dByAS&-LuW zxZa`Mz;re@VxpVy&&~F3$LK_E!S8OxKet)kiCNU`cBGBY8PyMrwJ!08Sj3O;&mCqD zXq9s(1L-bIbT|IF#|@HrucJT2m1FTf{PPp)8GmZ^jQ4-L_Kb#TKf^o^;Gdtni1wge zw24EG3VvZ9wLgS~{u2M-+OPO9=c$@skuX7{?()L~T}pBg@W@bunO~!DkK&)lXjt>O z+ptD2=m|!-Phyte;Gd^lmHV_qxzAwI-{PO&k#e84l>7T3mHQm#c^?0~;G*0Yxqv;~ zLVSs<@rr*hbKa^2;o*l{Y#2O%_%mSc$1<-lLKN2E) z?lD?!`v(6A@l`C~c&mWdsDMAY6oA#+H^xVZw6J}OmHTzd{f0~KCdkd~DUT4}#H?po zS>K|pZ@Xk|gsj$n>ddiyUEo z`uE~H9-b55_4okhdp-|G0dT@M4H%B_vfN0J8u5LG>ss*x9xUub&R4b9f}(;lT!OY1 zpdow3k0?}2m&QQ-S490Wq5i}~eR3Yuj+l)a@l!^@wc_6p@@D{f;gCUQb}PvjWabtB z?uLK&ABgvJ!uy4Z_l!Jv+31QI@t=%I)rwyt*na`oy+gwcbjZ)_S8hoEjY$84NTn(h z>3MmOGI0VTG7*7 z&A?zc_yP}8zuG$R3k=1B)KU%4kL;2Xsn~xJ5%ZZkZL_O6R0|4F2?i|T69B` z9zZRp`q8ZUY8vK9e%=RV$CJ_YPBX;93^bMkT%c<4KErQdwKQhDT1MDjOzKdI5Tw#u zdQ!lIDyGw^?aiIeqY3sFJDrNDJ%BYc-F%$e0vfJoMtM>ls7R^@VWtY3$`9K%hnIgk zm(4AtbAJOna+DhQYJZoUNM!&K$Evdt4Mu9>YwEj1c+*GCjK%o~fY~M}~8#D-G9Co)?XCDdqT(nu6#6mCMsv%G{mO%h&K(YCOpnwc)&uSGdaWBA&p zF0F1ove~PB6YPX}LJ*ozj7L!> zkd5qLF&kmdFBw)M?aEhk(nK;TpJLbz?$7D5QI-Kn(=bhKjv7&u(?OH^5LKFCYH$y1(`Q1PzGP;h#Vn&WpO+K= z@0XfUKP{x6S$vIGn$7W5OKeH!QWw&SDfTpE2<42A{ZbfHjCGY@4)1U5THVVu=v=&4 zn#%`9e{^li(-_YK9V}fkd^?e}fE&h0l%kSb76ScNvmU;K+N(|JP27AmjRgQ}j|uiO zZlQQ4(m#;hsVRFeOtuh`?Jl&Jd(<_gk4tqs+8g`c3+>!;zU)>tDJ>!mF2=gspzcLE zLyTH!AIyEWuB~0H1301)w&#nz_V;hz9|0H*vtbhi*jFuU_u{>#sM-9oS}UB#Z0Bsy9K^3vG;(4Q)nhP9SRb zXH=^3--WpkFxry?*_{ex?jVOstZxp+8V`XQ_p;Tv7u9np)^m(r2`_D7lzbTGixNqP zRDvXC*0c%+w9#~IYus?uZo5Ipoc7g&2==As+LzYU_LD6Y7Xc5GMHOHHk&~tsF9D{r z))fi?BaBHo7aBPztyH9>$NIzj) zgTN5yNU+SGqOaWV>MK7ZUwOdvm7kNZm}nj}ec>163;6VqX^g+5K`K7|3XSm=2JOS} zVxG+yA3=hDO$0wm#)$bIf5Q?U2dXEQXdb!eQgY1W39Rx-LmPM|VV=`Gp5hyFE#hee z{0ss9Em;H>_B;IefT8kd2|m96J-&a=sO0(FN~9Mkg`3J>M3ui}6>K7S*{1S8xT@Uc zU=Eh~3ab2%y2?@2Y-{~02*pXSnM(hYxdQQLMDaSUA$3)7opD8~e-}p+gNdlQi1Y@s z`zBf6TR3!n8!8n<=Uscnt-@K=6uWY0<;2B9+!JzLIh6i_{JdkR`CVKte2?=0@WrLp zXS2ii(Vjj4CT8cX)7MHLqK|DejpHLs`&UR?UE+?cIfg`!A(2VMkFlCNO*=F813p0| zeX1#Gb2;R~r;b!2e-FQZBYt%@KI3b>)zKaCRKJel?}*_a8iu3G#9-KC@z-z>(9c<* zUw|sa+wt{3Q7K=NQcAm|+NKl=3D>mpFPm1N>7mV~yER_^jkW#<=AP4ouJ=WSB5OBv z9#?%$2=(sfIl0b75$k@tJ$CZI&dt&OF^ z`VvLS!qmASsVTnnywDHNw8--WVT>XDq{!MI~t=EGa?6ZG9^zjBSqw?u8|@Ed$dxWJdK^u$kWjx zXB4u?J&358Mu#mo@@}Z@c4=o#>4=uO(kbpiU7V;qqc#vh&hZOu6sdz(&mlB&!v;v)I zB~`qNoCqskjUU$-2D&dADBh?jM9RBf6e}+BdQr?`Gf~{;ka3$sSTW7TMEj%JtsyDi zr>L=be>4$vd+9J#+|iJ6M`J>9n`myAJUc9ve|9sTDPXA`HcQ1bW9A`pxs$QfO%6-l z?6B1R$x^#4OFdwCmU^JgQV&8)J-Cpi9zq6lsA;LV`5_-hmU>VHEtNKG*QtFpku*&< ziYD7l2x4fmJ!lOpoj?AJ1;YX*f_p;MbkfBkoM|O_Id=^9o;D)oL!=0tqfXQ4JLGHeR$=p?iw42hRd=9udr8Zb#>n9pM)j;M0YWZG4H2f4n}O ztC)+hwvQOaT#SnO4&l7SQp}~8>|;&T%kcTrp%rsEkc?Mf$anzHy!t}Eg3-&B4!vCE z(96}Nm+x76xn_8Jxz?ta@1tI>E2Nj}N!}aGzUW5$cvHng67jc7^i6l_g>FW!Z@~pi z`Bv*4VxGIVAXb zjo@wN5L1=|zhE-+A~N$5e=$>H!=^El>%T8Msrds#%`3UoIQ;jII2gi9lVm)?WL}yi zzs9)lpB(P{XNUW~PVW1L<-TtY&wbyrx$oQPzJDp?zVDFxzH7Sgd-(Bva^IphVG6r% z6z`)no%aKD-Ve!nKSJBWeI{Yw@_uo|sHE8b#mHB#<9=+K=O<{Mf4G;`D6B2xrx0Cz z7k9A42F5@?!xv4O((&w)IMVLB|3H2}*Z9qr&P-XJYi?l4xPc{qNz|+>lbT%T{g;!Q zuNZFroy(2GdH;hkPx_@|3SOgTUMi+|EdN!!cK=m4yZtp6&t z;J=E$fd481^k1b8e@Ip8b0;&4aWbPcu#*{|(#XUnDovOZcbyta90?h}C7LsnbJ>#B{IMFd*QFZ|ytvk~cymHMv8la426fn-Afbk9mOdtj9YAImi@Dwn~ zrhv()fZYlyV0ThL5NVu}qkwsHJi=jkPlJOiJn zY0rD$^9=2ICg14w*mcp2uAtuzr{L9X=IwCGEJhQv9hzu$Xkt&&M99)aczBwaW7EW3 z)Wp0(nwU?Te^@}8_@B_em!0;7EbVygLY%EVFT&?Nwdck79M+!O_(nVF`%wF%U3sVA z9dPEAcgj+R^kojxmpe!oh;-2+T^b(gvW;{FNskmFeFc%elCSqFtBgT}g4+(tnu-r1 zj5RW25TWb~g9xP^2NB9z=;RdIPG~Q05MfkO?5?4ae@{Cbs71-S?iwoVk(~|tri`*5 zkgnj*E(z^L{!*GzBin~58`1nbbskETfC-YW*t#HhLJwO_lPQ#AhsB#I4 zrgIO<{s^rLp!tQaiv4K2cAiDM?nPtZ0KREdmmI~bjF=#D`rQZx_gxw_=c>`JLQxJv zR0jj9e=#NRnHu*>5*B!^?L;YuVEeI`W8~sh4#f($Ba(Ln%xxj!+3VP!G=Wd{(H#GEz2}FLloQ$QTi&zje?}B*Z$ug1-iTt`8&Pm?L@Bg4qR`%m zf_o$4gGj^ksN&NLsrU?1@tH{PSvjXQY1cwIn`cgIa>_Z#z-q0IbMbkdoeiII9*(%pyH*wa z84UBTRpos6GT(JM$_02yj&h;fB{|AP41*Ut82pZd!Apq2ODzU3b7ydf+luOx%WZUi z7wNpB5S>@ju;D5rL|M7o9KGPV2j!ZIe~(_+E|nTYJUpS$;R)qB9KGP-31MA%qZgx+ z;$pR|d_x8&D>oq48;y|*{>FoHGmc!=6*+P-YO{@8ZlTa*vg2EAyKl;EX!ExNJM)E& zmAV?r7Lu&|0KH?gOAl!o?hkQ@i@P4mRV-|uatHd5c~h2hC&%35tK2n|58X{Ze{_$l z58cc7(2pHHbf3eA=$0_Wx+P3;za?yFANrZihaNy5`gtKAdQdx*Kqd@eLSXe>{($wp(_{7$Xq<0upUrGOWDFF_#Q0FAYWX%S7}a zT#0^#A=>dP63VL%qUl#86zf+c6!%||7@FwUZA8C;M88>x=(h}GdmA}0FXmP7-YxS2 zV&$EoICz&hc+ZuC_Zbd8aB%RUgM*KVgTGoFd|UztpV&C~6gl`?Ar3w>e>nKNodf*g z3G;Gd<@2F9_<}h2rz;0vG8{O5c0&2e!2$j3gkt^dM8y4PCx+x8;$b<6c!7fmSAc^E zj}8~{fx|_rjXpb4Ln{uNmqcozV~zN+e~$!cSpZYu1xJy3z3+-N(5#zn$Rmw3bH=1i zrf)_@@J-&xNY4CSAudA8f0!4W*}Rd_kUFwU?zwzAQxh43$<5<#j59~Z0{93V8N47KG$Yf6~=N%ww zb|cN~Zp`x{c!f=5vOXG(OtF}V;DV)ig^d#4{2k4WJCoVy4)+-vXjy+`nl^0JudI&X zPgIx}K}2Q@Vf_*OwF+-!rknLgnl0;(wAigbGRtoLk=bbdkygw4_bkEsL!A8{N4{3S zGO(oU0;{TM@$vrvP)i30Q%pAig(Uz0o|6CoP)h>@6aWYa2mlchn3KvSCx6Xz97h!& z>uV)hioPsaNVcO`8#^|R){;!YJs z6$M4Xfiq|BzyS^v;2gQ|7w`vgg6`Sb*`1m0*Pm-}l}FO<>~z1^@ALOw_x|=@)?^e~ zkAv`F2RWYGj?hjwM%{QPM1N7x2_3Z4Mq%VeG4k>6pQ6yUJ@*T{?x9c88y=#_3Eg(= z2L5;d^SkDE{_>;EIm_y{kAH3byzSX>GYDIEYW>I69DAqb9Jro`$HRj)A}>UC6!<9I zIkH=AH$*%A7iv-H;QMR6`)lO>+R**A^!{4*LcQa94gB+2aNs(7&wqPwKePRVj(vbW zw%eE#LY?2REb9~|`;h|KkG@g=969k2)h{Q5pZ)kJ|Nc#n>VI0l{C}l-yS8iHKaAt{ zom%bq_&B2+bD@?{Uvq+1EAVSi?IZj7$Df_FQM6sFJw0kYL3kk7NnQ!9mCy0}JDu3| zb{>SGeew+Rsr$n(&wu~oPxi0Ity3Ra6OsD`>b5bLr;jJdHMYhaJGQ2JG{x2gp(?gc z578A{m6WpBnjU&Fr7pHM0s6XlR!f6fecg@@@f(wsfBgQBYu|r4ZjC**X1%~}Jhq)U z2tTrB;zPVNhk@7Vw(s4y$iKPcX?$HIk`Y_uk$VtZTf6Tz8h_VOeXntIZ-3u*>Njj> z_j==2bN}7u{{G%OsM}3GL_YI}=!NwIix4}NkUS+xa<%_rH6^&};8$XFr=&y!0tMBwKsZIT!*7hyB&lyyJtpN@lQ|CHg;q3lbD9gMp7dU8L?a_ z@Df`BJgL+e#3*bD%&lker+WEQrZSVrBdO6S#NaX{22_@09xoaEYtm8xgK1?m7CeX7 zplyc)My4zSRY0yAAg;H*Z*n~mBWajtc)IL{S(*+Sh`@plX4H#L5YxED653567k``1 zj{Nyoa`_v%{GD80lFOG&fi-Jd7D#y67?cv!bgNPd(79Y%8dB}zhYND^I!kU!A2f&* zv7M}_Fz018n_7_}=h$ci)mBoaxh6y$O-nKzx}{>%T$*)c2rf*)W$E!K&>hQA2*)2w zfH^X&c+(A>n7O`V5@gsA$&`e7v46-GM(vrda#C=`1RbU8H)c2C|+Pv{#v5+lIj3 zlIzt&ASxnJBE9$|Y@W`*3x6-;Md&l3O!+mI&r+PVNKeO-NNMGYP!9kjt=H}Q&*WgtWk&=2AiCV2z*yhuq_US=UKtX%0nK0*(*PMA0Tx_g*MC?gOW7i>%xuCo z>n6+Spnz76-lUXifH)-Ik5f6cqeIMT(DK42Lp$nPV77=T1uY@15d;u6$ge16ChX4U z57hA4vI^y8_pbCaK@@puAW)?hF^KAHgUu&qA&|kSa|vM72s&}Q!?%l*SPLV5r{rCw zT#sp+^AEqT@Nh;NXnz<->RTBYM^X}cnt(D>sW&7XpkbJg%u_AaX5o+uRF~7}Ek1eUVuP zrXT>H1~IaMPXKZbL#rZKJ<4~*&-Z3r>b4eU{A;Y1FS#dZ+J7s7%vP+sy%c*0ld&O! zBWAPNq6D41&&&-zq?CnJ6sLbn7hhNNC3(}PmolBE8g{*B&KYU_ z%_5Je+W&2rveNgpR(gaTJIjN}soV@`cBuJ!5O~hXwRxAPxF|=-1 zV?Tm4#x8Da^M5{T8a0z0#IzD!8iTCmEh|vdOFytu$o~~l*=1;BBh#NPLnYWu8!v;n zyCCokg`6NF0z{}XWha_v;m26qo?E4@d~^M+eEB3KW5eoD9uKg$Jm|L6{zWw$c%841 ze7-Wv5ZW=tGL(qQK%+I~WL;*It15Vd;Q@e-jnqgjLw|ej4I)c#b9T2WqkU)0?GjdCG12Hli zqDnjc?RrFNEitXSC=+v<bDAiiXuF>jKzBN+##fIB7CIf#RY6z&rwcc%jWtA{QHVW_AqSac+N)Zdnx#PoZ@nLt%1kSmvn}!dYSU;c5k&3d2LN|h);GhbbAO8ojy%m4B+4^a z+F;BJG)U#Awy#}ZPDQ^EBg-^u0;n7CdFnBaGMc@mfSuFvYbcc`^LV0evl$9$)H?~c z>Zk}yNZaoykZZ$O_y~%sG$}M}_i&tVd!yTvmq*u3?8Y{a0xq&;+F!fUH;D(P$LeXyG~(;D|_3nrANz zojyul;Rdj;3elNn<|D&O$yebb05N~(9NHmSVJh4R;rYX`nPFN-jz(FLSRwwLK|Hidd>3?B9lU0W)Mx4Dn%TOQ6CBHl<4CiOrMu2kGW4M3K!j6L$z9H8^H)xU( zJ_AMwSkWt*($ubCLoWRfztfpbf6>M-3T)la&*vSztt{Yq3#0yq!5KS>@O>g3j}l}m zIfXUh{u|a4<~V0zm^qk!)u7v=9=XbN-Wwv$m$fOz@3iXdQklkAAJR16a2h!H7C%ZF zD9$c06lB8vhJqvK%<^>q3s6f32+aT6uj>u~0J((#08mQ<1QY-W2nYZX5}330G&T_l z5fYeAQ%pAig_AW#F$ob8m`=?9+pp`BZ$=dXzmtVVBLfiyKySo%Gu0;>DNP%+S@BaGkon-%* zWbI^UGRf?<_L|#x=&N{WG&Mz7xX(~XNJvm$S`(7d7=g`D>O$s594c$*=qVq??D;{r zkZkdc0@7e+Liu^K*4buVed{!JdcRidj0_D0RBK#2hL+C;I-BqcsAa8tptHKy{CsA| zR`R!dE>%_Uw}p>fkFze_imLa%;0R+F?c512Ye!zeMLcwuy?)`+acoF%9FaoV>#$(6 zL$mF<3(#k-T8K)XF@aOv!Lcivq+rWe-Q*;c{`x-~rpRe;tZQ~m6?^RYlp5F|=Js8X; zF$lmG8~4=#;b5&52tj}Kq40236vbAaS_QuT4lwKcFkMca3`85QgSt=(dJr5dp~+tU_&-e?JU%AkMC!`#Q8yw_dy?}#k6+iIdl)S^5T171BC%lixN<+ zj?zvp9^9l8@Zrl&3zN!&c+ic!Q0;~w6~QDGao_hMueV0=SGC-g?sT!|M|l5OXmYk( z(<$pTz1BL>HGEa-tyMjlHkJ~n*hh@f6^EP`i|zU0m{+DM%b|N5AB-wnDlZmyYU6 zNZ~y8YtY4eC;wLUH+?hkFS7tig0oz6*zG){)N-JkVGhdG6K zj1H!-chFbe#VdrM&4%GcuE4bR7qfa6cLRaw%1Yyj{2I z917z7ZUif!OPyj)VYi9s>!ZTIaU`kjS_@O{$Q25E?#nYwK{A0HnZjoB`oY7`&TA0C zKEguGGYGb78^+5g-ju#9z7V&H)2mF>XA2wQC%>WMu&=gRAd*2dz*#5AC&v3WgE3ci z@AFNeM9#ir;;hbgOSA#=;bi;t7v+36w_!8UiIOAGL^z0WnY~c^N^vkOpyvLE_db|x z_YzmD{yWJexjgz~4S0a~p;I_BZ42K_S}{hEY^zb;!IZ{DAM4^O?i>5sMdM_7R{vxj zpP&RAkqtTF>71$UNSbpe+Uw4=hY7{}OSObYWWnax?^8=la;OIKQFzbB))Dm%Sy!@1 zXxdHy3~4vnb7JoE)R8DEc+d$qG>X98xCmQ>T`uf;FS)Q1+RV&O`(P6LQF=oVgls9K zh{k3n=iY_`Ju>b@q@gEw?pSY=lM#a`OOqnBnBx>{d-xL~CDhX*!-ZpNOq<{*e~I#2 z;h%ur;A-pcN7aq?ncz$SuD(l|QsaB*W0X`z_o^s_ep+KEo zFlH}3x(;eb{F(p8VDT-v2ZJg7RO8d{Ei}>^-q<`Wyq={6glfN|DZ63Kia#Zxas|6? zX2c!wN4{J=OPX*(p2J?hn1pnuNl6TjRMIfOp{%L$zYp0#iRS*VS7B(3LI41W7{GT97VKB zJa}75cv~!ZKL0$14Z9(mW6_*r(TNn`!zksW_w9bYXu|LiARZGf7#;X`$sBm5f`7rb z4}+$5`xiREU$gLpEL&MNHG5a9+tid8brp?3Gwu_e(d3W#aSkDWa^)-!43(V1b45r0 zlI+lNBYfxp=Tp~Li~59`=%p<@Hh;u^11Cl^DPx0hNEfe0PuNkfPUbvvW-&JKxh`(z z?!{eW@`tHqxSCv=2<{1Cx_>6>T`(Hyr685NtrSFg!@~V*&LBMh0m>Igtq!jFaQu2W zm|w~Y4Ix@T^lLvoe{o<|2)`YQEz|kAF7~rLPc_Eg<9%l_T4|8U2z3lBfZM;|;1=eZ zmr1-APQenYKhe8lSV0Ctl3arW5af(*;Z=K}wWg5yB%rCd2l2r@7|z?}87)O)+CJ#H+&% zLQE|X#BG~?rrhd!#rkz(4$3+~0cc%0%9x3qP~;v^{yWfj$S}{P@OON^P$Jfd&)+D5 z7B-;%;kidDVGdYAiCjVf&whx5XGr@Gc!T)&Q2tBkcV!Y#rV%kd1Ty!-O$FR*Bptz8tmkn}EJChIz_| zzj+th7ikQAZN%(METm*jKMfy{7}sg}mq_STz~30~Yw(e8_%S;ixW4smd>=`;evsJc z4~p^M;CL7orMUcrGnDzM8vrc^oQOTSNIa3_L81d;s?dgMGKck?ig)Ia znm1w&S52C+!KXkDxhI7-N7?g+_(pJ&^W{Q1^O;o=>+SEc9V6Y?YO)UlB+E$ljfF&;W!OX~FqO%oq+*(cDG6KzhUmAK^&rAY~Fe?SN{3@slb2bXz!55%< z%Uq@1jA#jOEoy_VUSdK1D7JNLB(|ogmV>sG=kCPE zFJjyUc1^O%Fm;Qz_9g5n8TA2Vxa4Xlx^nXS=6ClapO@6lY$Mxq@=@ zc^SE~C&>?XJ-HK~Y0jGHZ5zl~XJYq)n!R`^0zBwJiBzCO@AL;anRy&i_x$6e2dk6^ z!;IXDWXc0`%7c?GXus*Z;@ct$DZCs96NBkuIgXYKdwT1J zBv8f0Q}Cxlykq0}%h$f(thRF7#r(tugaq~zpAd2wH0kqt-msQ+uelso^XA5%Ske{> zeiAK&MIEtm&l+2hHU*sTF{o^S7~^<43?A z`mMOR2~W<}3cSg+D$qKJ3B^IP3<#5Ia!Ngv{8?(``Qnr^){*RE91CklP2!OkNy{yt zXVvB0dscl5IXby5i{vOrwDtXg5uEgsNCv;>h%UJP`<~ zeN|Ez4l2P2bQwRBRQ`M#Z=O4UtMfHv;G@BJyzy%0F?*R>`FvjO>co~%huzThBzN?{ z5*fSR%@!HE_vCH@5qR?u?qRR@rsreNn~Tpnr+xEi>D%TINH)CdF@!7t&N|)}c%D6^ z_9Y%Ne_$=^6yGTDAXIN2k(;mvCp%MO-KaP}wa}2i=y7S%o%`iGJO%EM<4`*^a9K?N|5AcW)R(`EYAXm!lZWxfj_q!zS z5mFpdwh^{Kotr>^Gl3+AP3HU6W^DHliAwn6qVn%D?(;D2tFpoaW`7>zAy||wP6ZYx zfqCu&2Pr+s?p%J;RHJ+xm-;$u9rTymtopG)^W@luB|Hms`ws4I~o za|D57+eaq8(hr%^5Ajls^yuHcLUP&sQAATCdaiZH@P*g_q8R=Ss5dFBH%_4!Rb}d| z>g(!omG+Z@FtAm=vUd=HE7;s8Y%q6lM8iGYWx<2g38mn6mex z#Af`^A8ybIC(Rw5?xHg+p2iy0x^ZQh+R{RjVIPMkyDk>np_S8~I))R4kK#z*WH^r& znXSfdyQdVK&AQhh4N|mxN$td@;_-Fp9G?v$f(2sjQ6-jrcF)pbHYk4;IYXxOUO!iQ>{+K`;t&DTe!a_IgWS3sdq+zQi$qq6Ip?(OFv|)Y zHqdSsE}GOcpygILl${fZ)Kj^{QvYIVgY6w$y`5H`f_MWUWZ`%%acll2DsKa(4l?hp zNr5&H9us@s30;?GRA!K$D|3+e)Da#KfMJoB&vA zV^Fme!uZx`1-ZMHT88;bK&2j|@Kqn_x8dCPXLN@K-ZDP7hb3-2sM?=&TMM1xhuLx; zVqO*HSAFc8yGc%bMSVLZ^%Ma{)!R!V8&4*7XBiLH9o6#o6!xxIYd;Y@*=7kXRux_? zZdyE@Ip~8X9_q`jf#8x~=Ev%4Y#cAxJY51JbVl(@bHWKacWIHFO6%#@~f^PtTogYH+ zZ_Sd2SWb|bv53_2TV0K=B> zGaSSVPH>JVPS|qhJI`9_|GtRSziRXfmX!FN%8H8*jg~5dYX+U4T7k<3-QKc}ivmqG zI|ah0Aoy6PcoXzs(YU=x@4 zWoUplgq+55)ISk0M^1$Ok*dI*xZ}Y9I)%XLyp$H938k_x*psP3(7Ny-+%SO=P#+o0 zFsQGjf&PPPFD-E7dmm(bqPAN1{$FX9QPYN%PuPm5O`B18v3i{}U&xKLZ`|1tXZ+!{ z|H&GkR64Y`1>%MsmaZ$6eM}hzKXVoP>7z=@kG)j_2GoxTwZw|;VX1OVT#C)wAL;X z_XAB?#$+IJZvbmRfVcqCw)^Wm!Kd1E;?8^Y4g+mu$=ZVbs_EIW6Y2bnd67*F_wf4p zZ$V`mn><6Av4*oIN_d!~!Aqtx)8g;N)8(H;Y#-wWAFv(^gyQS3#S+PF!~z%_%{rs) z2KB?aGkGXBA5&xoYh$A(^aiKXCPF_p*9@$(WqW~^rAq4png~{~QT%HEc>m!sksWgO zN}xN-MDAni`PN?y_&s$BEQi`G=Xw5 zMdHD(nLnJhTJM#b;w@>}Y9Vv{MWy_>%BD0*XpTpN+ALA0I<=w&hsYPf;CNO7uS*cC zEpo|xX70HuoPN6@B(1KQ7yd+lQFErHY8TM43px>Qg3icYcg9;!_{G;qg)!!Ax7BQ+ zS)bi)XiFK1>8^KMdjcA47s3~G)W@72Lf@HX5{Rq|&xza>A-C7sslQn{jh(99swl5G z?nSoN1jm5^w!!Adkmm994R^hDvh5xcUl%738DVt+6#3S~siaTJw2&Y(n}vVn9B?4{ zD&TL&@v?|L6Pba&5Sg**FDFKhjrxKKFErVFA&C+gr`20Dq8P1AXON)M8p3EIuM&pa zFq~L}25TIO5W~lal6+r}KNb_)Yx22eL+Nt|$ZF>lGegyzW9grrm!n+F6N3ZuF1a$? zPZNPpxZd1WJ4;!5JG9_!ngw*lGT>*NEsCB)xT^AYq;3U0y*4J$=b`i z^E0zwcoW!6mVT?^m-Y#y^^rk)$$Fzq`f$(pYKq<1I`LdI{zx0qL7dd7Yx(N_-KQPg zwCRB7?Ae%9_mxUHd`_}Ku7>`k2D9JpWs+>Vpx^F17bkuh zCiR5*CiQI>C$E*6mnat}-&39tTG+a=M0d3yNm6gu*a0hf--~jRFAZIXH2QJ?DL%)T+ z_hZ?30*)TT?$YN-PI{8Idw9Nb(X1>7LrTi--4mx~`X*-*qcfKyVi4F!m4s?!W&>0# z0*5glR*Wo2^6uaFgSOJyIZckOOpvKW2Yu>}DCu6rBiEOuRe*cRjP-8Q|IJkDcVlyuC?^OmTAqh1E=aw>qeMMVB9U;S4OqQ(Bo@=| z`}j&WCQ>#glz@$b(+0PV`}>nM9S>ku=}VJI6#4NF3sKU?J|#{zYgRG!c%9(sJ#{4D zW$$lt&;gu{9!;^`9omP z{3`|MR@Tn2bAh^+;TB&uP9f&nG|vA-;AW!SH!$Qh8t~JPAKu~&L|OXb?S`o6WcKMd zm;X{J1L*>5G}U$gE5`AYNBo}C#cbM1*C|3q9I@Vgrqo)PSZ zeG(;jC^cm)-{)~SEwhN3xHlbhd@>Dhd2JXj`Ct@T0n&e&zcgr!{B6)c{a5ph`rLpm z_M!bN2+%4M@#btnqT^D470iY(#49-!FNcBL)~kv}lanBZ#h?}BV}KigNf)Z zt{cMWRFVf=>rZ!fKeNmC(;ZKjpsYzsf*|PdO0M)~lniG0iqNSM6+u(H@JizFR|ay> zJ;^X3a!0Eq@UuBbSm+~u3bmK=AzLZd>^TNy0QX86)mCiTkWXSDgB(U3)xIz)A;Ggv zP6esItIcC;#^OPhPqXh9*@^*r6B+CT%*u)$ye`vDXX(n}Jjmk! zsB$0G}_G&=t1kolGeh_E#iA=>W{F?xNn;@MSYW| z3S16Wuk6-TV4z}NG8&s*{N6yZ9~t#$TzEZh!b=09+|jcA2839fReb4Nz04+gkta0w zz@l~&x%2vbi`{yk-6xVkzW84$B|hm`I8rJD#6|o4iY2E;JX_lI)8bLT%*1$r_G4kq zBNO>yn1;4I`V&ki(MR_>S9fzTM{vt16EIP&mPR!gMOQ2J>Ot%r>1)!v~$<9Ky{EuDWbb&gQPY;lpv zU|F9LJn*Zf9LZ?GyHInxNNKB>Y55mRj?sa%l=!e1*ObFzUX{Z@j3PgP^1~Iiu?l<* z2w~|VSMqL)yNcs-eYiXCLhjmennzNwwgKtc;e&u6vB-%KiCd0$9pf_>!Krc0^vj)f z|D}5x>Rk%SiA0B@ds-|30-G26Gbv(dCT3`+!6%c``F+d|+#d{?+vjhr%f8YS0u80+ zBib@i&F*cW??WCK(>%BUd0(S3BTtl%k3`W3&a@~0_n{G-;qH4GHW`|+F$evZh)*gy zU&U(qh^X-2;t@}5NV;m7+>b3*ZHT*eB#Nf2COWpf_R_W&PhAkbPEm=OJbBVssP$i< zzfag?k}Y%YkRM{=dkd%4=xvCcp#P?LC}%!VN$8r;?Q*0i@6PcD&dGGiyE7q02}9-xNokD zPG-*k+!h)tOG+XnLn8Fm?M@1rM9BVVpKo$VGo0TCO!7?FiY_!-^u|ipnXj_Uw6Nv; z_ldi-+$CS~h?u<}@F5d*?zl?gkooc#o_ed-O3ydhl9f=$gec}bGx}V#6Z;)Svh_%p zI!%{UYNbJre(k@w8KC6gUTWBm3WSXgY{6V|Asm0?bvHAat=aE0JcS>f7W}U~R=2x+ zCd6AV694`EeMv+_ax6rkjsLk54qc?l?T*3yu0w*v-v)5K^A<#W9>F<18J#}+FAd)9 zPE{AZ--_S$?JDd(JrwruCi2+d&FHAt1(i=z;-e$(m=G95ta>O!EHYBoL)gezE#d&L z(g+Jn|0= zHAO@uLM?LEP#P$x{8T8Y|Hqb-I!i+b%y{g`5$e7XZ8xnqY;bs`{26bVqO}rkYKd-{ zx}nv-H`ClK-Y_19N8tvO85$DVQ`%oa$SR9FHKo<1#noN+XR`%egJ9vU5{>?Qz+m~s zJ7h`-<$s!r(j`?-J}k<;2fPadd+T+3|7O5(5|?h6WLIA%Jhrj6F2*Z~Z^P&T6oH~p zuPyqx9eNp&z;^}|<86&Yiu8;RlD`q22U7AodFd(f+8aG^b6|}1uREwF8mMCSCtp$*gsn}VJ-_CuTzwbB7+w_djd)poKgc`-00`Zy?$KIR zVr}%~JB;Uc*38NT&M|?ZWdf<8rZCvTF+>g5up;t2rcOaY-$@xGAWH+^Fb68YSg5*e zsIvd7Y~*w7)U;^e$3)xh07=Id4-o zgsQ>9QOF&`!qM^Rr_2!`P<_ku_2&9^Tjf3C`pU#*$KhsRduMOY57Dz{Dsj@~A7)=; zpc$4$1$IgWwS4`fXl*&1F6obHQ;o;--Z5&XoY6q3j>Zd@6=U{AO0-;9admO%^w@4OkU4ve0_52?fIpWX4MeqRHk zb`x$f`-+YBnTy&L>_~ITB1yUVJ!wIn2snNlLl1f`<{IOMU*i(%_n1=zFR-$Q0YhY+9WP=Rocc$qQlQuTi{cEKTFCJlOdg5055&OpTGN&?XQ83AgdmLyzxYRAk7;*5a=D>0?6J4^`%0QBtWmo)|MLAZ$6)juM&| z?OXYRSDUj$uj}9Qae&Bsjp|dej@VgfZS8SxlS2=|+s|AgE^2SK(KTfoA){J8pH%jJ z=^?XQL*YPaEJD=}Iid>^VjJVLzi|cu;mt!1;~Or$;E{`Hryii`ZKt?u6>VY{40Y*xaRC4bTAD zy0wwjG1A@vDPW#$bXY_lfrC4!Y;y+)k!=^23kRFAoL2C-cWC_vbJY5t_(_$pgdVyIhif zQbP|5{s|2V-ZC51r?e1)e%0QJ`fm6y!SD+QAiHgf;ADmsG2Em}gs988+Z-d+Q8}Vh z!hBXi^NjLP1j@$3P{KdOIHTNOo5H*_CxNl@5-OJu1$2Naav*g?(fv7vq0vTp1_qgp zI8-A9{8d{4S|C$VQL@_j%}xBPiS3l~MI=HpWqT?v?rCqWjU*H2F$uAA;g&)*_j*`V ziM@QeWQUd$Sg|GH(@;1=Cv$)(%C`y5&%=-jY_o(}#@%nQbT;+3S#X5BQk*pACIEAD zxVm3yP3~tSx8Zwy4*kEdFk*x`^D#?e`tt>humN&^9jECl^F85KM4OX5QM0=ETS-fK z1AOJV9EoV7Zq*mVSF{T3yquVpQ@Fw8e<9EPhmu~+-Pg{bchz|*IiIEH_Xm% z9b&xZ>^zU!MHZ}zJ7~Tr&7INR)&L7tOj_+B5GW$luHe%MInqdrmyCG+B_1;WblW>v zPlU|o%aGYy0!FQ`TqSNlLtb&=DZ5qxlg1Q*5ENDY9D0j(I6W4ddDmo)$i}cg_4gV6 z>8UfvEjvbJ=>ML?)$yxLs)K9K;IFk$*V`%XI*z~p!HkNLOOs<0LC&e*x&uaMe6aq? z(Mtx#pR|0IWm#TnqSi3zqFjX?l)HS;^jGEz$0J68WyQJd(+Dor(K3LsCBeYSjU@3T zCX&MbIeUB@sfnzf`VGqr16XuqEQ@F!e{+|w`qVSJ{D%uf;IX*`B^t&0M8|&WEl_oJ zQmz{@>MX{UHO4I_BO3&-y8-a%Olh=7F>&QI&UH_53(yy)m+&!I6MaFSdOFfVzdpzG zAZqPxoLWri#>--%R1jB`bA*EqL%U~E$VTpId4c8eZ?Bc`-RxruP{x!tAwtr!m-$pI zux<7bt&e2oy50rH?f{q9`SW0VOujZ8Ye4h9UZZ}Zb?zm0Pq&kw3Ju_nqxw_#DUON( zSy)*tyK0pf8-0;|R(8A!&#}c-4xVvl&7^hAX&S?#!#9M7+xK9a;y@9q;J^w3HkdJ^ z)x>E1&n6|K^E<93R7HClYCb);o@~5zP|DP*JeUD#ut7Y|X&)yjcVw{^Nhk5%81m4E zmDybvPWVAobE0^I0tOxxzO>+8eq|dY8@6(a+K<|_Yo`~dyXEr;-Rq=P?@^}66(Js% zWMQzTz#Ti-TOM2g;V-}2dQqlSQ59i)3-*vP09q!gsvk|SHEjO&uPG%qTH5+zg3@!K z=XM?X$>7Mmm`dia;5q7~GRMC- z`p%%N{$3`p{d^BdYk3hGY)t;Pol!&PT^XPGa>I%wBuPOR6$OP=t+W|^s{hP^*Kwv} z&#-3%Fqn!UPi-^`q)otHvFv>_ba*c&Lhqf|l@l?|wnnkrG!W8vqe&JH%2MyQj5ZHDzAsvkYm5D{)WpVouciF-{~2d8=#|1HkTf7zSeb z<8rwg43L4esgA2>Oxt_Ur@~;84jQ-?r|4HdXQq~MN9bv%m*Q-L&xPYo`dAB6cji|M z2rnKojishI+ZE>D^eJpXnGtwU<_QEpxHIQiYVcf@^8q^A)DKNO2w$tfGVZ>bjkeJe z`@-_K0`goaM#FD$m*MAmq*e;Qmdn+6WCZr{(Fa_l#SBA z^kfX)$#6kk#eC*Jo$u`-#xOOPod96#BTt`JV#;b^f&6n=v17!Ny1qt)^44AB8>#dF zqLCAX=J2SesdNoyQMu(#BHJ5`O;w}^FsWv^9bhVn@BDu8CUAoL%7XG%Add9ubVokL zUt0)K>{kVmJAPFnDask%(kD5N=shFFRC60jhnseGLIRUOgNyWoGQpW`ouj@F{nlPoMamucqvBNHvUu`IBZ%a;-x! zWgJ@hOVQuPc)N!XUHOjsAa3@ioYI0rh5|LvM=-`7F44}0jJrk*gg>G58@fxD=$n^@ zJ?RIrl8d<)ObE6D()@?f%uI2Mx#nhNBhphEhNYn_fO$}>BiOgkQSS?Fkm=)~^2S#x4^;-I!89 zCYn$k9hIj!_6y;y7*4gxB0V*ClQZa=g<57DN=(XS;85HseZy{pgbJ4G_@mO0QYEEv~ zG@GPtoh;vC?Hfc+)Y)wa`SIeI`wS^BNJ}Q9Wby`i$|IJ-|BbBa6>T7vuc2u=K;1K> z17CFLpenNOYHH_7l(HxDK$j8h>6CPHf-LqW%Li9`fOV1 zm5<3KN}?KJceUy~FSVgtnL=&(-TA=FjqI-DJ@biCknxe@(QW zDl1IH6|?9u`D+-2RM~u0jxS$1{f1mYtGzC4}X))0}qpe80WCwezeGT)NJD1pUZ?)j-nm>MJmAxr?WRPK`^ ziYG#`F3x9{g0%}PgQT~_1YTaPHD3Jy^5EKm_XqdbG+R=aS%4 zVij0KRY*x`@ZlAVq&V%43%$=g1+(hY!2b|m@oH<2U+7R!UE%*9@ojnG=EXw(?_-L} u|K-N1{4yNm|Fiqw37?_<_v%ZHlA(hA50hFiLkxY9IxRzv@I~f-5dR05Km)n} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index a02821a5afb6682c9f5bf5c1ca1279ef3332b4a5..3c14aa6c0cbeedc4b1f7c5e9e212c991d57de2d1 100644 GIT binary patch literal 4481 zcmaKwXEYq%*2a|)Cb}_75F>h&AbRg@^ax?1MQ?){Mzj%KbU~CLLvgy+)Lg zL9|2(W<+_D^DIBc0ug$;FnB;n`_;UhGXt}s|5<5eFoO}l>!zRcjK|d5sx_dj zM!!}|M4Jm~^+`{9K!U}{goNVs^IKYX!ajtpl}~a%cmkU)b8|~;wIiVQcAWEO^7Gs` zdR=BQ!zQU(HFzV>VH-Cv52+k2dfx2s3itF>g~2T8r5jNnL&h9-}<8vh=Io7BWXtd^DEIotlbWjnd9k+LeO_JHu68(*g< zTnBCA6Es(&O=MMcZx+8zD=dK?C?$V(blQczVvpM*5?zAuXpQ#wKCCR~PAf0{Ufz2D zsS0I~$((80-E(Ko_oSN~CaeSA720LZ1c5=yHL88EH_fkLvO@~Xw`kt%ku-)BG)3gP zhFL~792!Stj~ou9GAJ9ZUpH!@GetFVk&cQGH@o9yQj}FYDwKb?jlb~Hp^9t}yi1y+ zQih@|vm$qE8#rJnThCky;|_XN;0JM0Alv5Q6r!O|Z&DjR)U;z!p4X%?n`fQtRVtS- zl$!oJ-65@8p`g$CtqXWA6%jfXjX&4&o!f~ERUZ>tZ2`*%&5dmWky!he=Y;ha>vIfG~Hm?UZ-C35Fa2w}c5h|H`?_r-$d<~O}tKu@mYx27> zF%b|VTy_1ApTWN^R|cPb!K7k7yj@fE_o_{cANhpptvYbtojX;1f1+}`dR}}*_99jF z>ywqX#;IpJgwvoyw)=0aqIFtwm&m0Q-9idXrxL}Gt;j%caS|0W6k2KbJS;NL#v*Cy z`2`xX9<-{!rlk_~K3VXB5hOgP76> zH?oD%ac72dl_OBXv_Xiv@hvTggL}wa(SBBqyoGFIg@X2Xy3tQZNOls(> zP8sZ_)1`K<(h!~(gd?$O-|OCb(qJ1TCKH95Dm*9MZY)kx0`({RoG$=^<<>|m>-9!C zQ1U(bUVR2Vb<~JmHQ@aBoD!SzI=fwciH#wwT|qpSR=G47yCH)u;;%zKiZ!m;5E+T~ z=)F?DnT9nOh`i^Wb;00q{NXV|EqbPb@~(cb-aX0=KuDb(?#hs90yA&?QQ@sLa^}$# zagv%d-il49fjszAGB4|bVpTaf#_wK&8*p}M@0a`jJSg!tyC9Me8ZN8f!KN%gmIs*B zUAej?Uk#7kW)0*g%pr9Vx4FYPO6KE)?6f?{YnExtd3zLQ>r#7$Au;7KPx(%O==ibI zZLgL4y?0B(;H7TCsm2yEF+s1?Cpz0Zdco$eePDxh8m9XLj$eS@9tD{4A z`u^dq09{>Zox9MxVTRqX&l-o~T@^+!VVBtJSZ4l)_e<{}IpiE;x(g_2y?JvXf`n83 z>yqkN85*fM@IjQ)9mgGa_wP~khpO`wK1Yn48!F_*DVg0jV_7;_McsCT=?|}ag+z{@ z&BXd0dX}fSXED`8MdAF=`hBB7_7Ki+w|9aFW`cWaMguPf0tEzzAKiE8T(* z5Pq`)bTGyRD$)K_0ZjV>y+>mP@O<3@5G{#;=alukO5Rn>3o0 z*?HF+^NZztc1P8 z1*&M3o*Is|=AJ~n!i|(@w|?S7(npsR6%#gz$5f)Byh8jYv(nq_>K81pE}#(xbyQ4Vh4`FwH2~1_Hh=SOmQZ5tVC_Qh;!L*M68H zZK~=mlnnCk2_w%$U`H~Po`8bywxK=!FPZ>~Bcr2exuaj5KTZ{94KGy#UKW8erH0ZU zj2yYj(1_DG8iX|W0)>Loe~mCshv9?L?|Rf}y@OBqbA~mS8A=}kka^UX_`%?-<}vFp z%6$8>E3f+VqoTGDzqEhAUxOYt=|osCQ>6YEBse%OPm^5go7HaE?Nb>ZU5$QaGDqc8*xhgF9qS7Y z?nlbUuLDkp$GUL8UKkxKP0U@n&eUv!eZSCm%S|2|yq>zpu2(1k`qtCvIXCfRRTAxe zdYP?tQPGNi?b)S|5!al)uEogSeT0CDRGjl{;&$m1z`+l0*1iT1t5l zzq+)vB4y@q5=%-jh>!O^$R$KsChU4@AQ709ffG#9Dyce1&0S9zLaZFnnS98$D}{0G z-0vUj@(BGY9xul0@(EGr6aLg2?`cY>zi&R(nDD+WAOU-4k-wX7!Wl4hR>?6ws;D3$ z(0IH0M%LQdvdT=^9&?OuO|-kyOr;s%wy2g7oCsiKvd=(CbY=e&ICM@uP}fF)(6&Ox zAO9MaJ}-=t;_Ry8>vF{E33~y3@y7~?rLq*YBGhBzIjRxMswUWy+K%8;M^8jI3qMt#=+Q*H~0m_xcHzH$zuPoyeQY7EOtq_bs2xIDIJ$ zfCf@jH@O=<@ikb2rEUURl^^yq{_bTG*&iKlSD5LQ0SxtXh~PJG6tU^Zi1F?K^9 z>M89ik-(EBU2VI;oMNNTvG!lAknA$ zP?!hU{uEO|@D8H$`GZ(}ucp{qx~&CgwWCV9aB5huWHc2~YfPOj;$zC)yfPeL(X?uj z%Ouxl0si}qzJC=U3 zhHn8JmP9tYaiZxK7`ypZFcS0Fl6ui06!CEISE*UNNWeP3k0XG=rF}sED-O+Nlfy6z zXzLQI6ENvMP;E}(S&!8?X}n#JvNyJk38@ma!I=Jp<@IVEmABy;PM7vE5R>ll3Y~5W;1!P$(vel}IL+ zJ6Pyv0!khV&VJLfusSdLkOia~5;`esX#q*1KoUkN?Nbk#(0v6|UDSzr5w3aU6 z@%0#<%5)aDBZF@=w(xoL3>|V}#z_)b`1E3fX4hJZ-qKlj)m}-UX|hT#bS?)$R`>k$G8GUi9~w`VBJ~q5Pk&Q$DmE zr%SZ#9v$7?g^AbRFo}Gkt|3YpO|=BHnupJ2^HYQs(8X#NiRRFeO}KEWa~_y=gZm6u zGa`GES9$lN^ZKL37LP(l@3sx@_ToPsA<#(4pwTaQ^D1)U#=W=xvjT#eRVa*61+vep z6BC7u>8K96`t%ila&d)lbFuXN>EwJNB2OoN0il|n5)d8suL;`5u!q9)@a~C2`sJx7 z;d8l%PDN3xPd?LpB0)U&x=u$2ejylV? zs$*a4AA@%c`>@Sd`1{Ue3f?3HU)44HYjN3>{6?Gtq#nE%3_4k##ib7BYgUoaGwhm$p{0- zSLysC4F5}z;6kM{!a(s=(0_!ne+hnEs02pXW>3;<{||HxvKnVtP%HMr?WG+`8{!p6 zoa?eU$elVC>bT>a4RT_z-63%hBw@&`OZW7qJS?@6yEeC*FS+-bwq;f(jm*2gZB~Y* zHhr)WRg+J#PKjP%3;gV*gEimO5!*6Bb;%kMKNrK#q{*^6@r$tiQXSmm$sa zP2Lr`$MRwO4UsRk9`j-tY0+W(T-|qQmlOAeyFY7XQh>=mzHHQI%FlS%?M_=whbF}IF!4BvO`et9c6V}Fw@R1*h{?1JQK;RL!@Amn zzrQX1c3^+l@t^VcC&qv8{F_IA9NNFb@VBG;-~8HtSNQv0|9N)M@APkq89_;|{i#p< Ndo=x?8)^Pz{{yG2HKhOm literal 4215 zcmaJ^Wmptkw;e!Qh8hX!6c7ZYK^Q^028J#X7@8r6?w0P7Mp{6+q&o)@>6S)PVnFKZ zukU@o=ia-{k8}2Up0m&Xv({c)O$p->2!Mlw1E8;uRR#P5kN=#_;TBwG4)zFhdxT46 zTDb9|ENCzRW-x%2nWAE$W2GU&qQJMnEGLgs7_UYjf;{KUjUgeBOQhUeQ9-SE-)H)w zLO6%X7y`g_61t-8sP@%%Z!Z)goN`Nf2dQizMdUW|#r{Gwzq+}(lt*i}9H_zh1*+?u zq1Sq&Q9}>gzUqHp%*R_osWs|WlCf`-${vaF>C20j&>}`xT@$2HRjsQoS;*~@F6_fw zhncfAIrvC;mc0VVTW3saV_0<}ImH5y5)WK;)t-L&c$Cwy03YENBqsdRZOw+8i-J63 z*iL2Z4II~b9g8B1!;pO?08>d**HmV5Atv)ajyT;$^{Kt#7|{Z1%FRMaRU4NC%Cd}f z!k^L6$6?R~Nky!}A(#~()FK^Dt=EaKI205DjE`S25JD5^0gjq_$jcRc`7S=3aT@@!*T| z1pDO-2g&{+R=aqfkdlQ#c~eEk(-9gtG0ya5(1L{8qGYjt9@%;YLedh8&&at0lSs1# zQ_~(ZC7WwFkiB@r4K9IgDqreOwYv=Ta`|)jE>&gwH6PCO5uia#5}p&?_?ioRpbDQO z#XLlpyrVCTif(!xZ@hrC8=(q4#4_=It&8d?ec@N~-B3kGwu}!f`AJ-bX}6R778U3} zaWs89C@?rK=P>C4_Min!tlUq(GKn?Z1m3MdMob5{1zw_XO=)i$d8f?XGRl=lG^Xke zm7{sY6n$ zPYWs(^>{Gql24k#;)@(}`$dR5e4uzUd=6zg&x_yhDj~H3k}|)nZqnDoFjlCViEJ%q zB`ZA~&vYqQ4h`o(-(+?W!e(|NwIAm|>u5}v5$&VTOo{Yv zj{=?gJ|@-^%afD3?+$WCDG$ zv%3%z2c=`1;cxFdsEXe1{18NcCFW1!cCR^w{8{#D^}1UjGsWZg%WK>#z=+xx=!Rtp zlQ{0^LPWrnW6I@zH`=X&`wz<3uF)46ed4|mrw<0l^CTTXtvl7H)wbof^S#w^rr}Q? zXQe=I`PgCKW|mhqMekOFG5q*(0v+S?(>>04KErWBL$ZR?8}vVVNvqp;B#|874$M{()T;R1V!;h12EY1+edWWa!A?L)Q@%PxNycdYwnejH|) zw5d8*_WY#B1CDH*nk2_0$;)}1j)TVTyvwwecArFJ=t{ZsTsUJYlMq8|>=tc|Xx>4iPT(Il%<_@&avyE+ByR*so~;_0wl1 zjxFuP`kQJ3SRXK~g!Po(o1s-LWmTjM4NSPylQo@oyxldyTBm}r3K98{zQ4=)3{0a@ zZzc}Rq_*$xy6HJd(UxS@%39Or30$sN!G(0S?4?AuB-r5I%U!*CLG8v^rjY3IxR_)( zC^?yNC(K{BVjfl>1xujAD&^X6r#6BqC{{XMRYYt{4b>*whYR6Sr3nN~4lqa2V7Czb z&|Uy`oTL>YeBtBcvZ-w(2&$#q>G+maGuW`LWKws`TS7{KMl!u$SjSu;UBAcUU3;C9 z6}qFOTp5&Bdip%XN-dB1S+QzY2tF5=C0hc{X@gb>Bd@V*^28X_G$yyR2ouiK>325< z(4(>-QdwS}+xNKz50-%sJ2m&lA#di@-ivH2arPSvq?(@JiEdKqe68K20-eIuzINDh zSoxga@URuXHy|(dL|8l6PwTYDQOSUE&zfA);t3H1(s(0`3=D0j*FGK6Qq&|O z@(5xQ>9W@*Zf-LhKs@kHVz1SB%dkGKTH3-a=DSp>NJ0Z-Z}KhM&6z<2DF zBBGWr4$d-B-p44vv)ifFQVInGC+v$XuBC~zZB0Qm-iZ?=WIw^|#1WEW&BVaUcOHOAKfiuWo8+7q@VDcIno-hM;s`_hVd$J`ks9ljxTG618|v z3q%|7jfe=OXvWE>e%I-Xb<Kx5|&k~;MpqkMnE9+ zdZ%grhIdCox6E;kM|o0xv{S+%nmWHReYM!+s-=q1ctY`>evn!;TLW=CI{}qPbFmUV z@p1tUg^Skmw(&}PT7$N*h4;G_O|K`6{g&?ztZBDmCq-UVdq+o*`~sGj1HXS_YNiT5 zre?SsMm=|&p4H+ZNTu_oi-p?a^&q-J*!@C{BWeQV7Hz+d-BvZw475-(~Af_ zK(kh9L-;qfZ=f?bK;&}fH87^3dZpFa0Q5lLOP<&Y&uHB`PkP%?`qkFqP%KK$~| zy*;@2i~q-YW?HzQeWSj8`;mx~onIkX2#Vv0!9XZ!%h(;$JELaO!yv_leabkM$m7L3 zs9Hxlx3%F2(|jpgR0Ksq6Gd}iGWprCe)1PvOeF>bd#O@iyeyR#4bTqFmOBiajteM0 zjbzKBYFdKBL zKZNY98V+udCPRXBD1V@r`nBQSEoIO+mE*`gGQfC9y|j^njTd)V!uy;ad(blNOA%4&)u8KBb7YQ@t-t(BRj zRGe&=5&87Vt;mxty`mjWYPFEy*>%g?IyET&2_=sZMhtCJdpb+rVwcQzhwM9!?JsFh?C zLs%6vR41$^NXFhf>gZ?;jlMA*hmHtDA*~!gFo;q}1YX*M?j^z(K{xa5>> zf8D+qt3v3Ie9T8~o#w)t=O;CC$VorJnz6IhaH?v>@J-KHJn_ca;dF8M75J|{-Txqv zdiw|fh$Z>|^y#l#H*s-sFtaxKD@!if>4y$V>J(iQt>gj?-yakA3NnP9U#_fl;Oa5) zoxLPAOYj`7y8Na;>(!Jn`;!34)e{-TLhaAAKvM$%RRr{#Q}@<#A$PB=a}+E zbNN1OoZL-luhtF+33&E?&!L_iKfZP_I|HNa&UhQ0$+fRb?pv-yQzo<{N6*$I4cN z)-e}SJy-Z%cPzfEO~H`Ua)mi(+EX6?%o6g;;@HuGgpxKB9kLR`f~u~JSL|zau7n+b zQbjsNq<66|sDA5JVzl?VrenMo8)KAFA;rTjK?&xie3`4zQH!uhKc56|$Dy_1H_@R+@Az7{NY?I9N0gnpFoNWPX0T0!#= z3UxhKEM+hyj<*8s_RMt7@!%zN3hf- z^r>TNj}8E$CXC(udi~WJJ03Y&CP)wf(P&1$Vh!c$YGU`nKj93u1T?8%0oO$ERxy2Y zdr$yy;R!~UBpw+3Hl!yG4gB#$qYEG82W-yn;RbXToG5iUu-!gA5yR`OywASE_)C5! zvK6yl3;^IK#b5HHp@RVb8P@-4T>jGk-}vX~{@*YEDJg%A&3^#I{@-oRe`ok-UH|^O b3jg0iq^5-V$6Nsb7=KpdpZycz-{^k;>k_PG diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index b01f92a6cf5d215610d4bd8c7888f038044aaea5..b51b8ceb24b12a0c3d0859776756245348edb247 100644 GIT binary patch delta 64 zcmca3aYuqTz?+#xgn@&DgTaDt#zx*ltjs`q^Cea{W-vpVvylnJm^`1`98BNjwg=PF GJdOYpCJ^2L delta 64 zcmca3aYuqTz?+#xgn@&DgF#_S-$vd;tjs`q^Cea{W-vpVvylnJm^`1`98BNjwg=PF GJdOZm))V#s diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 7634af4b8af96ee4cd0d56d21212b2e682a084de..02b4f3935d62a383bc3e059eabaffa0987bd1b96 100644 GIT binary patch delta 10174 zcmZ8{Q*fpY&}?ky-Pjx3wzJvTw(V^6#I`pZ+qP}n*w{`sKHqaMvS8Q5IM+m<>#j==s*#d~ z=eN7JQ;VIc>CWdIu9~SoYaKEZ(SsRSgJ*+^mbd9vNA0|PsKkPqvx!y$8nXa~q+jEG zc$t~Xh##$MsIk~Tqp0lVU~_>awmb8lRCc%TbZ|D5#9o6J{H&E&jnkwqWF=~I4Qz|7 zi?=k0ai%vw8hd!8S`^^)ZJcVWT`KUJ6G`$ zOuWOFzd>!n`j3*;BNgqSxW$WX=EvYvR8%!%6_#LZ>TGohN9&oxnSa=1t8B7S z5(6T&2Oq5R=N_K^12YKtYG)vg9ouQnxGIr#vVl3^@5VIPE%;*}&T$+jKv`0PWkCDm z*`OOTI`}7A82+v=F1KLQUfwLW`Nfe#@TXMXe|Wm1T#tn(ggrbHbUPJAg}+mQJ(;?zfyYBE$>^WJ5Jia(&z}K6?pSV$ilF6(J-X7C z9jTDA6dO%4nsxNcNowaG<&o%IB%^z8jh*IweglFGkCC8{Gr*GWv7BPZEb zQ}G$oBStiYWljTv-cYoUdzA?OUI}}l7(H+kX$yC6zLAzq?BcB2=9&}O`BcG$ty!E_ zr>Zm?hk1_Q1-4|i0{(!4UQWN~PD3lW}IrRHlseRTf>f!=p6~ zdEH?Pup>0vYyy5^nrkX)odvnu>h>%G0;$~ZS(pr0#rUo{GmaPH|DdoE;QUNEsYarB00@U>j zQ)+Gn!nqL^ex+7;g04QXhFpv}CSi+8V`vO>K{~~$Tq3(k__-E`P#u10yj%yKdnArM z#Nt&@`)>;vUy8}KETJg@5%Xl}^8xq@g%*>4(C$EM#x{IVI^N3%O#xi`q0ct=rr@j- zJ)ZZSq_QmdRsWCY{Z|g=vEfEe<9Yh}G8GCDZaJi&J(OkpRv8>a>+Xvd-XB`31@|R7!=12ET3&Zi zu8ilnF;6~c|19MZyNXzf%C{P1g6T+d6-y&SY|uw4`vAI3Cj(yETvTMsFcVAA!W) zmU$#G(w<8(t;k?U+-jfS&UFLZ=4HGHaoh>*Xws6VUb)X& zD4KD$x=S%3?M;k6WWM{xgx@7Iu#7uZ}orbEmz$IbBpOnM|64webJFtg=J8PMLwM(?(r zv|{uinklSaIlY`MYmx0B^i`ml z66{Y%ItvW8&Dej`uyKW*sX*!~Dd0^vk#y{c&dGJOcpwr_RlZgHMF5UzAJoO`UXN`C z?RpsW>G+Kqo^5ef)TxyGLdzTj$)^&B9WQ;xlX~9P?)L?&kroo4F5ZARO;L<$q=^(s zEQ1kd-ic5C36%2=%1j`Z%TG(u@)D?EJ=zc`cU)7%sr$gUcc=^cb>Oiwf+a^UHnFug zv5(&2i`4tbBLrlJyRJ4!ML|knLHK81oQO+p@V2>dEhVp%o9^@l`k)4<4L+g^w5JDs zgSR&7x+L#tZaUR*U%RedPIWG5U9zSh(~xyjv%~>b%j2+8htOrpwnEl;4yWzRoABV3Rpc@;hGTWZX&PlN&2&2U+l-Z=-&?LxAyZaxha@74aECaU{YiA z^+-5!$<+N8i^qAwlblZL;S@u=>8?-veq=*0G@D;G#;@AVBolk+dH8tU2GsZC&g;WByd zdip8xgcT>?P3PCW0()qO0kzoTT}9>%YsauHb1!NA4109P`2HkJO^GlTF9p-(>k^sS zY%cNb$^W}j#FpKyAKFwOyR&B{WURjNwfp0R065Y05KyFbJlkykE;#t&morv}3MQW* z044s10DmKqixuOI%o?FS0qFwVhj@glSPhcs;&68!Fe!;OeaI>a14k zEQ*i^grUYqQ*8qgQlXQ|Ne%Sl74bUzxwEfi9DonR&@T!zjW2G-(mBnu+|Ako&&yWNY_woO=-AInZRJ0*L z1+1*5;<|n%+IrKb2$ zIbLDS2R;+bzf#O*bd@G!Yk|c!czq&J-Pz>CxoJFdkxc&X8%QSF{p$tuq?2)ftvKEz z%h?$|FZ%-0G5sp^yk&YwQ^@OiZ&@T~ zKM4u&QEEuhuO0|f7!cz*$cUpy6Zq3kkAdYyLO9?&cH6DFZa5~1vZ0P_-lUQUoF`1G z$Wyg}6ZK27!miVdq5C{FzR@EX9O8sKj+Kq%P(GWwNVs^+1p_O@7Cqu9^aHlU!lyGt zwq@hsy%2(*hIpQHHfo|?cgRDX-Dcbs zE@AzPC_RVY0BMOqz@+@*ok&t2?2Lhl9+3rKdJh}=?#C|{?t-=MscS#i_x0A$D{1{e zUt&bf&`wZDXLPXc61+s2IaL)K0Pr!kRf(4IorAFL|8s^Su&g9^%^;d6!GXJiu$=p?QsS682a5RsWw-lc zv&?qDm&!P3DfUKwXi;^%W$EtK-8E@bUJ_XjY#7tJEkI3)e2IupjU+&6p2k?qNcn1z zLhl&o!i#+s*|3&M)nf;!AZs!7i5SOM;`}pS>4B+rO%nj6G`t|XOdPFuXJtuLlH^!Z zt%qeu^~AHM8gqb@m?hA`I3hhgxZF@IAnHm?d$w<_J&{puml@OSgt9i=MvVvaGi?Qn zl%KJZdnti>P2X-Xvs}{*MB<^UERwQ`MBCOmj`J5B!P1D!dN~QOpRb38Zb^aS(w_)^ ztG(b`!gVOX-2n3@kXVnc;w%0b?Zo#0we#$iD>0SN$txG=QO9icI!oAjXb}=sGB-Ij zmCq7^w)CY!Zom|;V83ZA9d2pE$_od;jK(A^tYf=s2c={#|Dv8J#VF%(Gg>UvKTcw| z{m10Acn)FP<+u(kO&HLThGOS==|%G~{1O`fi(%MS&-v)=sfv%03a3YyH#% zu~@I;+wO#|E`M6fLeS%LXoJP2HOYE;3lnSIF4(1J>L)*(4JGhqFC$0b}a^ouy;UC{#-5ZVIJAXFPo? zaxxiV60jd&U}7!^;(l=_4?5<%PuHCoTk3_z-ouN!Bb2^Tj#{F-b(!9!{N`ArP5r5MqILx0OU-|Asnzs3DtA(j%FCmVuSBHR=BOj52?)@`FXhFRR9qX$LYe zdh|IE=R{oBPoVq|f1GuhO`2f`XVYQ(c*%5|92kOrneuO4Dvq)sxYLofdAi$(f8S6# z*MZPhI3~a28%N~6<4c&e>jQJ?QA^C@N;&W#J%{aFfPN7;~zw&_dS*u$DM#XIkK+r~dI34TW7R z--5sS&g@*%Sk&)~ESJz2NXuLBdO>AE{Zy!F{rCb$cnl+7wAhq>`kuTN2R>Fl?*Ui- zvzE55x|vlyK{_PnNkP#^$c=r^q7+^ztkU?~20!w9U@C4(&ZG090hG()G5^T9H89Gg zH})Ax9+l%K=O_@_b4&fnDShjat>Z!SN#u6=OFPe|L@cxEdg*I-ii-AYZqAAyGv0tC zYnv;EH>QNBz3FD~TA_3ZC?;GsP-F$5V=LB^9HvO0}6ibt8s zR5={fq)~dy&TVz!ZLlhSQ3TJvMs?Mt_d!OxxYPAbO7x977WtYMfKl|{2114L zWA5za841;U0@eGm+q8c+-Mx?1K1RJA&iqU9HHe-X-K&T7gNOCWt)8H?UmyiIWnKNN z8XiJ^{a({-qB|#nAXIrP3u+*BYK`fh>eX2H<>)cCvzx)jEP({k| z=EzKh&A8VLa=xC!bCQq);M|CL$N#wdKIpg`E$9yOBg5@D$l;-0YLe-N()H*)IdL*R z=Zt#Ps{22TMR10pkxom(b*9I>Zy;#m?x1HoIBxw-D#S(Y15>s^0GL|>%Qw=$C*<8n z+mZ;Kp)J~QE!w!5CsMY!Whd2dJpY(SJ}PxX-y2kk|Eq4cbz=p7bjMH{L0-{}QNOrT z6&&!re|Qm+UKZ|?cer6ASaC(T#dVB&pK?PBJ(7m_N$Enm$}3q*yzyrdBb~kfI@CfX z&R>AK@DZGAj^KV|k$DmT)99utFf(zJ>PnwujwqSwtAIpvcQYbV8&gKaDtjZ@TuIC zw)wT3Bpojr=;sPu2S1Lgs;x&nU7pQFNhm*tx*^6DXiG@}Du&xM^rmw?Yp#D~TPLch z|Ku2}(qOIN-;c&yFe=>NT3WrlE6$%B?l(U#5ADCc!5xBnHd+F1`FgEJGO_&-Fh-P< zeSNW)miZ;u|^p{G;2&@Oi$tgKD(`&O&u zHFz+U#w}&FTk-BaKDNffhR&95yCyYX`AMm(d*4n})0RkJw1mK?pMPfQ10NRq>~g7@ z83VA*pe+?6=nvrqSAQz5qvasAPCO|13~el;_1P;#&Vl$oKs_B7KmNR!duKKtTO|I; zqWT1h@zuKT!*BK_E_^Ni$xLCEGbnze(k;sT#V#=+mH8h=r@;Z7IL$)G%K|UQMXkNW zkK^6%EC)}XR%>ZMz<4+NLDbcK`F zp3hHU_EttW++kLffUT6!gp^gXJe?C_;zq9Ul_7s!K%%_x-Y;Y4sTg#)b1TtB{bg^c zX4T)f_4Pd3Ly}Tbd#+^hq&a^O2L)398>eHE?LP7j=Dl?o{X*I-r1IoE;6+ykyeTpB zz1EFPcl1sIf#iOX6YZt*^^^-487&Z>Go81bo$8%8>zCeYgk~7_bVthZS5WH!V^bsY zB@4n)xL@Hr70kZ|4yG9*?+7%j!P@4lckFG}wSEA_;I5xAk`wYvqyUKCk|t2V zM52&26c~;)T~O}tW;ZB<)&2p=%SZu1m`uH$Y*O$AtFh$+4u<+p0>p@ZQ#77V74183 z`BA_YRQy8+p$ONDj^WT!Pgf5_g(vcnNW{s*eHcI^At%k(fqMw+p_KJcKVY9U-Y^R1&;uzc0f& z&xzeQ?(V$sm^&_|;WZNZ+Bh#kdv>TjH9j8GyzH87$VVvbtkX zR&zXe-*%eLBTa18NJ@fFFy|;nRUadraM>?;>)U&vX@NSUtCW7Q?+VX%Cdy|qmu=$A zdkP|0rh01HCt}I583teY89B)0LaxOCr&#Fk6iv;@z+=Lt+O{68s)ko6SPT?+j90I3 zQZTH^E@Y(vv!ZK#CFD21K9ZxirJz>l**6YI;S|ZFnV-gYTG~R8Q#4dlmW1mXFI@4- zVkF7awANBjvIgCk%SYwy-kcd6lTSwHbwVvlcMq{>KN9`=g*^@=DC%s5-QrF9}G-i3k>Z4arKg5 z@n`@78Qkktq8?+13vQ>*Tgtk9Qqwih^;irl?n-ISh@=<{2JP8wVZ{X%wuK76pY7fk zw?y%19^{PD1g(zZBu;;0xgFOg7~@j@5p$Cq_QRKZnR^v?oa>n(k`?hUEa=5uzn#7L z?G(JWd^OTKnGyyoRlpF=Tn^SQ%NjD3NiYK_9SM*&gg8U?nZ01XpN!GEyKOlE?XW^b zn>SFy@(1o1Tu6R5IYR6`UoQ$P*z^@EJg;4ke_~-1&2e7do@)6vz&UoT+Oorj#ez7D znF2{rAaRyZ0(P9fYvSwI?vIK*Z+yJj`Sb|5_XxD^OfxQaRIdmF2B8cqZ67jU$7ukG zrJD$1Hw0m0GO-{^5L9abYEU5nUBhLmnd%0E{QAfwr4lG$KMe?X?#l7`b(jXg^kg(n`&h~iU0Kwwh`8nmWc1q^ z%W;#`6~9&dtfc9j9^~a~o*&G>t>maPA7MmU{-e2}Om~&{i!tu#g<#O`LCoxk7?gxux<|-}1)V@HvLZT7E)=5FI#WL}!ie&z^CcGS z+zKF`S+k$1UWn3)k$}sv9{r&yjz-DsRS-<~5ByeX{8RXW6}@LPPe)xO)~7A3#P8V$ z*tq=gzJo;wuA-gL7KTp9s$->d8gsJf%6}8NU?hHb*W~{EeI(c8P042uUsuq$P=EX! zl6^eOdOn4979-At%i*Hts_&(3#PT7?%Iv^lxPVOZiu}rBZVKSjA3nnR>T7)C)?4nz zHOt}7E#IzdE%q%L<*47AIBJSTHsEl08XpH}yL`*}btwo@+{Dl@Ly^&w*ye|o2AWsQ z;z1%Uh_belrTo)b5rzw52B zR-JHTEc3NxC;;S-SX1N=A`iYSW-_}NSX!OtMMAd{`}zYSPkU$jx-a{2I$zqn*Jhvg z>r9JSJ!phqu59-4y;w#B?~k&Z@6cSp(A19Oy$5AJJ;X!PI|_QRdBdUHbj}iM5HaZZ z`C|4(B0Iq!%2q~8b3Y@_sH(fbtSTKv4t%Pc&KMeD5#T~Xtd*3{3-|-u;e-C0^L!X& z;SO%shk~KaFJdY@`_)SmRh!@8n`-$cAKdt1Xf6$rc`Rif*Dggt;im#28Bw6V*_kIY zOm*fRVj5uf7tx>qMFhq#@yMwgGX%xfwZN&|YU38)jJ4KIZ4RmO4vg+Ud!O+>vGw>} zRhA}o3DDFJ-A=p8m^6&k%a#lsL)LzOi=>qsuA{>TBJ(oI@kcxPFC&uzVR%7q`}_-s z<4k6;LqYE+EkoFn6p^2JUmrM?6|A}PqrAY%GFL1ZPI&SK&_PeGK(*Padgo1&K@ zgNQ06^U%rVA2^S4nlX+BZllH9ZzA-?$jK`TRK_0VlBQ!njnznI6p$~mU_Gk?kD(#^ zfW|JLAUJgKND@!~OERkO^n?LMPfWRuu|7bfwh*$onFO(2BN7_Vr3nWjndYrn1!JV}ES&EyH#1|H(@#)jC7ZRu zB4~-DoCJYtj0=P@u%bo7x&QmOiz=cHfV4%g9Ow)4tF>>J6lG?i>x>T~1l^}>$RMl? zwmERJ^|4Ohb}YUENQFcDhK$Oz`zUw%nC;r?MIrcfo_EZP+$gSCi9f&nUAE-Ev)4VZ zL)p?e&f_M|SabgSmhwiCH43Vm{(eW6vUw>;*if}>9J=W@eSw>s*7&MzU9{X7KpyR$ zI9g4Z{^=rrvWJ1tNM+(Pq}s1fYA{8cR0uVImB|@ii*%^sDY4(0A{C#nl^}>|12H^d z2zQ5pJwuI$0;4o!Lk+S{R}YCQ&OS8{{2}aLB}$xAZQ~_Ti**il_6w(oX;9<}pMGd@ z;@XLglk2d8zX{$)jeXQ+F&NPj7!tWcGP*MPg?8oP)oBHl)8 zU(-nN&tJx5i=;@N;^OO<2=Dju5F=nWt9VUChYqc7|itJ$8ojuP0S z?_!Q(gd<}%+EZkEazLz2w$VsE0f&nWwu^(SS_?+DB<-reHdm zJck2`O)TJ^5L6bF98WU$Ng0&`(<{C+j3;P=ueEu28AYA5x}k0&T;5lGo~jt5kzAJw zv1-mSiEVhey&fyMM4p~_z)NgfY(YtaILsgvS%oEy1yos5Cd;dDHG`y= zT-yiZKBXX{C=@mv+iNO;UN(6+bHdg9x{5v_N@al*7shw8CwMOLW_BWPLU3$Y!t`pC znG@F}Gf|$DI0>uHLFgUOKb8d;r$4IY(y=#5$pOuX9={wDeibk2euk>(ljqnmT)svR zsbNLo-XyjT!%A9bA;C__;Qyg5;xZj@*ClU&3MBcdNPPG`4i_^Oka`VQ$2BFRXc_V< z0+Twrvg$YhIVy^PF;V`OlZRK6DV!?KGiM2)u13*W0}-amMFc_xF_oZIBYRs`|467J zys{2-algJkg)j0{?D(nKkf_0(N$Vx*h-Zb{@++F0>x1NUq~03g5i$JWKBZ+bGJFwi zW2FdM?+$EcXbwCZuzqq%i}E>=0mp9WZLErTEFlW;fYQO z%V=Da7j0oe5dM$uH*fu79)oSuor|Fb^E3%GmgDr?Y+qa&!0wL-Z69`(E!w$6L=%deg>rXyV7aA}QJDlckXS^hV@MEy0G#4ZNS9o=H1$be_R?O0VY zm|%9xy1^e0q%(-2#jcr%``tI}%*EEmr)2iO*-kf*1%z&!Fb8`k#1wthR5z&$@V7;lPp z9Is<${abaRJ)7RXI)0w*_!WyBL&ArARF+XEht@Xjbj7M!=yU=T?;aRCDf{2Q=h6;5P0sp6~?c|hyr!;_u zBH@0-9i}4FLF|X7oGcdMTb<;TgG8}0J)zZUU`nHVK0U&z4XMw70vVx(GD}u%k)l4d z@LWRGgxIftei^481jQ*@jvRv0;%S%e$PKcBXI1*nFmm!c2l;OQh(d$EDqU(9&(8?+ z^*DM##_%n@EH1>#ZiD0U1NiF^43O!=E6BMpYnQp6AHn0j*-uDs+bHOL1L*EK*2oh*_Rh=*M#8R1f>XBFBj$#IEzOWObLpAR);I(i@; zMDBw%jxHm}bPqPID6jBjFj%|6<5*vh#fGjJq_H(akGT;V=!v;?u8SKM)vb=JI92RX zday^@IIl4$u^adEI?BxNF!Ik3`bp6O?uR^8YR^a^d!56x5>=3_%@KefV?c`_@m7;P zWwqeON=eIQ_+1%gNj<|Z$j*{#W?xLlT<70@B8T2Fbme2v;;Y!{UmDo$dj=U1m+H;~ z@h7Khk}J%lWNa|gX5_EeVl^dsCKIAG^LC(+MSB{_LVr2BI$BPij$-Df)xN2ma>m1_ExZkymjRNtAnxbi zH1!J2#bQmxq@wwbY6p<2;~JWW)7J?J6^zhbaXZPtwp_j37N)c0z9@Fe9}aYl0|Iw> z&d2rvn*VefunR55eq3!{SX>}_54}aR%%LeaGFmBrz4fNxasC8!St4Bn6&ZuLEo+YB zb7tWlNC^@i8Q;k_gbW@>T%}l4Z5N5;k4EPEXD;-S{1#=XU5%(CHOS#`H;FizXc`Wh zlBC4XXimEhKbg#k$^&nEKV>PkT$OIHTGBVoHt%7mc_9pDxr*Z* zsKa8S(p?LGHWC5r*vev_W+_UZ)tKA~VNM#VNh*X=D!Ho1`-aw_;6W zGR0;8mvso!y8f6u6~cjedXscc#y~yR)R_KGs*G3}ixR-mvXOX;XUWT?xdNVI^>(F2 zS{>(mv0U)CG6Gn5Qm2iediI`KC~xaaAHm~u`cv#A*73OlTcP|tRP3u?^5=4h7&TJpf}7PD@V>3Kc#Q@?0$nbzEcPB9jBcKjcTC(Nx*wsSVV9#+6kr3OL8RD!t? zVa8xCn$bdssVK&tTyFC_KQENRU)-t3^Ap%3q1BFeX<1vQpoF7kU9t9P`O4rP%Ti@i zL!83BWakqLALHgC3(0=y{2Mud%kCs?DUWAl2^*-~-9mbnOT;5B$~_bunbre)s3D%> zQ%SU=kKlmOYR~zm6VDpGnbP9#1naWQE9mB95__IcPYXC7D#Ruv%vjaNrKhu69S>yV zdEA4Ja-r7qV6oKBv33;$vnsuE7=-awi_VO(q_h*+u@LP`oQ}xJh}D9T?3q)4(V0Qk zRRU1CD1nsA&cFU5Yfn;FtaDVi1tsTPVPSi8(Q7jRY9WXlR73iB*=}dOqsUyRv8DKb z?1ANp=J)^#asRdu5H&{TP8F>sx7wxE7yR;_5Zkp&;J~mu_Xu;5V0OANS zLK&hLMrN>*Jxc5cR!OANV@aLlz`>0@&yKoF-;FJFN)Rq%1a3#{Qwc&`L0w8}8m8l= zHBBTjY2V~SVtOa>U4*sg*jzQh095z>A)#A{s<$ztCqrb_rbwliU1_r=EYrVpW5~80yI@%&Gg%%ZR zD~N(I87OP)MsNl2!yo4uz$SMm(#Se~9YImgf zi49ZYcIfbjCqxinJ&zOV1M=sIMuc;L;FK&y+aQl-39FTsY=fVtJ`7((q5mx9nk7Ra zn$r#FebTi<4jWmt>!%i319Z?++3+cIW6m(oi8RnfpqoHUN%N`HL}5Z{ZWb2&T!&&I z-XMlY@cat%N_ZW9E~_y@+pqeGOkDJ@gm=&fBicPt1qD6EC})CB4`(!%oli%FPv=&F zTYNlx;aW0H&86G)!T2PZdVc(qL;n&&j8aN7c#s21=~!zF3R=h=0dclS7-%^z*A|rQ zumF{yXWWt?ojkfnZErU{CIXFK!wqfJzuvfctz%aAqEDwXf`2LVnq_t-E4tIoADuqd z1Z&$#-k!v)P+oh=`~!7)cP@7xL!s4$ z2&{wTe@XD{B=vf2{K>DWSU!boU&>O8Sa-Y);H>kBQdPEeq0x3pS`p-g-h~Xuxp#f= zfVo1$_`*Lfz$aj&zzeVBJuzT7T6cbzg|O8X2=R;BUfEt6cwh~_bymIkkKzC}RFu&( zB-`e?SBkX(=KK(*hJlT6cTxz*l!>(GRZ#N&0xH9JO*i=0W?Tp`_`Ub*a2v;Bs!59=vhMRZsu59Nu8ZbS7oS-BqAgZnbg2k7O`q7tbc z`zcKNC`^iWRIJgW1O=mAqxXJyoTPYybqY#Gx&WkX%GzqPpzYHhcmCDodGG4sP?EIs zk^B@7Ft3{MW{47qiTBJPO%DJyDUDBMvb38%OmzL!cw8r%11lswcYb64=)%FqgLCUs z?CpVTWI#=od4N9i1xE0e(Z7z0Qqu5hHkE6my%F);a2_2F7m&$j=0FT+-~V#PAx03D z1`tH45OjDDdmD>};^q+#r+)GQ+eDviwf8!fZzse=qG$BQrlbpRA4mhrD`j5BR}Oc< zvOUOB51_!_0OU2DOx}z&ay42~C-)E&#;|jHa^ag-=M%clcQlr}uRUIVocItYWd$?( zjwDzuLan}nbQy2LD#v7o;qO!eXE{A)K%C22o4AqlcAi6~a9G>(_n60QiH+CPZ>FD2 zA8TaBEa1&);SZIu&L(f8z#P88+hu`KQ8~|8_fPk%JrnTDQ)V^B`&8Lc4aH()$|2}e zX45O!Z&$P=oi6Bj>_8hK2f2L0gWBFh4b*I1zE~_4z=<%DZa(LlBByh}TnKZcZFP>){!W-y>)mI(#EW{8p}O`Qx9QN+98= zJQr0fN#hJ8vktfC@3H;fiRBoF*^oUIO`}u?iFI3v+nx|@Zm-7iP;8D|QX~t4hP~&% zxioAg*bRH3C9~26>JATMwqqT!0F@Kp6@L3cBaA`nWUDu9v*^G#!t^D#wd+wPHT+@d zaqM(Xwp7`C#XP}_68?$~EZq7r?riL7FBO`<#cr<|BMCJey%DtS)@RJ>HdbLD%csXD&g4K;)&vfWCzb!4WK)9%ZY+& zj?Gj@VrmehR7$P%5_wxad^xhK1lKie4eaVF|Ct)t?A)^O`5UYsuWI`nGv`2Qs9kF6 ziY%B7(L8gdE+0c$+mP3DM(E{?pD|l{G>xBS5?LQoavFy(d!unmC;k~%LSx?@QKGP3 zHL`vmaSR`Kv_Y*m8c{0k2OJ?D>w2P*rf!_6zl$t_)7F%-9QXR7Tx0QLU-5r+1b5M+ zQ{o#Cd7}qx+U5({)0k|4g816dr~LOQE|X<8;u|z*ZNbr-AY2Qrk>ngUA}*L$QrUi`uivg%z!*br4Qse(Iaf1~j@xm}E!r73Iad zU@$xd-Pxo`48!(oOkK6L6W#~}FZB?0U9FTF`&=65W@Ci}3n)Kj|Qc{N#?n6v$ zf76w=#ooF5xsR{~j;FS3Ve_lPetXjnkMljy^avI0jbEL2L(jPnJ**Id?B&o zqysK&w}U0=<*6EfVP4miOo@k@HMKbRbkw+^UpqO#ms(XdUb^I)3W#zZthcLF7@1;1 zoyNlA0o;uDJnARs8%RFzE7MtlmfRp`#`DVIwi$H;Bg#fW&u8wEuBEn=D*+{qi(oD* z?o|=^w?1c5AocPgX=5ooX~Xvoe4#f268hJbz!kN*A@$8a^6>>{lep*!57@t=@51FA zZk|CA_GF!3zB@1pXlGM33i~YRc3d*+9jhl=JPSJym|uN0vM(2q8`{6xRS+!>{`N0uz>%*d>W`rQ%^^E#b!FWhX20VJ;h{nGc!NN)?*F9reb?;d<@ z0r0Xp__0-+_bq-?yEpzjI~s36s@LIWk)mbT)qv79k>KY*F?K3&^13tC*Y$K8$oA3q zIB4=>yKnMuE9#%$o{4XssKl!6+XHB&0c#A{Ty*{lgtJ#6bIGgJF^fh%A6>d$k@aA< zrG#u?EA$d+W{c!5ANJjly`Oyve%{ZaPZQP7BK%n9j_-!y?C;JCdW%8XyEL}`wP5?4 zQ>FJ-&co@qHihy@qWys#-^PMu9X9F75^nxJJdT!gSJz*>1#%H*&Alcafi)HBuw%SQM81u8z^3E~z_VV&M*8EjY z&83<{rdbMciG7*-UB``-m~3%TAO!%@g|0elP9HdNL)>)D04QZl5xxZLp29wzrQWWv z6wb4b6n4J1#a6H?(g58?6nF{y0X5s2w=LnPiv$u~yL!RNAYJwYcRPQ@GE3u3h|BL4 z*e+DvYYnl7A2wvK*PCK9v$PFvTW2mce=k0IH(^*p_Y>qBe=QO5^6P+}OG|)*IfzAh z|6#PKNP0*$LC{g=n8P5VL*0Quic!pVF;zC_G^ftw)*pAl&4+)Sk}2YxbBE3kUzo4! zzquaTw9jPbNPa(c7sj_y8I;F)@*cozufh1&LRL^%lETZ)iYpKHs=y}Fc%f=rhWL%XfKQx{f@@o1yAYO*Jn}!EKl(L0QIFth&;=Lqg}c~^ZsvAbsg1*>6I|8Z4W@hQ&m&gHO=e|M zm@mf|eHFDn%zv(tA*yo~g?7`G<~v^|YVC(|7$R9ZPt{8sl8nZrxkdc}=>;;bwBrD* z;*}LxNF$w1;eGrdn#Sv>TFqko?^xX-V&3U(IA09mh;)G+C6`;D!3nD$E9zd0s>3ga z(qq1cub}Vw=8J6L8)7)=7)ReV2Jj6cG0(A#L}#1nIQllR5gGz7*VSx>zd9xYX)4$3 zYR+XTmjoT=>1rTw{P zA_wj1z$uKsG3s+vdnk^-EgSPpq1g_?R?jPdjSEsasMV$+SBqOsijM z^Gx>`y{WiR*(A%@=*r&f3lwl`6|ax zl^uAhORantfGp9CprshLu1EL{BJ)yr3?FEzB6Y*yHyDteV&EC)J%BoZG zoYKFztii9IA3i`j@&4vd7tJjm=|6Cz-@2)C=)AVLJSsFFd}$ufp$#M4ej$)gT=T6r8--iT zrb*|mcg}waIr#FuY5-k*dD!k9Lg7tZKT<@>itsE*i{%4TXD3dbg^K!m*ifGg{onLAjxYe6ep*a!(~# z=*4#?YjXE9g_pwQ=4O@+TQK}WC;mdm;dr*v@}rS`z52CkT`p{_dwV~B^X_KG<@x!j z+2Qsp^TCy`5Y%QNMxcN9q2xEiOmjWWt<6*c05*X4;aQx%hoAbt?c9*btaR`)KF3M? zFYd3O2K|1c^HLZG^bdsW}x6mRtMMAILu5Gx<;B2o;vy zZXa;sd73=T>{Kk_Y%PON)xE~~ZwUw!gDwd3E}fnj>-oE}iI5bi(T>$-kPn-oNx+$` z>(Qm%5t)4$Ez=#`9{ZU!^~dm4kLY&ZCqYvT|M-0l!_6D)>L-!oC+PWb)79n`-Ms<` zcD=6|w|<02;ToHDXbQaV$?Kj%Yw)vfNNNRC&j=btq3A8 z?Pjg0ke*UsT<|vH!}J>DE6v>N7CD~W*e{W>GEOy(BxhB6%{ln7+ZSnIv)!1lm zvN9@8e2ZD&P;lySGw=NRBQTR^b|1SO_p>!7v9DFZqSsoZ#q?~CfL2@ml)p~mcRiv` zw=SQ>bNr696;r7dsIF&LZ^_jRuP}1K_oL`*o`-#4dP(MihK7pgBU-Q<9M7r^!Cy;V z^&|7-*>LP{Df2A!bX5Q96R!Df!$D=|)0kCVmWMknw-{IH?51m(^8iV&L|c5hJEZcO z>_vGvt1iQ;aP=u&*OQa%uZ>B4pLYA>P&{>cLWrN}hRW(5yN$H_ep4sE#oc}ib9PTw zoejc*TaEM2kh_|yP{h6S1{=A7e5alpZtTOXpIf{UMVj6;N+JB9%04X_Crra> z$m%IS=_@1Q&@<1Pnz{X$cKPZbw|)8Pq?I?lg5KwWx>7Y4V_HepA7F@Vh6CJ5fEL@> zqciElL|)!7QAoA~a)QE;MU~jRP^bjm+iJ0&L|-?U$pk3eTICvZO&VaeP3XNZwsyGDK zdq0PYr(=houC!>L7T5xwH#gCquEi`0D|E==~VPoq$;8>E~HaD)6pz zl_7sR|GKET=Lh#{H1N3G&)^qbi3l24ybBxyr}w!JEgpYSuyCL)$i z^uNm-&p-5o%R_tl%W+#R`f0UKXQHf+{kqrz3Oo?0*(LYeOpg+j^ULaSdT8GSOt*nz zG@BV$C?K+Obi{5LSR7h(@@;oLoIF3caNe!ztY5cx?q9dgUkGe(UtP`pQN5{p(Z}l~ zTV0W(pZ0Maf;^XKSc0aitwE~kvvBue^57Wi9tFHf3Qpq)}`+EYE4U=JKbHfW32 zh?G)4?AQ4TDVm3b_L6%1r5rP4G?Jc-b{xPG}80UWDGvpt$9VfwbGAsEgwPdx# zY>Hp5D57lu($l8wyCJ7-mh5UY1+6GQUPwiR`ojNH8;0!RdYeH+D5}ybEWirAF4<_$ z%V;SGQ@odMrl0bmI1XgMGzgD|CCc0OowfBlT5ZFeWHYaj`&_}{z|qlDC8Y*aL~vfW z@pQ;VOQueeNnVdMv2=$m|GBYlyfN)TMKMb_i*rI_wIhaWH3%9JCgvy*uLzqC_OgO7Xdu{o{8<7sx7=P%LiX;AT8`l#;4NkM!t z`AiiGg!wlR?zAB+_Q|8DD@^~EV2mc=@~4C~-7;;`ScEQbI3 z9nV!OSFMD5_vwox_Cc?S=x})VcK_z}Hrdk^EcOX*!mWKkD1v#>@(tyo=mLi%X>!Tk z9Xq2mMN}Z1qe835Zc5yCWkBwJWm?CLoq9XcH#ok_RbEA$6YwMUN zIwVJobW3LiM~_gyFZ%JKID*eYcMaz}YL>ph9jmx1rwqq%mFtW*FMD&Bo(q2MOE~d4Wja9`MUsa-%zm-K= zw;+yCUwE?!2kIupk~AM5155Jz+r1)T!H-GZ2IC_8&|$8^2C3zZ@s|4^*CT8|w{7;x zmR(+OdT5Bvx32~KWe8E}$wuoqe~9N_)$dwKiK6vde42!2IopU(oVyfm(F;Kf3XE28 z8krl}5kdv&35MKJ*fP*2cmw7uV&3PL>UMM|QYjP3l(3Au^O+8=!8VLu#_W=c2IET+ z7~%y^f$(6~Z}ug#rI<2d?|kpT4W-q5M}K>9jvx!WW!4Y|99b3i&54qoef9FK<6Qn> zBYxr~{e$ehk31!#L(&mBhnTHr?7Yw~(>Rn$GCG(5&Z|JD{*uh0FEjeJLq~XDIW=`k zBk2vbjdkb?jV%_sqEnS7)r1|t{HT|ce;`cW7LW|%b5V&ab3tyvx@yD&0Fp%*FdRqH zVz^H$jpW}CJ4!K4ccG4uCC|cR;S2Zs)}s*zm?{fi%!pjDU4ExbiVFGlU;G~%ny0K^ zh+4mtnM%L6mo_OZK#`t&kE!-hu*g=23YuABNS(KijOLlAVX&zmb>pE)W!IOdEa&<0 zZgbW%*okVZEb|mys?a6@Q2bfYm6H!+0h3^ulZ>TaMNYbM#*s^xQ$kZL!eplQ;_OMY zW`A`jMk$Kq<)!DsuSD?V6ke!=`5g$c8X_XFJbhPZnl%4~YlYoM{a4Z&C%B_TXLDEE z(Rt)i+Me?%(l&9a1R1|3((W9^?1m9bMh+_CxNtl|evf%%Jme|^*n1cnL$5~cKP$Br zn>mT#AH*6vXeZge5Ho9UXGKfrDC;Wjqw4e_&UcNP;_mIlLXNnZUOl-vHP>lYU}Mg^ z4MtGX<)6=d&w!%bfB8-00~KseK8Yr{F0&OUCMZ3Sn4wH?ZU3T%&*xvi9P$X`Npto6 z3}sMcxWOHVSiq(okc&*FJ{TK`bZgKS^SsD5T-ixi+JtWY@#5%PW0I5xGXj5tj@q;` ze)Zs#b?v=omnRsQ13K=Yt|IFdON{}?wGQcr|uuu`Ev9P7Ip^a{x zslTEHMBSV9dk@njPu!OEsznAbuBi%8bWy2a1RDrI7dZ~jEjoc4=HCS`p8~cji+df^TpBm9LF-J8o z9|R3J5(a-;Bc-~{0A8HVQIMBM7&>eZn3=GxbVue&3L{42>;+(qxOJuUw$8*UdadAC znN^w@6M}yq6DO6ZsJ;qUivw2aLk>KeDIJ00>RyMjt>&uUz80fJBWLs^D<2=c|3hso zSms0?WC(~?{r^z=|B`mS0o`|KwEtePRQ^AWC#^9ulmD;uf2VLD{;$0dCebrdLjTv4 Vq|5|@a-&JIXCj3=p#NXb{{zBH&oKZ1 diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 4906adfcd6c77dcf19ea48d19aecdf5b0bba076f..1feb9930013a7863010f0a8c5f658366cf0965c5 100644 GIT binary patch delta 2359 zcmV-73CQ-jGPyDhP)h>@6aWYa2mm+^n2`-M0T{7DCIl)yPm)M>Mzgd@P1o$X)X`%j z6Uz8dJZov#SRa9K=cdghp#M{KA#q`I%{XLRj+DUA{~-aJy;o_ z6;yS0#91h?GeIf(b(_ z#(!3KIbM0x)S&6oW|$S9!ExWpS4e5%S+kJ|C3+Mrlr*8lvl5|Kf`F87ykjBbjd9}z zu;@6)5=c58lGNQu(1g1{SBcW<_qp(D+eh^>OBN7>x&`5f2TOT9^(wzzyL433{WDmVd+NQYIBFUNRs;{Vw)tOoah)H9IzJi|XrmL$ z-#->$g3UsQVs410>0?MbogdT<3nWY7d~!2E1dk=q#yt*TWayPkJARWbW@A{UUHM@Q%I&W z@5rkQstL?3Pet}m1NIvl9Z_+xZftLyHzM1H!`N}srz4nW2pQ*)rD2CBYQAQfRo;HU z&sKi2~ryCtPynn^G6`~>q$(G;T z(B~q<=K(`P^DVpez_{fPCM!Ayc|OT@=Lb~_nw3!6c52WIV4;Z<$4Q$XV$c^Nsu!V} zYwFa5w|#EHq%Y=q2EV-|k`zGe+xP+mS_c-q9n|lbQF%G`ip)!q(aYvJ)&<IE>iEfxZ%f-s)N4 zPQ>{tNs66z)&sT49>@NG<6h43)yVOX@21>+UQ_2!IQClZl{n*d__pj}cs)Md9-$>2 zMc#xkr(JT_h~5ROlEJXxm4?taAjda?l{YQ87j+Xy{eWyiD1X_F6U>{C>zje==9b*V zjm?!O4T#(DP25hXZUs)!-oU;?)va((L*K<)6a4mW)ZnflnZJjm zL~*xUzvK2atAEh<@+$K_tTJ~a$@_V}=bre1Xb^r7-+Tx=o_)=|+tKk0V*XM;6L1B+hh;(NAzKKIv=mDeiR0=hF>Z7nF35n~`zl z2>lFF-R-};7hWa{Zld}u?_`kI=aB02yd}uDuq6ntrhojV;0pu{{zXuV&@Z7a_r0gUZkyX#u_-xWqT2F7Zw9_AIxPrdIgYpMDD|?un+VZ=(v| z;VLxMO4X|XPsa>>0WH4EwQwPS4}c}qlbTU>A$%Vp{D4EaahVXjwQBxOmgD?k80U|C z-}*5Q|9^!0mfAw!I$qIcpth*`l{K|u^R2A!WIshG`x!WyM1M{aBK<|s!$|a(JfePu z_YPSYZD1 zI&pV5^*gle@4a~Y1D>Y*Q4#=tQ#Z#ArA3omnt%QYZS&`OP1YVB%zp_7vq=AnkM{`~ z*uDvo_{B6!?{nhlZx}~^=f=Ky`L=<8a`)3qji!HaTe{l*(~qWq;qbqCG#zhYG>u@U zbC!_{{0~OZe<4!h^nNHA1nLQ)|MO5NF+iaRE#E?VhgKd8MFbd%gn_IOSRW-0B2&#N z9)EDfMd9~Ruu2Uxt&%{slCJ+MDgRW-^&}RsTWEX8z{X0QrhO138fv9kkS!K zLP{qlA!P+mLddQQI4j*;yC!4B*ABuFoyQ49rH88$K=0-8!lAE>M2E5pDOWEL9m?u? z4TiD?v91NID^^GT%|Wi#?7qu)OmO+@kbh`BZWublJAqxhIfM<7tpM0>W6;bfr{VYe z11QQST>8x*a4WrRIeE}^a%wJV8oJLYE7?m7XytUY^A^v!wt{mh+aNh^-Mb_-5x+bG zjeX|4WOzQe^;yy7?yIvd8hASz_-t-qYst1bhKGntHO@KQIIcQ7P@Qv8ozBR<)PK=O zj_Q*O_K2AVXB-QCl%0O;?Lu+=AZ{BSUhcn49mee#9bV!@jA6G4bHjKyV%vjZ6xmSo zExK}EB#OA{_TtdJ;i2$_oN~U9#QPrQg7Af$vJXbx+Y)6UdPkDsr%Utij@6aWYa2moihj*$&C0S2)`CIl+oD@i0fqgmRdrfc?G>gchN z31xgJp0zY=tdBsrbJJ!L(Eq8rkmYfH9+Q#;)qnOP@nsTeowYOBs#movkq$|z9;^(| z3aYwa&Lm#)xTBK}pBxv64u@Rb)#ZScZU-J$0CO(q0kHO*uuZjMl|ZD2ER0E_2c?uG znuLyksDvkp9)i&X%q%cMFNZgDlqa@39>j@l9MSr=T9Gvwq!=E>^e}30M9QQ9!Gxg| zV}Gl=9IrfTYS46PGt7$5;J9z)E2K2>tl7wf5@XWTD6JdEkCa z_6JhLITo}FfItmPF^_|6T-!42!rBGNOd?(v%6uhue!8UUv>!r zH%k{atE$?C=>|2JP7xwz=(Lbt%UOH7-%zJ7^5RJ~Nfa~CIM%QdgEH3wz7@`HVt<|U zhwB3210A&451Ut#Ftw>^n_fr2{JKP9?VB5H`GRkK+kI8bLRzF1kSJ0E2|&b9&wEbBAo%P)(tFPE51M>oenfXEJJRYvZwp%`+%#j zK}F~+;yDR;*3cu%$`LYbX#A+M`Z)7BjK+h}h=+zsElh_T;0Eyj1iev6OMl`Fp*NAF zNFND!)?c`I`#3Zq1I;!=UBBjFKx4LVe8;JH95sysD}skw+x)M)xXzD4ogWPfw9$#> z?;i^=!DgXDF*iih^f4rz&JXH_1(Kz3KDn77g2xhQ;~obvGW5!&9lyyIvoR}&JjZEz zxtfnhAy0rpAZa$CPxMofn}2oblhCi84Dx#-Td{s@`{^w>dB02A8*GaeFS$wdDJ0XG zcjVOt)dc32ry~2O0s9S&j;J_TH?}v<8`QWXo@E z=yQ?b^ME0t`Ig;!VBGQtlNB9jLgrFAqDG zMDIY_R{-rsdXp^Y7JvFI&XzgLEC6W^NOM4%1JYcGG>3ZU>dyNb97gQoKwpVKZ}lv2 zC*pjSB*jiU>w(&2k7IwpaWCiiYUFsxcT?^@uc`AV9D6PIN}TaJd|UP~ydIx!kI<5i zB5y*N(=NGdMDK!C$zWLUN<-)ykmDP{%9|G4i@J%Uen7S$lz;5T3Fb}6_07O_b4zaG z#^%bC2E=XnCT^@%oY2#Gs^rMuQt#kzB^goN9A1RG!GzeS;UvhnguV?(@MSzRYeKri z{L5GH?WCQ=a?q3`0Y34VJwYH(MO%-=&& zqPW|w-*J1IRe$Jvd6jt|R++nz zO!^T-w9|L=k8&AE_OS@r$C0exBMW605@))_=qI=qpY*l(6n8r0^XUey3rf1j&B(ZN zgnkC8?)G2a3onxeH&K0-cQVN9b4c}h-V)?n*b)R+Q-6L_@C5<}{~{iS`Bv6bkE-c#x2Xa%WY_?W?SwCEHM9h zow&Q3`W;&K_g=jH0Z&u@CA=_c?L&H;kjdb7SAUeA_@kx%=s*M$xGhu)C(nx4HVvgDQ)x1gwhU4Na+YA zA*BNOoxm=>y;e3vwgOW!v$*H-dY3M$qtYj}Spq10n&Raa^+6vC4Y=h*u^}HpaiTLFi zXzVlRCByT%tU2i-rGJh- za#WvOut&@^IOAC8qwMr!Zx@Q|2XWiz@N)lU>M(A{=b5s5!)UNqsWGu zZ_$;#ktpJ(I}eBM4G)Dc(L0h1KV6!Cca#lXfhiY8 zu1%DSgp{OQ>|8T6zFbf)A;gLMOF==jchjZN@J*MZgi!6TL)8F~GFX3kLsIU|&5~|y zVlh0h`9Dxg2MEjY4|mWF0059J002-+0|XQR2nYxOXS@6aWYa2mm+^n2`-Mf82neP~Lm8Yy`3`Te47SW_4Ogi}wn* zd$I(iKu7{1gd~uVLOSV{kV+B~(tGbc`BF$idi&BdGuz&tPDXd~_xtkuovpil^XAQ) z`A>PXySEyJ$#na1=@vB>TQ}`E<=$NG@ZrN*BX5~y+sKwGQ@L5kC{7%CRLRBCWB6sK ze`y&?hgm3>D$cNxcg#{zQ8q3-b=Jwvj_bCO8*}E$Mgx?&Sm)S4WSJH2sykqwUeWQA zomLfPg-0e`kGH#|#>5D)($vjITs2=R6iUV1#rljsx*I3h4NpL6FPIHf^$>$h&p<)Zvf$?Ls^fBckbS-nQyHhL#)t77PO2?%;;^g`LJ7`?%T zQTM`d$(k`LeWl{0IaPHv6KiRKPh3&rt!k_#&iFO3YHx1u_%)zpJD1n9?jl)SBr7eF z^%fb_i&Is7%E*om4v!d>!nVezkO&D7AqgV1vi_xrFsfHf)bKgYO(RiKAW9lUe@U>R z=0%DA-l^xEQe}>bC9@z2Gaz9bNSI_7MJ1fBX2%OgwqQD0vp5-HZTP-^3Dgb(b$~#rlcVzBuWZ#Ztt_up^tnOPc8;lYjd*kdk7d9k-MtWxi*$Q> zw_fg=cZKFJhxuJFKeKkB`9RqbfB8l8Rw#;+I&4}KdA%|bQ_}_pI2(OKOV|#0Nj?@o z2KZ|1hNJ1f)74&3crPft7Ze`xUlgymuVh(nptBFaZ`V=bqh=@oyJ2Q!Ovz9f?z42; zRy*}#vE-0r4-_X$t77WPF`rlphrp#ZUepUl&mfv}YYoysF=eB2a5!Hoe|z5($%0WB zH!5~&bxg~6ao?~eY8N~<7H^}`-9!%SXlcNWIcdUNEm^LZGrD7FGrARO*_9+Y>B2h^ z$6&ukRZakP4S~D`!vU3D=SJ@R#-vd(ig`mNvNS0q*=`n1$JDJ+-KrYLX^ToJ_!qoa?Hbec5_QC z<}P~*DDzZTnF=W}j;Khi2Mul@4c_x#tib>hr@=0I>Omqk-FI7_()N5I33AT0!?#DSxOxxTds)L{ zOSFw~_%T&17)2*A%of-{E8Evx^^>&?XAhsfm)?tu9}Y4QTDGPrnd*UazClo84T8EY01tpcZoq0NOenb2NWKYsNK)m zF;EKSy3n_46VN#>yu+lUB+391GoO^S`xvcNQO?y8O0TMFnHkeI$4$$0=8{AE2S)iw ze>`KualtZBe--5D>DEc`11pxHtn*m(dQU2Jl=DCv=c_TLEfmF8E>IJzK|MUU6r?UC z6VhF%Cc7e3R8VzptW&_a)__=ro48c36hUY9@e2<@q0k9ihOL_pB}Q9eOiitU6QY6j#R5hw}wnI%QtRIlJeEZ_VQ4m@-EQ*Sx&;qRZg-be?VLM@K=>QmP7r-l| z^U^NTU4)r8L{Kjh56HwpKt}3|L*GHdOH}PB*(IF`d=zvysJ5zvc8%?p5bmwIM~y$q zs>=>Ke-P5_NeBqEhRj`Mdx3i*PbW`}4FP{G;LrBKSSw7Tvy{*-ZJ!x#&jGTS2HbL$?;MN zt`!5aJdkDdiHVWYh|6b!Xak)wgA^62VKS}U zf2oo75R4@Ya6%|l3mUT`GOz-2#F(zJB8;?!!j)=-D}!)8=sRnGuCi-obXOF0HI%4@ za@DChwI~_m+A5S?7G!K@E2_erh$nbbRi*9BAk|^~Z#KFyU(h)myAJ=mUJ}{=bhMTA z{2_oXdg%5?uL`ok19MUa7EWVN?CEYf)JTqgL?%ZBXN6~~En8yj zq8$d*Q-(QQ};mbZ4c8|LU$%jqT?benef z<}9e`8Mxcqakm}0ZQ&}9!Mcn+6Lq+^#<}j06^1r@7P5FYvWN=0HO8hRg6gx)33^^0 z^m73MpTdQmJy5hTU>g(X%|^OiJRabo@3YxQEPX2VeLiu<5pSI_h{*kv4KhH;H8?A?8Ug3m*8I5 z#ZAfs;jI7KDkv}_%}YZ8e^Tsa_~WLa(-#Na71_%njH&DuI5dg?SveWDet2c7O1Mj~ zSB8w(y;@44IK^ItSMPGKz8b&pbHBev%PbocZp!xKTf($QDpiB>-D|bBWn%~GAO6|v zKo6@Mu&K9>WYZlDkw;W_-Sn*xERH?x(W*l~_-&P9%4Tx#`$9X!=$NMG zr=>OChR0KOKd$t4P;~0}It}wIM4g^~0?<1`3#X0=TZI8K6!uPJ^)6u59%*l#O~Skz zr|;qayJ0xPu@?eT``t0L|WgF~+q_Br1rXSKeyTOF-fS8`$By}>yYFKi9d8T|A8hzd0J16tyT(h@(C1pgn2!H-=AKUqMBKZQJ^m>T;TYG4ao ziKh=&!1h?Xf6?|H27(0C4STSn|GCztuwPJM7EK0bU{$4{O#bvse_33a)_WwD^04zO zRZ-Hq?^!DQb#Q24zrpJJ7FU;D?w>X~cMX+*GbHQZYEYy9PSsk{Yv_}@CEh06X)K>VAQ zP}su=)W73|f54h+*bV>ZB_wVrS97ncPA`57$^TE3|6j4RsyIQ!`ZsMJcgkCWo$^@i zPW_O?6>tu&`Yy^fBz)Lq#^b)zpyweKOeF`4e9bn&4e^U;~HJo=Y~3(#k84%Omc}DnEvF z>+)O~u1k93t7zjmX|*iwv7xx>RcKP|5brcAw&SNCn!P3r3j8=}8^=rASnF?NT_{I1 zHfX+dCxBz{6Ui}9qHf&lN%PUaoiK57h>26`f1#hB3RZ6A>nWz_vlvtO266zJa~jOy zJrTt5jkF+fKRx7rMqR{_EAvghZ}Brj)>&fhGtGrC-W)RBvLKANVzo^Hri=kbnx;04F6Tj)5x zTX&|{Mt?#?iyRpEATGTd&f>>)Mk#&Q*%Rh%z87^fL?L45Qu9$D!M;G@`(^hV4s}Am zM}qYe5Ew)Drwq5ciPnw6rgd`wQj==SS1NZ zcRW37d=i(K0wb;MUHmDAif`!*v#SB(tYs9Zoavt0TN;;NN%ox%YAEVz zW+J2y1w|2A!a^r01Wr;!ZF>(f@lwQ#%jCt^B7Fs^bnm)N*BuP0)liC==n;h8*Cc#$J0I4v7>lTHS7xecUAclw7ANj zNMYbf5N!F4u;@CrYblSCg{!dPe`aSM@s29L3DxstwN=F%ru=58Ao)`u%&a@N+2th6 zr1(=2~lTj7Wvqx@>{i}((W7#jfi%|RwBO*7@V-QXY%};7>qYJFFWNak(Blf zRNC#Bk;5A>K~{Vw+Wro*eM2|#Yi$O<_Lr;$%=RoYo2TVxgXUWGS+i8|e?)i=if|{1 zaQzZR@Il`ABb6lQU9z0dMPp*Gu)Q-I0s;@r=WEHaQWI?HSp2 z(fv}C?Pb_t>WFlX$QCcJf6Wakj%`7HU7-F~YRkIDhDx?GY0l1X-0^#td~_MI!lSa^ zedDi+%L zOeFbtu`R>DhZWoRamQDCwHP(p_zzJZKf?a-+IszAxCe|L8-$Zk;Mk;hnAWzRH*OuXv?fueY zpNQ*tSG7C=7?ZDyj34ntTL}NqY6;PfAIe%jp&je zyAdnGNGOhpMnbU?$J~d6#Hz?cH)1sm$qxpJVf+kJ?Cm= z(tj?9^*1*UD{VOv7nhK2C5 zQkLig4;4EgYpvhfuq1Nm6a8qY$T;W^#%6VrZaaC|85(i}qY2s=KeQC#km3tFJ6_fs1NlcMoo)FVDXC-0!XC-lsOn1oNxP?~>$H4iEsNNDef7w4ZiEGjH6_8`YQr=*#yKtlRY8@6Biv4FX z-L8kQQE`rshbnsh40!&A#@?5$yIM^lBo3o)X6HqN?S!?tXf(JEe-1=Ly|^A-{036) zjZ4=BxV-l+P_s_|c+#D>yC?Wid?H?b5<&66QH0`uK%s1zuGMJ08xejtQMvqNbi7MChV7sTYZE+9T9pPAoR4eo02AiNPLD>+&;fx zqlZ|Qtkf&RhWN=Oe6NK=6Gb z!uLh6Km%Zf@RE0elat?!`WUUxEOBDFAq5gDnAHoCtzn=GzAw)Mt7ZUx7M& zCE4#@(BT#w$40SuwJ*eLYF`Qz*dG?JqgNOY8@yK(yuv8oD-y4l0(hO1j}{kych(bC z3*O}$o+~;~%+w^Mx8P3RN_GC=xw$n@`w z(2IA`ZjkETGSz!1P*PNUAQ~0lOHmOA-WLfp?}tF6hzG-X@&Ur*2YtLgMDfI9{~-kI zhe^zjkkcatJ`XBB<|FpwXZ7=gr5bK*fV~!Bc~l#ec+CgPQVdekWdhJ?O-XZ$yqlB*r&U4EZgj zR9t*3>>zzR(n0!;)Is`gO$X_FFc!SHCB7f+A^iY3(u-T-hw_VC>6*7Q#xmkZwQogf zN$-`Yre23?X*nPM{RdD>2ME7`I6#mW002cv002-+0|XQR2nYxOI1ZSz*B34d12_(t qvj`%m0}VJ1m`=ZeI6#mW002dkyd^CII1ZST>?J<~I1ZSTE+#?8!MnHs delta 6116 zcmV@6aWYa2mq+Ij*$&Ce{cbULV54WvJuF(Y{^2QnbqA&TD(`d z-IFCC1wsl*2uUCzv{ce7A(bQ~r1#!?@}-c3^!BA^X12XOos4wy_xtkuovpil^XAQ) z`A>PXyEhxfiFErh=@vB>TQ}u6mEK(L(4j+FBX5}%+sKxylernkC>0Jrs^ntnG5oT_ zf3ysx!z@!UWI^*PK#&z4sjXARwV-b|OSm)S4WSJH2s@q|nUe)oE zomLfPg-0e`kGH#|Mqvb4Y3dn=T{T}W7R#mFMf$Wpx(g@Ri=KeeUNl|YX_Snrna4{l zT8!O>GU(%$and5$t>3aWmy7Z{DX;eyfAf>3W%U|)+vqLWR@Kn$G7$7m>&1#$HF|>! zqwa;_vNdf~`^u#WbF$`YCf3pdpSYsLTh&-gobjt+)!y8m@vA|}b}p}H-9@svNLE@T z>n$>&vR93C;M#jT5HvXKCr0JLU)h>tT3KGL>a&BU?HtwM8u91^9?O77x_dqz7wY!Z zF1^w<=L*eV4)eQUerD}_^MSG>fAWjwtxyytb;z^|dA(YQsc8cPoQ=MrC2R-0Bp-_( z1$;Gj{gL$Fsah{6ycZPS3kr|;FN)XOSGFuS(AoRpx9h0zQ8N^P-7vEp{S{iU;PM9!POIE7pwC)(%v~Go3b|pzpxbRNI zG1#wBmE%BNLm+R_a6o0(x{-UIF=14VQr=LBEKLeYwwoo>F?DNHw`#^Q+JaIF{@=D> zN(kpG#@s#aFm$I@HTrbRe^QbY?vGxAGWvL)jh5_ zqE{ykXRW5Rk2R7b?PCN!>tdRETr7?zP-VrpChb}Uahy0_Rn%_6^?me~#Sd9P_ZAJ)(cc50l;R57DJsa)1u|- zfkL?kGD8w6AL<#|e{?t=L)CKLD1hAd$-&pn8)1`emNDVbE=q+>nxdSp#=(I{m+ruM znBW*vWzn(X4f3cNW2OQU;wE!iE9l-T=MVM=*Oaz!+*Z!e z5^ZA~eoU5%M#%{bvl%wf%Jw!_{bX&!*^Oy|k|bvN?66Zce@m07s*FynA>9_x)K;~1 z1;)H`wWwP`pjIiEtEQuMRQzj*>1_e7+)t`?8iVzjTC#J@U1HD#Qr%MA0fomTYWH(i z43t8-F7)mC1a!6w?=a~oi3)(k%qJ!7K2B>@lykI%(yOXkX4pUL4-jfO)Ve6(tiP2UVQ&VeTIalG~ zqBN`~rd=uxA}Z}J7L%2e7}_re2l`~)EVOz^Wgz9ae>eakIH->ah?>iepKqJ)mF4vp zNabn26iKr_RgEg0ZC4Wt>j$JQ-?s2@6oi%y3!)+^v;Zr9;gXJJ*bdlQIsgXS3GfQ( zytIpS7h>iO5!8#s12SgnO&*R^yMc z>aqh4e}pu90s;c9A#+#R9^jtH)5%j~L%?4P__Mt*)(VsJu=GAe$1vs8m;V>%)De_6 z*uk<))qvnj-pfXC2m94@5+oQcn}wFH4N|Q4@nQw}vRB0+7)7aCrn8Kc}sx2!TfAugZ zl?{{}W74RuopU7%91e`~!TosVW6wZ!KNI5Mimo}7vf^$AAu>A$_Xs{n(z9ow2+sx) zj$+TqW^?m>7S`^`+0{Id=72N@q&XnXNu)U<&AFr=U~&{S-Ars~X{8J?*&Z;r7G zw;NDT8FsfbWptBk>Q;A&RNY;kf9Nh5hpgFdh#W?t+pr8QZ|!V1%+YI>(@i$$Htp^+ zvY@8t;BIfh-FD=*hO0ad>oWFS)Zv~w=eku^7~1T4$m03PA}Z*X7@LX+s?Rhh=(%~& z&-n;^3Kw>Ef62mtZ4}PU(GYIr1+)NE{Z%n z9!}B`tU5BKmwF&2Zi0V!j$wD9)^7E}+THl$W?9qsXz7lzfeGp0rJ57$Ufjz|a4+nl zCgp)})_+Y66c~}_rJ(>RfA%u`abwWwiv#XT?Bx)~RQ3uS8byGtoCsS#ygFGU+$Gp6 zLq_aAEu~PLVz0uhx4TzgjoHFW&80hVcH|rnnC&QwOZSP7h$+CNnX0OMs-4UdwRsP8*5FV99e;a#)mR8ssLvoe9 ziS+wst$oE9)Ea~3az(Oz2c-G%CwmLJ>02RK9DT}TRfm2U z`c6-63VRR!d@z=Ff7`|l5BG}cQm5xva@wmJw2lJhTEndh*n=+i-iwP&;PP?yJ_(=i zm+<+JmQl!FAJ975ArD)Yhf)e_wZtm;GgeDRG_gR&=NnCmiUn*`2R=@e(W;%$viszDWnm_)Y#8Z1DoMW zJbkDNw#U+qf427s5G0^%*o_7K&$Tv%{et4MXfiGXs~W{*@~2<=%i_wk-lMUUhn-)k zijvlS&r;d1gEIsB4HnV>z0UgA6vIw(&9HBS-P`kMq>#i~W}KTjk7pLzmh zLTOOef3|Rpw};-uJ3?>bon9E=%gC+BpZIdn1n+798#t5pT)b(NR$hTz9(7k%`B9`> zm*>iGUD6w0MH|OSt7UPI4#iEcLX%>Hc!ycF9Y6ih>@{If;KxYYI9A%mT7MhsLOG(b zLGz_M4jh9YPmX~Sb>m)7n2Y{xgozVFOq|pRfBpPquyQM3PccQG!I;7~kOR=1Q(zA7 zi6D+|qy>rlsUi2%8X}HdnQ!uai=Q5{&Jt^%X)c8E86nfn^TK!w7TXkHDi~lizBS~$ zEyDTC(9DuZXQ3OM9k{{cWH&e`;s(7K*!klnH#j#y!+E&U7H``5QSe?6j&UYgol901 zf4v&} z6b7CG!Is|ui>_lkm+~Z8xC$F?e|F|!Z>aJcQ9VypTUESY%5Q=Sl0OZ?%(`=$T~5MG zia#Ae{){=tKG#E@DIfb(ezTTT+MNTT5z(&LN#xH42FES!kv#t%2II}m%T9VqB&9tE zm39keio^)`cF`^wflW_uo)&C~MpL36G8j9D&ve*c=JV-jH?^bxioZs0wW5b+a8yeZF%So^jZYCMP1YJtNyL zx?hU2y$t(Hk;V}nfB4Jme{(~MV^@%08>s)4+On>(p|b5vm@{+xcKp62A6)V)c6+Zj88CD`CBQ&-S1_%w?#AD1N9m1?S6)Pe+OkakL^1#3B8Mw z(7P!KAq95S_=A3se=i03hzZ|Eahi7W{-_&1)F>){fTA)|e-Jr8JWnM25Jf^H`!EUM zE%uT6aP?6NS4j6UneO8hE=Z_PM1}e!*$@Xl6`J7F^(Me(7r)SiYE@l63U0oLcn|_bD{{Cp(32vtamasLALT@ne{SsHj8y2DK%SmUt}Vj{+xw-b zJ`vaPu3Du47?ZDyj34ntTL}NqY6;PfAIezjp&k} zx)CeFNGOhqMnbU?$J}Rx#Hz?MH)1sm$#ICeaaorbX8 zG`G;-N+>;DO6Fls6j@pz7c77+NP&+MpEU0?f10lEt*yV1b;|A+NGTI7^PF~s> z(tj+7^*1*UD{VON zrR1`xNdFkgg_jC`UJ>U(UJ>V$0WUxS7_7FQv88Am*t622r(jMRG$x!T&#M9(!$Npj zQcLuKhl=fxwbpN0v?Oxq6a8q<9dr61XOlg5Ms9zL3qw#0L_l#7fr17uo(lmV2VxKn zu!{^(Zc2aq@Y%Cw6}X!e=xuus#Q~CdsFBmxr@_6GYZMuO{dm^|s;TWpUK67}<}Z=X zL}Col`2;)@iA()6k+=-mT<%-?iaBQ@ab<8O5(i`pY2qpfeQC#kmI{T?Fo#5HL8D#)>6DKD@#TzIkdY6BJ+iv341 z-L8kQQE`rshZ=hRGTscB2iP1r9NH~R>E79#Z7fY4LUYD$_2BJmMcam(C- zjhxeZ%dCPCH#cvo0KNxRcdrlNmmq*&3IN`?$d-UFP6WX(^X-ET>eIc8uRtBX zlI(XM=x{TRW20ES+85$A_3s1<><^3A(Ho2pi@aA9yum2nD-y4l0(gUyj}{kyw>1(~ z3tr_Lo-H|0%+w{Nx8P3RN$t|k~VTb1xRlr*ghA-krU-5}MwWvcg3prokyU^FVem!cvLye|@H-VcFB5f6p&&MM%t!3U$!#Kkko|yr}pKZUG5O>2F|$3Aw!#pirZpPz&MFA(;T z@{5N@?Ux9(Ncd$E&YO=R*b| zlHMCpO}!1((sCaB`wvh{2MBsk&`^*U002Zu002-+0|XQR2nYxOsJ4!?*B34d1E{u+ qvj`%m0}ZIQj!t?{&`^*U002ajyd^CIsJ4!i>?J<~sJ4!iE+#=NMDXnZ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index f465506ce52360166db37722945cd68c13eb9b5b..77ffdd4b08fb04a556430a2ca34e074c665a0254 100644 GIT binary patch delta 4091 zcmV@6aWYa2mm+^n2`-G4Hqn7bFvK>5MXv^C1a6BasgP8xk!Ho z9W|1S$CHW1rQ!bYnq??p3|j!vF71!+r6shK9>Gf`lH9T$8ZZ!SVyF0Kh7f_ZkhX)`Yep z6OQTWO}ma%kl+LXPC3Bw$;xQp;PiGFz6e3600@-;!9O~iSrbm_;jWlAOq;R92uc+| zsRk$kdF9BV@ZT4QBk5#nlgvil1tF{fgtdS$D0lJ*do!V~xE6}*>5!i2=DL56C42Np zD4vXJG4pfG8c0pX`(oNgj2^4BZY`xHBAUE(%(^1P;{fq^KwLg1i1*1rsL{K1E!wiN zFQpjpp7sZ@AVn{K4X7q~`!OoKkQf<9{M ziuJK1Z1gS*_toZIA^ELAz7FJTrxlaOp{n?=B)JVpP6x?xTNaaqF)F!lBsT-(W`f-K zdAuCd4|Xj9MOnzKB23v99Ci9;TTuVA1VQi*=&@)doQitHfQAJcx{H5DDudjg)*~M8 zwlMw{9{F%Af>0eZhFQHXofCiRD74#g%4U$>b9%Dh;q&Jl&JfU1>%HLj(Bu0zeT(+<2MHLE5vd=+{^ zPwU~>ns6+m&6S2!597ZRhTIZr(Q%#ToEB^0bS9;#;aE)Yb(?=*wiiV|z$Ho`wYH5q z6Na?b>2^F1%a8z6N0e_92(n?cN*%B>RSMxkxUO%D~ z)w%S~OJYqYizOq6IGIE!ckUa)0?8xnAW9WL!wN7Q8l`079>v|2 zI1UlVp_twkY6X8aqg%CDc45fthSxr{KB*__DR^M)v|G$|E~&lYR6CT1XhID@?T&zY zCs8VywCm7;V$g7bOb)$mC?4*s=cD4>!K5wC88fX<^AYqyNf34xz2ng0lBsw&X1j?< zt|aMEL#phvE~4M;B9=~bLJwsF&Ygrxh*y1JpouhI-&H>p#3l%LleaDqrisY*bV^V3 z)Z|`p*&nV1#ygg)qvn;jJ8{lSi= z>^5`EU3>SKg@r<2?!VWQX7| ze_-;<`;2T^8Zxx>af8_&yQ!{xe(eKSyvUjd>)nHacyMpNtwmg%F&I8b1w&l!oi*RRlRr4&GWx`3{;^YKZBp2g>Hp@Nq#Q3w)5n3 zhnGe9d569iIFkMWH?XT0i`HH*aqVA5QeP=T>Z?TRYe?$rHmPs8e@T54Nqvh*ecLAW z9c=NgMe2Kbr2f+;^?hvlfkWztg-QLF1QzoVw*45}!s-y#Sf2p4K-jVSPaWH?a|w&` zXEck?ZN+?HE9Tz>)B*OTOEF*J=dV3J(XxJ*G9>xyB6|78(aX0S&;P+2Ch+e7jv#+u z04}GeA2|6RQBVIZf1;}^^^{ttP$YFI<4|n8 z=_kq-x#e&%KT#&w`cNjiF)NcyKT#$Zt5uaLT>GiOzp`avGX9lmK&+%}ktug9NwbF!l?b6qMb`F%}Jzxe6wK*_NzuHfUa{hdEVG zE$|p7gz1zrr_zAEZ}WRQygw6u*$ByfXsX#df@1X_1mO_a=0_-Kg2_w35IUdm!jVmgDW2 zTk|V2E$*3vnNOs0!6AR)QzGFr zB;j*AE_{I^|E2^otS1ATNg&{acINmJqs>>8IljgS`3;P=l`N0uFfDX1Cx$IDx}4)z zz9rK^*8Y>LZRI?6fP9e*qJIQRn&BL^rn&ng&*`YNvf>rq=j25gZ4tFpR!?>E-;AM z_||}{P07{^i<7wzL;5fH29n!!XI_Krmr* zVX(SAM-wGiq~!Q;B}N$|+4i#`(UAzTaHL_glzI z7Nd*pWs^G*G79H6%Gndop&fQYlXnr^0YQ^g5-I^Bvwsqh0s=pulMxk2f7zR>wJqKj zIJ_++-af!_K6I@h{>A4BcQXBmv`=Cm6FdvZC;077r={f$>{B{Rg94vnlcy|!&+*%f zTq>5b-LWsQe#e7t>`Q=Et{bZpI)ry49Fy2r2<~e!P=l|SrgUH$ZqcjXvue!nVP7?T zUCCrj3n#dm>Kh7n-`e32GBc928?qhkoxPs#G3fq4F8L$YoVZ^*Rqpve zIN)3OaRvJcl%kfvsN0T{3Kk!K+udx!epALALQaiHY?KEM)LP_ioMnLHabjD50nT1HA~c+ns1|5inJ=l^ z;z~%JZLfsX`T{Eh^*-u@lRTOgiT`5rm+&A)`Zx(GqDj zB#46ANL|izx^$fYbsrX`x=dYwy4Zo=JX3e1E_QOdSXh&47b!7|cx~ee5t!tEy7WW*iA0G^qcIyc!(1H}&)z5*( zYCAZwN6`kq;6ok#rd2?YS73PiH}`~!UM-_{r_?V8dC&J8l>Ev$l#lJd9;E$s*!~;t zkqUbmg}xo+S-(|#k`vrI~m1Fd9gAOvz(&PyA;6V z`M~34DCz^G&3^nRkn`w`-ZjQ`Aj8uz%|RYZp{L~mFCJ#Vg9~^r0nZ~;H@i;fVlNeZ zFM}+^Dgvdrxq=%hxO;+ICG1P=u+r6`d@y9cIy?K-)tS+)4(-1lS1P-k7Z%l%9~~G8 z&h!TJXBwx^o|8ZwB^mT<0qZ#(006IF002-+0|XQR2nYxOI1ZSzejN-812_(tvyCXJ z2?;n3m`?O-0qZ%FKQb{NI1ZRjap3z>%?bbjIadGx6aWAK000000000000487k1``4 tI1ZRjeS?U=a0vha?@<5%3;+NC0000000000004rM(J~(fEHVH9000Xpj_Uvb delta 4138 zcmV+_5Y_MaW%gwaP)h>@6aWYa2mm0oj*$&63s(u7lWn?ayR(vQkw|g@NRhipe+L~k zl8ncbiN>Yj{_vV*C}0d*0MRb(k1y5|T1t=Lr4mVQSq}}G8dr3!hY1*sk#Hy;>Cs~` z=n=Y$8nKiXHj*F_>JP{J^pw^XPV{8LJz8i@Te}LgONSHboku2CQsOBo@d|>sRP>a1 zM+aq5CP4}qCKOAIpp*d=A3!OUfA<~>D2macrQ&;xMwnpv0agHDmC1`o1FJQmZODXU zdV15YBNZe#L4Z>ZaD1{d8aOz;?T0Ty5GnvdB|z|x&SutxQ+l{7rVZ0(EHQ#o1yHI1 zN^fX^Ds?FCDY42=O>TJRT62j|t*^G7xI?Ze5GEZ0t*E zh5_C+Ld1o-BE(w&;t7DbLS8Zkh|$iQMl4ByCIX;I0H|_o0D+1|2ne$b0-6kfrU0NS zxor#pSuVKesH6$lQ~UH}{8y6P1|+A0+ z4(bQHmVlxxWL6QTYzvM$eX}j7|5<_{_y_b@G!jllJz_w^0u9~8eY*^eD@Go z_!EOvL7H{a9FGvBI#P{=4MVI7Clbjt)oiVa?qt13+@jNJ?5gLWmr`#c9M@*Hp|vf{ z3CX~GpO#wJp6SE+f0p^;TD(h38Iv14QZQSzYO!eUVB31U<#cx$HHR^z0GKq!pp+r` z`cis-IIT(j;h00QiNe=y=72IUR;qJFVJo0&C18zfX`t&+v+T43uSm_Ri40$bp3u{J zIJPDn%V_hYA=Sh9?}Q<@gj#f5r#YuZS~#6aX=*qY6MWs~f0yk<(GPHm5=gCWqt1jO zt#x^Ohq7F4f$7zl+~bHH;Z%>74oN~qXCWNbmVLlqqo=geR8+P^%hlC(c@Ry^|yeJB!|NXmQC@JRGy#L?l;| z^r#_K_E{IvZ*~z&r#YdAvH|B#LM6njJ}}Tk8n5pvKMGkp@ZH|#P%?JLsB*5+lISXzflG#E^2;PeTSTH>Co-0CS6 z<)x;7=X$lgH}WjEWr>!TA=CI_Ig+;m$Rkwp%6#_rfmvEaWhq&eH*rC3_mpM(=y3ND z@FM!4yqbf$2BEGk0=1K%?kknncCMnix}txN%W~xXq%sIkdLo?KWb4fiit_$oM^kni zx`Uf-TrNH^oYtWvAxNgyMUxqbKHzN0f%=X?9ergg8PTGE)tG62Bv&twY2BtNCZh5I zsGtL3G68wb=rc?N1k##oeOTXMDzGA@_w?F>9wbSkypHs6u;eT6RDkiG1bVVVa2S6u z`Q?2^wk!=9T6#Iyc0rF0hG{r#CwJlWBbIYV!HO!~=4tw|tbsYp-2_M(A)uZtAPOlx zIBGA9>IDalOR}CbZoxlrg7x48S&>8BB7s0OgAoR}56Ut39XXD!kSO8`Nm4C7CK5(Kq4@ zH(5$Q6!`MFd6o}DbstVZmW~QYj{}4TJ^}|m($V`-IYSrI`_Ycxk8z7|dOy~EM?Mbq zetZ$VpFn({h^lN*3&acnL@y>Dd`^%gWi|O}VN5AK}ML7MQ@4h2nfcm|# zh<<-X>|TWW{k5&%ixJ#!#$3Oa$=mw91oe9smJxqq=y747F|WljuXFT#ea@&^9o-=L$8|zA-Ih%Dxr&U+ z?qtff4fk6Fcq0KE)@~;c5aW$uqPvOE*{k|0Egb1}jdwE{$1P|Vx5B7X_ZoT;_=# zj+SO`(9m&P6&=&@pa54r_m-4YyKCJ$ovewg|1G+mm9VqQkbf@)YCF}ik#_HX3bbt? z-(~k8mZfP)E#HkW@A3G|y^@0KDxu%8)#B>}^G~Xb(pHORmi+QPMZ(D+oN)3-w`FqS zN?kf^b{!D)sb3cZY2kdb2Acd2xJ|04!f0%s!FXZ#s;t_1|SIaa1mgkv| zl4oMezhleC9DjPeus=OPHj4sJ+LrMY4dQhAG+73!P>`R&&(A`)Lcb(Gms{I;^0~vy zqWru=-wPZ`|9~6V)r&=Iua~&?FC(e16e0ChBK0*S^>v%nH{5@uzKNv1MWnuMlll&} zc-JEJy*yI?X_NXsw*0^$^~1uX{!0Rj`3T#7jBR0c2y3iQ09zpJ*!`!DZP&SkMfo$D z#pkwSzOWVZZvyH7`_iSDukiEN9-nAgze^dC{B;q%eBdgdtIpP)~~2(vwmOEtImXo)llMo)o{O zCnbO_gSMWO@`8F&DlCqbN{eHqiUx5yt;X*)fX5XJT>%hkPl$R-ty3tHI+SrJHs16T zWsBT$xR{?P6Ks7b6Wy4VNv5ADlZ(}=$`r2sRN!CPvM@6L$}}KWQnvE=CsPo$7F4cH zXETuc650T6eo3XY)Ks>{N!3Au+j1EDg-!~}?&KJI4wJhICV!btRyYSVuhhews;3rs z3=_h1N|{q>z}~mY<^yG0$MuxCcxPU&>scEuk}}U!$#!V(A*UBBw&x8NS7~VjGd9#qg82X{+=CAS= zlKHq}m~TtvRh`Q-_^g_LEG#UrGQm4E=XcR^-op|82_sCDmkjfSLa!E%7C50mpx);| zWlh$r#SBgP0IB{Ess0yIEw_!3t{#fcsgB-og5&HX;tW51oWsl~Qn}!efAA@h@EMZu zxg8h2K#_k_0vXnmfz2cka6&tCe2LNKE6N;SV}$$$M%zl3M{}4Kx|b8f78za6@hjhw z=^$(W$@kcr%8&T*zvw}AxgM11qQ$b?c7Adu;ul$o zWiQNQ*%TAFsRjxcifHUiDwHZ}Iy-t($$`QT`k5qE)^yUsEtNrgq0>*z#^|yAMPGuaXdpe`Z^8lFdPpdWw@P$1qN=NLgW$H9(kT+hUkxb0L_pc`#Vr zUZaVUD^hZNxDum`k!(9#C!t)OutuELe4N&BgSUxmG$E2L0AOq(UorYkvtN-45YlS4 zJzu!79VnRMryZTyK%m^o4wO6FMzsq!-@yXqu2O}-nxsmBdBNTUlL`?MAw9{>_98cv z(an_N&Tq32WQ_BD6@9qJ|=h;kWcX2 zolZ;38`!6GmIehr!zNEz0-xiz7r9g{WxHcvVEv8<+t`-?t6Vo$Cv*t!MmQ$1uMphV zVxR_JF-_^fG~A+Bzh~8$;lsXa__~tGm=;cOHPts1?7p?bAu?{}vhQeXCp?B*J2qrH z+Bh6DUP3fl+6VlMEIgfA(;Xau*ma$EQ>; za#IT2jGM^4%O0YA+bo_k$K1_7)d$&A^%JGXjGh5QvtHsF;e%i`K#XPQ6tt{eEyv3h zWbMOxRbX=`1|V|kCOI@BQZ5F;vBhoRKF=>4k4#TBsR(e2Wl(? zbrA-<#k0m22LSbFr5SzL!B3Vk&`B++4wp6x=<*trGSnc3A1^P(B#4U!9%( z>gvqsR)_Xqk1Lhk%?o?hlOY`#3GVa;^Jf~T&zX}#9VHo&funvm9RL8YUjP75O9KQH z00;;O03fuEvw$583j-juj9}Z*Fr?O9ci10000300RKF0000gG5`Po0I->=ApigX diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index e046604a0aa80e6fef90dedda625947e9d6efff8..070afd3c26b9b9712ef0931da9dd7ac5daae3ee1 100644 GIT binary patch delta 7161 zcmY+JMOYjR6Ql@0ouSHATa8XAg4i6wx141L(}m0&u~`;d%)YT?(|SRX#aDBf0&py`=p5kG;rpgCfZ?#(5ux_8&5= z^V+L34B?6#85E}_xkf)^o}&{OpBplm!_>XB*@E};Hw!K??9sBC*eW}1av$1}ma|N= z6R5spX<^*am?ZR7fo)ySBOyCmS6R7+a`AUmL$-bggcz`j%8&DWoaRo$a0j5nP&=_G zBW3`0X07W65CqQxuy6oH-2yhG^GcE=<42YX1E(@-#Bd6@Vo?+RX_Cm`&028TS(mrw zcdZo4(5b+B1T5ZBP(P9^>R3^A{v@%-{3v?FsMR%%3{%!r#a*mx-WB3XIVK6e@Os`{ zlh1T|n=%kv;tvXg6<|EH%avGd$Kw2FJ3X8&P>dT+ZMQiReGF$Aak>O$2>+7=gB9HP zpTI_W5l#MaPHxPDT;+Sj?pv@;m7V0qq11436)Z$pgpJJ5+ z%Ce3#GiNzd^~Lx;EgA4i{nV`X;8e@UPO0m44$J>0ot0#zbvPU!?|cN-SZesKc)0bz}9_?jKe$4i)^L+#G^5&!<}szRin?A(Z<+$zZZT(KRC!A zV!SK1hrs0C!q57vj%vt5CU=V5!Cr|E)13aWQ6ztu+V7CU?Z<1&Dvq8piODwx3NX`%D;(XVVsh!J!LLb=t58$ZXCjM*8LGuSJQ7U_#J_Vs1TrXD20YFAGVhC{Srqu`$B9F&gz7tu{J(T~W#XpvZI^e5m4uZdq_qZf8n8g!VYjEF`GR~^bm)ah~W~m^p`GzLAG5iDh zX#IwVNM9+beiwta77O5Ul#)MCyojb#@tT6;Q?r{S)-(N9TulMYsT&ADO+EL@jz?ys}}J0j}`aSTl;a2eKpn zQZ%<^UVXJri(BYc{wN-fJJw)}QgzbHJbp832Cw{AnsI9iBaTa=Z%WqJLypJ>L!I7~ zLSdUb0V>wFt9gvSXV6-TC%@mXjP1pS#|a3?a=Xen4(jtf(I7F^6wbvaaoJxNr#q(; zngB}fRzLB8FGor%zP+|D$OZqA^&9>s&bjnJW&stpRa5wi#)BTWmFKn)4oYh5CQ}6C39Vj-0=h^>){~Au#?AFx@%LJbb}eq4X^>i+w7OAvpwf$Znv`XP`qU2i z=k*fpcvyY*@RPj+3U1JLf>eZPG!4aoXvS^{vnl>m4F2OjYq$Lbf$7^h`&@c{M%SbntUd~DHB9_s5+(V;yP4aim!*wKF044pp z1?y=)FG!qNV&kb(*Pofr>g(0ya)dCLo5N3%Wn*X2^6$7YPeY26+qF&)IWArO@CRCX zUTbAlkgLekCwZLgy&Q9N)X2&>LI8tnDgK%iZ;3=c%!)BLyoE{CX3T0q@;DJNcftHZ z;FA6rJD+LzO6pvM!#Bo^bd$hwC|PFIM8wa!H;vi8-$2xqOq`M-o)jghxCz4&AKK5X zE`-Fv!h2&{s$9WReenQJ)1Mg+I<4f{&2A($J;I6n8X}P|6P`Pi>~L08#I3ZOL+E`i zj!%w^8v;ko7oU57w8U;HA&4V`vuo{o9|nmB)030}WMup3JI@Qz@ue5)|TCLxcz5JfzIQx&dfZP|`pa zn800CNVk&|AJElGR&VNc3`i87-mpStQ4<2TK&=b>p&USp#d?-4K&_9M%akv-OH2EO z=HA-3nd8g5ME{M#;0;r6ll45;V$0r9Tq%NOqS4BZNt~t$P!m_H`r%uiVoJ1JH@?G( zdqZfGl8ykMtikQ!l06vAFL(9za9PnsTsK^L&af_V_b+~qPoG>s$RZ^Y$$HwLzOUxY zm=mq%)h9OsC&UBW{g5<=PeqWzG6Yt>D8Obg5W3__XMdUjr zq6?^_I(MFVq7p*yvI^^^o|+7G3w8mbGjIVxz?W}$TN%ZG9?~5?09F(jfowrX95-er zzmw#0xdYg}r3UU0_IoHTTR1OkMgHxcl3gJ7y+_8w_;-L|?=)x5;#75$1|4`^2hL`j zU3(_Rz@zhR;)lue-ln$5nr{n25xAlYqpJ6Gwd9)Oh)az zDGk4gJCuzZ-}YUsth^0=<=9*#jsr{~e(#DX{RHYx8wHCFo<2*G%CXvv|)j&dzgBAQ=%pQ%!=-cDt@u=p*9L*3i7@>ZSzV@oPkq7Xwb{kqb);`r5KY zB8p#JGehI9*(p`!2!C&Mt>-aY&^vY$IamA3?pF*dAz3UR zrU+AA;dCwwvld%Hq<{pscYvG0VZ_6~(M{j(H*Xw(@oN$mNNA%#0%N)$8XVs@&@+3o zVB)=nLm==zL^U#bq^Fqt9)A0Vv0I=U9`vj-4xVzYX&Sf7pFGC((^*oc#l97Fo_@v6 zdLi3E@961`{~pVb|gz16VU=vchW~ z-%9=z36%;3ooN0oU{fe^Q?5c#NfW4dqDo9cR`6#~=$DNG-o%yX_tmPY$SVMO`XX8$ z!Lsslal!LPQ%YrHIavza7+WdY`oYK9^U-rAS#WbEQM(Jg)!=+1=Xd5y^zv2z1(ox2=Go#A$!x;=c4U}Eh>w!Sg zpQJx#G*13%PsOd;`61mvI!S{+I4+Of;pkat}fF7s71 zRpUMw@AH`Sj~{zMc}TsWRyln-j0Uqhj7F5nUZXmn6ZVTzLuWxr6UnLEqh>DFV1tI! zti`+P;#y7o5c)tzs|d*0mNi}&DLSWB z`sT<7y_%(v^tOVE&QYGCEgH?ijWdgeIuVxTg*G6b^T2Yl*=CyAW+2c+b`MQHO8GDP zhg&Sp)2s`Ai_}|F4vXOUg)eQe&a|8Qi6=sjLz#ZI^4(N#W`Zrs9H=|ACViJdtroh~h#OOn4&DItht ziB%yq-RUG}?y!G8T(G`l!-7f7-A+xa5*IrtT+N+K_AkDomJPI!+GI~n_r$CO>Ia>b zoA%SCaaM+W17X}QbmdC~)8JpNngWKSZ;lVRaRlK;OEHvlk&qxTu9hdrmV9}ifR#<( zulZ&=tmI9wVPDa@su*%zhSE(d%X4u}cDNq!g1`-p&_+4xQ;Z?AderD3XbGUOfmWAY zR<>@f!ZBzmGM`zNa_DqFgy5Yv)5wUNN_YXNgygWsZyltugl=kQ+l283pEwHQ6SmG} zZ3Ju=h(%*voO!|e-@$OH3I^VO#vo@CWU#*H)VZ;QEUxa$8$l2^1P~b`H*C$noqewEGzYd}H`gG@s9~ zV(bsA)vUdcf$JXO?tLhR>&8TLR?bT52jMk#JUo*>0;w=x#5aN9%2JTFNUX#g60&y} z@iu9%!=6Ifje2tY#N;r9iGuh^uW6NS(MJkr zWYkfyo3I}YF*^5PAMED@q#N3jO*l+1gF&UI@2eKG-7lCE~4|w?_mn`8*Gf&p7WDER3#yj2B903{^p9=(z;h zs^#z4<@f9{OZ1@BAYG~67KUH*JO(1}6IBN}pGrS{4w6Rcp&DMJ3Lt^Gh*gQAlAXjF zg7rnI8G8oUX0XAl%zNy1d(>!eB47Sd_&Kg$6^w+mYbV^_lCL*BIEGo!R<6r0@OU_JXoRBrj5zy^)%-o7bh+$?^!Iey=$6e-E2` z+QiCR&exl&>>C@m72{?>{Kj7uTVjLJ5AK!Oklt^OpUh_1rORN=0(?%YJVb7a)bRd} zQ!!3krEc2pP4(WNrCyDJ9=PO-I>&;cQ(ZJ#loyQ=M@Nl1SDobX=Tbd|&s)#cfw&NmdL^p@{=nGds9jd%i+uX4IPR$FRuRwCH|=Gc%&R7($OPlTJpIfp?6!y-2ctV52QM|NEVkt(mSayg_I(hCOA|P&;?HFZndTY3tz4hge?OTF)tG zMkUQwG#x!yRP%T+YdTHC$J)E5wB~4Rt_>|es^A)oyi7B@S)`Q^nRn8` zu?ejyoF_b}RJ!9LYK>EH?mCgdSrxuJFI?f(NNvpPVz3l8Yg*IFWo}&81gC!6H7-8K z`7^M6UiM=a3dP*M!|r<3Y%q%f!WuS#pT+J}kmkfy(D+bb{0jkyjU=9SXwQ`dr7+4J zp$zAI&=(>{)?CB&3Aip!i(icaTH5GnZKANS{M4%l%rlO`nv@AYy&w>MX<>|i%3S{^ zZq0rR4Td=$`Ndj8{G~-guoAsl`%%PPK|J1h(cCc&FY&<$C7+5a8?tBz&rXw~7A1@1 zN1prX2zpAE!2 zKS-=%tL`juGAUYDPQ*lGg$rWayKJTN0B77Dqgtf@*qu-I>k=PWf-glN8n*fTu#C1d zvt79>@c<94r8J2G1J*+C!JFxRLdc40rBQ9&m4?5ELt(b*a*>{)iS7FwS3G|N9}L~l zj!)(^cF?d{|0U_bW1!jo!nCH1{kYYVPaZjFJyvo(SQfTtzTkm!?iJd#H==)RG>3@= ztI^m>C5E62AD}XTe?g3FvpBu#Z&le~s8^xcT{Zn*zjt)4lYcQ9{&+_{cx~viKm51w zWq*jFUC_Ua+83D$iuyGf!nxiZVR~MRg-;tyH{IQkG0zF#)kz==VQ(IoaRvviQ~cR> zGQ}(mpkPtJ6Rc{r!VFs<7?4_Sh?k8twx*6bQ{TDa%(v5$J*qX`48s4XQvAfWvOA35{(HQuMO((Mrcdi1;=RbX97KO`<{0LqQUJ%` zUWDH#Q6c0MaG$Eh&GPOJP3}bkb!fuJV|&!N%d1LS5p0eq)p;4tmS;`EmkK&{(*o?W z>;q*wPaOFQb@L4Nk=wPujB+emT|W^2QzhpdOL!<1NUVN)JKv!bM5mTcFQd;_7k2tC0c;;7yC=OBEL_zV= zLV@?)ZH6hN=SMCWRa+G-oBLka{9YggeIlsKzbvfM-=)?zFZ)TawN+Km6njzme%f28owXJXcGNs_D6lZSr*l-B~z}Q(428@n28` z{-Q7*r2fjH|$TPn6+8YmTdY*|=32ln&HvLpzH{~a!nx`<{Q+9M!7g}CWlbP%jC8j;35gzIbw?aX;2#w3!wMA(iFxbiP#*yJ|GKp%0pcK3;D04sQ#ajD zAjW@(%Kv3kJQ!Ih|M!AC{mhm?1pru$002C||2vW-DgBJpQvZWWhgSZ&00Dqm0ssK* o|78Fpp8xCr4K`MFhnE0l@#Z^*{Z=^gs810K{>{f&c&j delta 6816 zcmV;R8eiqUR;W}BP)h>@6aWYa2mlMej*$%^f7{0O7XeVBsAYNEu@mpejzfB7SaFgA zVA+24Iz1wuAO`E3cpYAl>>;K*Z za2TXqkyO90-$%6qDM{RP%29J>v1pdEd$lQT_yBgW zYwmz(_f8de>m}VXa(JsrV(c1d(3?Fpe|iltU}tk$rkEQy3I(7D16b&b1l*S_D3+A|y%M{JLUU07q{y;nRF{7mC z`wDtdFF9=IED#}-U4U{9piHwpvw#vOYj52>2~alxnhSv1W<_jBmbf->9@QzfC=o(A z4^Ykrl<@hzf6#K*!kBE&ED<8K3jpmxK-;k@3KqX*%8pUU$d;v@ z+;7;<{3`c|#v-7x7-)2^o{olU77A{3Sy1gJQCR|1mI9To<3R5BfkuKlGk^Ynzc zV8m}6io8IjIa$(*`kAEIEiq?vK%1P@t*fw;d)bmI>cvsrvfIu`NNrw*p%?P;@m3^~ z?ez2jHHTrOG+2`{WG_tQ<|eoQ(7UAvI`_N<~q2RB&HQBMd5Ui)&RgQ>JCWk zdN)TnqL1m8UdrhrHESn%q&jH+XoX>|P}WyTGfH0YZ}*H_LgFxQ#N}z1t~q5(SG7Vx zNR7E)R*PaQz$KAD+}Pi+o6qR|2M34bgK8hJ*X_z4M;y|uaot%Xe+eBU)o`@?CIX+e z2}xX+NTLeFu;80hc6k!bxaCYy5PQ(B**&vq);X=$Wxf}gkC?T`d@sK-T83!{|DVbV z2VJ->SE==q*gc}clyIyvii-Ge&jmL&h!W;_p(agpH_U*3h9*^Kc5{|_ww~G4lt{S4 zo(00(=n7LHAtuo(e_GB431&!wcl{4bkefs{(cJC&ia-N(fuUWCyTu2*x8?P4mvE;)gNtW!yW<;x{s2+2q7})&qcT zK=T|?gfMtymf}@pPMs?W!u-%|IZpz|B?CX>B}`!Wj5=Qwf2Fo5!!|~Zg5jJ@4IJqo zmWTS1Z8nrH1^pnnCo+X}GX!z1kZ2>nv>oljqfOG(h%(woFARKvm=M|nvD?B9v3U^) zPv*C{pA*`Gb{C2*b0e)NvzfnsIys|ZqmC}otddb0w@;h?5d@Vk&}hNP84h_-TewI} zErHPn9Sa%+e`C^9v1Q6_B*E+>J`;(sm|6yoD*OA@u#{#PXjrq2&b>t@u7P)OV; z{1}!_w6UFly`5VC>jOIq+Ib!r+wDRp9GJ@a*m$=nf6b0G(`}P}1OvAluWRJl(q{lFdB-Dj`1tAR~t&DRH5FUU5=eRk}Vt-h65IVH#Zeam^4nZG*4M5Azc+11kvZY9z zOYBGle>@wcVJ$7EOKb@3>L~f`yZ?v%_7I}w9L#C6bnr+t>DjO#E`lgnoGd%B#7Jn< zuPZ~aFJLWqi69DW1i8IbOm|~KWf|Z`jVYa6$HH!RX7IaqYSc6fx>gE#MpFA_p!Sfi z7ey4z$4*P^7%I!c8UezA2^`SCKiANx@j};QO69;r@+x|1M48P&cZ7+9hZKhz!ZidLu z_Jjs$jdR@+)MKIq)|iGQ$pNkD z`Ebt1o-Rp3JG&*(x`c@O3uK`ZQlLzS-3mz3t|KP6ty5l8so65dCmeR01WBg?$&q!E zCx<+}Vz-OQro|V`JV3i`cmTH9@mgAEOhRBGc zmzyy|Z7=9!4zX0qvpZ0^&j4mpY`F32F9#hQJ+v^1DKT112g%eQ^qEpi>xfz~ZGa?( zwf8Iu;XGSP3hX(6sf8V`Z#^_)>ke9fPbhPwd=U9(&&5HW2hKt?9Em-j8-i!u>;+P) zYs788-vGGq`U)f6#^*+~PyL2r#5qkDgkekTv1SG9!+ymqs zUnW5!c{?(E7j}L5tSi}{vA&YoE2I{Yy^^rJ3Uzol44Gs{>s#SR9a6ogf0dl-dVDpq z^%`G~_kbRoBYJ!-lw$04fMIT=I^Ken4SPLy?(>??4^}EEyVVExYCh?L$0 zl$P|)e9F^eVK9fc*U%PA%ATQPS8RmnO02#a0lWnOES%GS72SV(68mV$3>MS+-C2TS_PUv z>4g6Wb@MJX^LGOir(HaA-2_XNA(uQ{YmdM!Yx#UnwH4lteI%9lprGGNv!SM~l+bLz zL_oKS?ji$wADMn&>hH$^K2Txm+sM>E7&di*eF(qa;ufNbDh}<#e@N>iKx^5u=~kp6 z&tDYzmVt!6XWzzQ0{2lQ@G((rT7If>kE#TJ@oGze`5eN0AA%g@42taIWLPf3PvG^P z5e}rzJcW4OO+);apOhe3z8~>?3K%;5!kJr0Ke}!3&>{P{thV-OMZP-LG4x0+_3OTe?wQziKY?(f8Wd&y@7ze22sf3aErHqY}P?O86>3YO8HwY?>`6oDbfnoi`=EhCF{g zkrt!=MP%Oq$+fTtAULMc{SZQleUm&YcKjAzeH)OiV3*9ofBxFw$>OL9PArsivccJ+ z6m_=WL6*M@EDI5T`aSMXeINNCFb`#T0lPwuB(d*96MUGY1mp)&TjxmsSSa@pjWPBR zI@TY8TvqO=VcI|fG_G5rS+l#Q=7CGquPcL1^*{vVQSe8osfRHPpPFhsnillZxHHic zUyD0-1yTJme@gLzz?VLPab~M$JxOOmFR`CcUiwqaX&%HTKcmco9M#Xm&Q)Z;piBWD z{9iy8bn<8kHj=%sQIr;?jB{*h;mf1<3>6Uv`4f3^DyrFMU%)DBzx4O{%(Pr&|B zk%0X(5YxY+V){3lC>pKYgbyBz_;NWxAsxEO0tHUI5@{?>Tb3x|A#FJsiEncAspFg6 zLh%hdrr=6$#XuE_K<5(GbSwhNZGnX4cD#N(8iD+09pIy7JUJxDT_BQF#7B2bnlQs4 z1{^dUe_N90kfY|%y0PnA>N>BYE2Z|}0ioOcXtxF6VC9A6U=jHu@`T(0%8Nm5lDq^P zE#-|)i#1w?mL)Hj+64J@5Wjo|7P#!{`l?iK?#3tF#`q1KfAR_(cqMo-(b?>4cNN}S zP4~70u3TP&1}LuutChxbjwG)`1)f=v_MA@&f9#2voV*^}Zh*F{*o~P?cDm2ZJayK# za?msjO|#H63r(}3rdiC3vax;eDjRj13FukGtZ%*>$tdZ;*%1>YLz6R=)-7kT%O+s0 zYhm=5KnC+tNOGzK!h5EeEcRun(NcUnYS&z+P$$Au*a}Mg`TDWeN88|mtrU{^c zbCXpVcQxDF$l_pRAa+9oov{w~7EXF{d45{Pof~<#m}pwPqXAf9M=$Te z0k&1RTGVep*(Rdc8?nHB_-#iOFD-fIeYWBYRYj(bZMKmV@ z$7uxd7tHh;Dw*lQwUv%DdMOuB>qXLfP0M+4ZNaxAW?>qIl}KTpd`*yIvv$HTiynkY zgm4`}sL{7oK=94GPTyvQaoT)3e>!-(Ow&=D)%amdfwR#Hhs&T;+K%A!ati0=amr9m z@C5cGYW#Y@v9^&@xm5?Qb#c533A9ju&D<@cCu5!~gv>PqI8`nYJgA1Unzs^NW2&?wcgjNbKW6JMEIPZfRLNFxx{RsDk1T5(v zypTVDBY%)a?yGa;$wE1@cq)G=7^qdIJ)Vd0_DA@N&_^RHLi`ioY?eO;J|HFEhc!^C zT$JRG6Ii7131Z9}f8vw4l({)Dt^08yGH25+mLz|QyDr@KkUvAN>+=7?=Co|%fZU6H z7QNW#sMP;F&hsz8z&&i=Y`n?lj>Il&q&MZnc*nG=r{%b_BY(;FeqYAu_!WqbJr_1I zYGkr}71jAQ5X<@+j<>i7L#zH**3vp=wQw(Zx*h7G+ z*(l}p6O#Nxl=zQmw(qKQwik_3Y`Q-jo{K*Y=Dx?sBe)%gEC23^KKUnnKK_&zGQ5sI z!|C#KT5I?Pf2}oO3*6a|AN6hUmsHC~Oz2lZIsWUgOeOg@ptN9E1oB%d$g%0~sNlw{ z-v>$BW05574?&Xl_;h8m{6~LpMgEh&$0z^U-zSm(g0%mNOFxTaOFww#!k6CPxL5pp z#47@Ze<1e{MMj0Y|BURp!Hs`aJ*^=Bn`(C;tTd4nf8G8{B35840u|WUP7Jq`d^IUa zDsa8q&7dZw1#>ec z-9+0XGMB@fM`e(Adp^QjK=2k)rGhPRmqJ{1slE=ldk({FqNtw#R%D-0J09 zG0Fv%u2R`?>P^z=KFWpMy<9{E0$yEA={OC=Dw1zSMr@CSZb@_S3`dYq+7zdfbIX%? zn3v)EiXwH)9T_lfXUsTJc?efg8_tjiyet{bBW1b^Ldwn{bb4I(`6;flE0jemyU~R9 ze^lFdvyJQBGa5=i*V^8Aew|*3R*NrK?J_Le@lPJ|{baYTvQJ723T}od2k;CNyMES= zA)ShlpCQ_7{3|*GXInheVV-h?s}y>|=lZXCDo_f8UlzZG7n1a4DYwNXaeK%lf9{~IT59)$8g z)!}6eqZoo6W#vTygcrvlkmxd+UY&i^R?VgUx!~`@7w7cD(&=*ft^OzC6zY^ zcKQ~i@>V>s=Ryg7-CE$9)|;e!~a#KxG~GO-}4vVKe(S68jFB*>|~_e|-7$`zcg#PJV999MpnAMrf=VFK;Z{Bhu=9*K(VC&7HFDNFt-SKiNfmi+S|Oa4V= zmW*pE%DtSxqxdS%gaP5*%1ubhFS!VR6*lW%qX>UPX8l`k*1tnazxPG>SfyG20c>=c zQJT;#!_i7PeUCTHf61tYKh7=uk3`Yy{inEv|Cw9(U&8JF$|3(PY~g=L$p0V{`X?9C zzqp0}8``Q(9(XlT&B9fITevDl)TK(57Op0J3s;+ownwDJho`1O7Ou7eJT;9HRoi?E zSMji?+Tnxhtgvvki;R*G&8e_JwHpuFS~_k)>v@c6k~){7e;;^gL7hjj3%kyzFiTVx zR0JqNT^NKUpSMN6J*$feq6cRQ?HUoGrBMOlLW)}Z7LmHlSCzWlw`cWqZqMo&751#+ zp-$z|@U8I6^y#_x`cZS&5XWdcT|!f8SI+8x2j(NL}3{Llc&Hy!!r;nguPZ zn;^&8cS6mddgvuRTp)D`>JE}MF?L}cj0x&RA$%9d@Kt{eAK@{CCr<-UA$Tgn+Zn*? zs{@{>?gDu6*YMTd^cp@F@tzP1{V^6!@sdAw-HUwen}(15#K!^dF>wh%Jw(f~m(JpH zZ0N0ce}6?*9YBA4n8rT>&Q8TMn`bxp+P*6T+N-Pa)znZ|T#KZil&QK+r{dXB^{5{* zhUpgvBL49bkfw^qMc4ngw#q_iE~UZn>N4CkTcr_%WB#6qdO7;@texmz&1?K=P!19jDP)Fpb7*pGN5_zoy`Y*Od2@ z33dHkLQ~TP@bCWtP)i30tfw$A^BDjD3ReICP)h>@6aWYa2mlMejjBrrLE)gDYw HVs!)n;W-Zz delta 64 zcmcc2eVLm#z?+#xgn@&DgF#_S-$vetjLblK^G8NeCNP7Og$pb)S&Y>jBrrLE)gDYw HVs!)nKFt!5 diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index be78cace730116d1e6d4b09e3c26842b18ece442..8697d473d1afb84d0892ce51bee2c8d73b83bc48 100644 GIT binary patch delta 64 zcmbQiJA;=uz?+#xgn@&DgTaV-#ztO4CT1YL*^$W$!sui1Vg!jyzRhY5rbXH8!E`vA FBLKC64vqi- delta 64 zcmbQiJA;=uz?+#xgn@&DgF#_S-$q_TCT1YL*^$W$!sui1Vg!jyzRhY5rbXH8!E`vA FBLEW?5)1$U diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 24df5fcd5..621a6e58b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java @@ -29,6 +29,8 @@ public class Logic2VampireLanguageMapperTrace { public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; + public Map definedElement2String = new HashMap(); + public final Map type2Predicate = new HashMap(); public final Map element2Predicate = new HashMap(); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 9deab87fd..855d7637b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java @@ -19,9 +19,11 @@ import com.google.common.base.Objects; import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; @@ -34,6 +36,7 @@ import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -58,6 +61,7 @@ public void transformContainment(final VampireSolverConfiguration config, final final ContainmentHierarchy hierarchy = hierarchies.get(0); final EList containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); final EList relationsList = hierarchy.getContainmentRelations(); + final ArrayList toRemove = CollectionLiterals.newArrayList(); for (final Relation l : relationsList) { { TypeReference _get = l.getParameters().get(1); @@ -71,14 +75,40 @@ public void transformContainment(final VampireSolverConfiguration config, final } } } - for (final Type c : containmentListCopy) { - boolean _isIsAbstract = c.isIsAbstract(); - if (_isIsAbstract) { - containmentListCopy.remove(c); + Type topTermVar = containmentListCopy.get(0); + for (final Relation l_1 : relationsList) { + { + TypeReference _get = l_1.getParameters().get(0); + Type _referred = ((ComplexTypeReference) _get).getReferred(); + Type pointingFrom = ((Type) _referred); + boolean _contains = containmentListCopy.contains(pointingFrom); + if (_contains) { + topTermVar = pointingFrom; + } + } + } + final String topName = CollectionsUtil.lookup(topTermVar, trace.type2Predicate).getConstant().toString(); + final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(topTermVar, trace.type2Predicate)); + boolean topLvlIsInInitModel = false; + String topLvlString = ""; + EList _subtypes = topTermVar.getSubtypes(); + for (final Type c : _subtypes) { + boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl"); + if (_equals) { + EList _elements = ((TypeDefinition) c).getElements(); + for (final DefinedElement d : _elements) { + boolean _containsKey = trace.definedElement2String.containsKey(d); + if (_containsKey) { + topLvlIsInInitModel = true; + topLvlString = CollectionsUtil.lookup(d, trace.definedElement2String); + } + } } } - final String topName = CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); - final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate)); + final boolean topInIM = topLvlIsInInitModel; + final String topStr = topLvlString; + InputOutput.print(Boolean.valueOf(topInIM)); + InputOutput.print(topStr); VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("containment_topLevel", topName)); @@ -96,7 +126,13 @@ public void transformContainment(final VampireSolverConfiguration config, final it_3.setLeft(this.support.duplicate(this.variable)); VLSConstant _createVLSConstant = this.factory.createVLSConstant(); final Procedure1 _function_4 = (VLSConstant it_4) -> { - it_4.setName("o1"); + String _xifexpression = null; + if (topInIM) { + _xifexpression = topStr; + } else { + _xifexpression = "o1"; + } + it_4.setName(_xifexpression); }; VLSConstant _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_4); it_3.setRight(_doubleArrow); @@ -130,16 +166,16 @@ public void transformContainment(final VampireSolverConfiguration config, final final VLSVariable varC = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_3); final ArrayList varList = CollectionLiterals.newArrayList(varB, varA); final Map> type2cont = new HashMap>(); - for (final Relation l_1 : relationsList) { + for (final Relation l_2 : relationsList) { { - final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList); - TypeReference _get = l_1.getParameters().get(1); + final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList); + TypeReference _get = l_2.getParameters().get(1); Type _referred = ((ComplexTypeReference) _get).getReferred(); final Type toType = ((Type) _referred); final VLSFunction toFunc = CollectionsUtil.lookup(toType, trace.type2Predicate); this.addToMap(type2cont, toFunc, rel); - EList _subtypes = toType.getSubtypes(); - for (final Type c_1 : _subtypes) { + EList _subtypes_1 = toType.getSubtypes(); + for (final Type c_1 : _subtypes_1) { this.addToMap(type2cont, toFunc, rel); } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); @@ -244,9 +280,9 @@ public void transformContainment(final VampireSolverConfiguration config, final variables.add(_doubleArrow); for (int j = 0; (j < i); j++) { { - for (final Relation l_2 : relationsList) { + for (final Relation l_3 : relationsList) { { - final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.newArrayList(variables.get(j), variables.get(((j + 1) % i)))); + final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.newArrayList(variables.get(j), variables.get(((j + 1) % i)))); disjunctionList.add(rel); } } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java index b9c1d28df..2d9d566d3 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java @@ -62,7 +62,13 @@ protected boolean transformTypes(final Collection types, final Collection< { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); + int _length = type.getName().split(" ").length; + boolean _equals = (_length == 3); + if (_equals) { + it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2])); + } else { + it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); + } EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); @@ -74,6 +80,7 @@ protected boolean transformTypes(final Collection types, final Collection< Iterable _filter = Iterables.filter(types, TypeDefinition.class); for (final TypeDefinition type_1 : _filter) { { + final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract()); final List orElems = CollectionLiterals.newArrayList(); EList _elements = type_1.getElements(); for (final DefinedElement e : _elements) { @@ -156,17 +163,26 @@ protected boolean transformTypes(final Collection types, final Collection< for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { { final int num = (i + 1); + final int index = (i - globalCounter); VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); final Procedure1 _function_2 = (VLSFunctionAsTerm it) -> { it.setFunctor(("eo" + Integer.valueOf(num))); }; final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); + if (isNotEnum) { + trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); + } final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); - final int index = (i - globalCounter); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_3 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString(), + String _xifexpression = null; + if (isNotEnum) { + _xifexpression = "definedType"; + } else { + _xifexpression = "enumScope"; + } + it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString(), type_1.getElements().get(index).getName().split(" ")[0])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml index c0c367a16..a2a573fc3 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml +++ b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml @@ -20,6 +20,117 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml index 0d17c01b5..f8fc4d59c 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml @@ -7,6 +7,11 @@ + + + + + @@ -14,6 +19,103 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -22,6 +124,115 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend index 3fc3d70f5..bbea9822b 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend @@ -81,8 +81,8 @@ class FAMTest { // add configuration things, in config file first it.documentationLevel = DocumentationLevel::FULL - it.typeScopes.minNewElements = 4 - it.typeScopes.maxNewElements = 5 + it.typeScopes.minNewElements = 24 + it.typeScopes.maxNewElements = 25 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax it.contCycleLevel = 5 diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 2cecdaac8ea5d92200fec7dd3d6ef38718cbc6ef..7e2c1f1282e5e02f457bf872bdaaba0d4d94ad52 100644 GIT binary patch delta 64 zcmX@8d{CJ;z?+#xgn@&DgJBQzjE%gmT+Bdvb12sz7BC}(e=Q@3F_}fs98B8@+Jor^ GK}P^cR}%#Q delta 64 zcmX@8d{CJ;z?+#xgn@&DgCTZX-$q_nE@mLTIh5-U3z!kYzm^fin9L$*4yNq{?ZI?| Gpd$cu;}pRF diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin index a34ab8462f14ee909cc1487789cba2ccd16ff772..9ac7c906684046148eb756337f7a98c2d6b3723f 100644 GIT binary patch delta 1093 zcmV-L1iJf}F`h9EP)h>@6aWYa2mo{nn6VA93x5sjrL=RG5Af><@EbD$LfFP*0JW*5 z0X$cSoPGqR(y$J-$W<<}Oao>BEu5>ePiVk5nE?#$x9Z@2o5A(ZmdSVIbX$I~7&)q! zj3W8244b#_L0#Q=?qasstkZ}T){7QJ9#&S%_WG}?YNp!_8}RM$mvtlGN1J|tM;$BT z$A1~Fag_2#^@nKd-Jz{N!lle_<)j3--6B86`21vMe0l}^wS}LCe*0OS-+msGjlTPZ zoEFJ1nX8cDR}3FM{kjguZ=x{BZxO-oW+K?d5d1zw@P|4Cf5i9uq6q$kqW%n`*3Z)J z{3T>>CV#Cp4#@U5Wc&LJHhzxqk0{$e<$sor{9fBOsbF0K0m;p2UckOi5MYr*$p;d?7YyK&DB_!HTk<=SFC8>YIPYe$$J4+5rLsG4@%^iCEB zeClFOz^7#a^yPKXSJXjY3D6Tg0rKYDDy&y~Vuq{^cE-6iurqG2?Tp!y7;KDlYeTYi zh-5w3nOQ`m$nP5>*>Txos6!`JOn(SvWaG>Tw}%593-jFu#JLf1K2*y108@4na|%9X z@TdxtA~UJE*$ngh$>6|&hB~Znxcf} zl-#Ks0I_g@#R?T*)B^ms(?jx`_!K4@Jqz3O}^$UOz+ay732`}=&XQxZ)RiHE%jD-$JhlIK9QcG8ijQz&e=B;zOqFP}K{1MH;YaMsp z+@GL+2ff!QHXVTK45@VusDI=B3zf3ZQqu&dlJOuLeIW>PdctsxF~c;x>83-M?A<@u zmq@#K8$b_4e!rnP?N%#1{-8ubr>hXrEptYck95`#@L1My=<0?PB>DNr+be7cPX3XlCtZnZ;?~Z(EC>H6^HJ!I=Y${{>J> z2MA)WH8~Xz002)d002-+0|XQR2nYxObPAZWRu9q!19S?Qvnv*@0S$Btm`-A@H8~Xz z002*u@6aWYa2mt!Nj#&?qW9Btj~y))r%HI9@bUM_WG}?YNp!_+wbl0m-QmwN0WYl2OTTohZ(MM zlz;Lz^@nKc-Jz*JLR0-lPD+5+E%IXw&rfECr&qvVTKH+`wx89x?dLJs=(}IYX_5Sr zxe6J6#qidzo*{VdJSUqbd~ z^4Dn4|AuUTpTWjY5&jWn`={K}k>6|ECV$ne*fux%L;i(L|G%NCt@e9oWNd zn3DtF<2+^(_7S-RZu&jj(@efqvE*DML?YJ& zs!lq4;YqvSwn~wV?O!-;qzy18i~{X8;d3onb4di#j9``~6RKC$+htAl-UZVl{<+iUw`wjc)E;@sMhY#kz54|Zl2 z(I)cShDdf?wixQrNfi@98QC^7!hh}I0LQ|7w*hf(M4S(mGCshRoy44iPZ>O@!lcMd zYHl{e{C+ZcFP8`dvk7R#Z0&6`ehtpzn*GJOIURI5u9({*G`F)`-ny13p*bbDt|`i$ zA~kOa&mEzs)}~|ky<(egmn+cNSstT570ONSG}sECJogy~GqtmRAX2$f9Dh$)Gpuyl zp|F`?zonGxM&VnfR1y%4+D4&aQzut)$ibD?n4oTA0>?v9a`qj1JWU3ZoAad6(eK6ueEvWoUW)=*aCkfd~+6u1887hn!_dDwf@6aWYa2mt!Njv nEd%<#j*}Z08v#j^Hy9%W`o4~nT^Jhy9+P<(9|p`900000)xzZ> diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin index a18fd1a51845cc3e22a45780ef85403476eab345..60e770c6508852193f763994c965aba04d54ef72 100644 GIT binary patch delta 64 zcmca*e9M?Oz?+#xgn@&DgJBQzjE%er0?a^qbAiAwHZUVsd@Uo0F _function = (VampireSolverConfiguration it) -> { it.documentationLevel = DocumentationLevel.FULL; - it.typeScopes.minNewElements = 4; - it.typeScopes.maxNewElements = 5; + it.typeScopes.minNewElements = 24; + it.typeScopes.maxNewElements = 25; int _size = typeMapMin.size(); boolean _notEquals = (_size != 0); if (_notEquals) { diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index c5ed4b9049268ffa40b36cfc926f9ff3fe08470b..1bcd0a44b7259d8211abdb0c2edf8d150fb8e60c 100644 GIT binary patch delta 64 zcmZowZ&l|F@MdNaVc_84VA#VvV>!MGhve_}KT(>hG{U^>!MGhve_}KT(>hG{U^