Implement Containment mapping (partially) and revisit enum mapping

author: ArenBabikian <aren.babikian@mail.mcgill.ca> 2019-03-14 03:45:46 -0400
committer: ArenBabikian <aren.babikian@mail.mcgill.ca> 2019-03-14 03:45:46 -0400
commit: 56df1f808fa2289c3e97d45d84bce8acc8937280 (patch)
tree: 8956a784e9bc76f5f05411e891da86776c10629d
parent: Implement type scope for specific types (diff)
download: VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.tar.gz
VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.tar.zst
VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.zip
23 files changed, 590 insertions, 143 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index 1dbc0055..b7ad8f3d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -47,6 +47,8 @@ class Logic2VampireLanguageMapper {
        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support;
        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(
                this)
+        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(
+                this)
        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
                this)
        @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
@@ -80,24 +82,26 @@ class Logic2VampireLanguageMapper {
                // SCOPE MAPPER
                scopeMapper.transformScope(config, trace)
-                trace.constantDefinitions = problem.collectConstantDefinitions
+                // RELATION MAPPER
                trace.relationDefinitions = problem.collectRelationDefinitions
                problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
+                
+                // CONTAINMENT MAPPER
+                containmentMapper.transformContainment(problem.containmentHierarchies, trace)
+                // CONSTANT MAPPER
                // only transforms definitions
+                trace.constantDefinitions = problem.collectConstantDefinitions
                // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)]
                problem.constants.filter(ConstantDefinition).forEach [
                        this.constantMapper.transformConstantDefinitionSpecification(it, trace)
                ]
-                // //////////////////
+                // ASSERTION MAPPER
-                // Transform Assertions
-                // //////////////////
                for (assertion : problem.assertions) {
                        transformAssertion(assertion, trace)
                }
+                // OUTPUT
                return new TracedOutput(specification, trace)
        }
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
new file mode 100644
index 00000000..0820f47d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -0,0 +1,123 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy
+import java.util.List
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
+class Logic2VampireLanguageMapper_ContainmentMapper {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val Logic2VampireLanguageMapper base
+        private val VLSVariable variable = createVLSVariable => [it.name = "A"]
+        public new(Logic2VampireLanguageMapper base) {
+                this.base = base
+        }
+        def public void transformContainment(List<ContainmentHierarchy> hierarchies,
+                Logic2VampireLanguageMapperTrace trace) {
+                // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST
+                // TEMP
+                val hierarchy = hierarchies.get(0)
+                val containmentListCopy = hierarchy.typesOrderedInHierarchy
+                val relationsList = hierarchy.containmentRelations
+                // STEP 1
+                // Find root element
+                for (l : relationsList) {
+                        var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
+                        containmentListCopy.remove(pointingTo)
+                        for (c : pointingTo.subtypes) {
+                                containmentListCopy.remove(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 contTop = createVLSFofFormula => [
+                        it.name = support.toIDMultiple("containment_topLevel", topName)
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                it.variables += support.duplicate(variable)
+                                it.operand = createVLSEquivalent => [
+                                        it.left = topTerm
+                                        it.right = createVLSEquality => [
+                                                it.left = support.duplicate(variable)
+                                                it.right = createVLSConstant => [
+                                                        it.name = "o1"
+                                                ]
+                                        ]
+                                ]
+                        ]
+//                      it.fofFormula = support.duplicate(
+//                              topTerm,
+//                              createVLSFunctionAsTerm => [
+//                                      it.functor = "o1"
+//                              ]
+//                      )
+                ]
+                trace.specification.formulas += contTop
+                // STEP 2
+                // for each edge, if the pointedTo element exists,the edge must exist also
+                val varA = createVLSVariable => [it.name = "A"]
+                val varB = createVLSVariable => [it.name = "B"]
+                val varList = newArrayList(varB, varA)
+                for (l : relationsList) {
+                        val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString
+                        val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
+                        val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type
+                        val relFormula = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("containment", relName)
+                                it.fofRole = "axiom"
+                                it.fofFormula = createVLSUniversalQuantifier => [
+                                        it.variables += support.duplicate(varA)
+                                        it.operand = createVLSImplies => [
+                                                it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)
+                                                it.right = createVLSExistentialQuantifier => [
+                                                        it.variables += support.duplicate(varB)
+                                                        it.operand = createVLSAnd => [
+                                                                it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB)
+                                                                it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate),
+                                                                        varList)
+                                                        ]
+                                                ]
+                                                createVLSEquality => [
+                                                        it.left = support.duplicate(variable)
+                                                        it.right = createVLSConstant => [
+                                                                it.name = "o1"
+                                                        ]
+                                                ]
+                                        ]
+                                ]
+                        ]
+                        trace.specification.formulas += relFormula
+                        var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
+                        containmentListCopy.remove(pointingTo)
+                        for (c : pointingTo.subtypes) {
+                                containmentListCopy.remove(c)
+                        }
+                }
+        // STEP 3
+        // Ensure that an objct only has 1 parent
+        // STEP 4
+        // Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
+        }
+}
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 5c5eaff3..548deda4 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
@@ -10,6 +10,8 @@ import java.util.Map
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 import java.util.HashMap
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import java.util.List
 class Logic2VampireLanguageMapper_ScopeMapper {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -24,7 +26,8 @@ class Logic2VampireLanguageMapper_ScopeMapper {
        def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
 //              TODO HANDLE ERRORS RELATED TO MAX > MIN
-//              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS
+//              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS
+//              TODO HANDLE 
 //              TODO NOT SPECIFIED MEANS =0 ?
                // 1. make a list of constants equaling the min number of specified objects
                val GLOBAL_MIN = config.typeScopes.minNewElements
@@ -34,18 +37,22 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                // Handling Minimum_General
                if (GLOBAL_MIN != 0) {
-                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param
+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)
+                        for(i : trace.uniqueInstances){
+                                localInstances.add(support.duplicate(i))
+                        }
+                        
                        makeFofFormula(localInstances, trace, true, null)
                }
                // Handling Maximum_General
                if (GLOBAL_MAX != 0) {
-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param
+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true)
-                        makeFofFormula(localInstances, trace, false, null)
+                        makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)
                }
                // Handling Minimum_Specific
-                var i = 0
+                var i = 1
                var minNum = -1
                var Map<Type, Integer> startPoints = new HashMap
                for (t : config.typeScopes.minNewElementsByType.keySet) {
@@ -106,13 +113,17 @@ class Logic2VampireLanguageMapper_ScopeMapper {
        def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum,
                Type type) {
                var nm = ""
-                var VLSFunction tm = null
+                var VLSTerm tm = null
                if (type === null) {
                        nm = "object"
                        tm = support.topLevelTypeFunc
                } else {
                        nm = type.lookup(trace.type2Predicate).constant.toString
-                        tm = support.duplicate(type.lookup(trace.type2Predicate))
+                        tm = createVLSAnd => [
+                                it.left = support.duplicate(type.lookup(trace.type2Predicate))
+                                it.right = support.topLevelTypeFunc
+                        ]
+//                      tm = support.duplicate(type.lookup(trace.type2Predicate))
                }
                val name = nm
                val term = tm
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index 021cb0ea..8d00d3e7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -37,11 +37,11 @@ class Logic2VampireLanguageMapper_Support {
        def protected VLSVariable duplicate(VLSVariable term) {
                return createVLSVariable => [it.name = term.name]
        }
-        
        def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) {
                return createVLSFunctionAsTerm => [it.functor = term.functor]
        }
-        
        def protected VLSConstant duplicate(VLSConstant term) {
                return createVLSConstant => [it.name = term.name]
        }
@@ -61,14 +61,23 @@ class Logic2VampireLanguageMapper_Support {
                        it.terms += duplicate(v)
                ]
        }
-        
+        def protected VLSFunction duplicate(VLSFunction term, List<VLSVariable> vars) {
+                return createVLSFunction => [
+                        it.constant = term.constant
+                        for (v : vars) {
+                                it.terms += duplicate(v)
+                        }
+                ]
+        }
        def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) {
                return createVLSFunction => [
                        it.constant = term.constant
                        it.terms += duplicate(v)
                ]
        }
-        
        def protected VLSConstant toConstant(VLSFunctionAsTerm term) {
                return createVLSConstant => [
                        it.name = term.functor
@@ -84,6 +93,13 @@ class Logic2VampireLanguageMapper_Support {
                ]
        }
        
+        def protected VLSFunction topLevelTypeFunc(VLSVariable v) {
+                return createVLSFunction => [
+                        it.constant = "object"
+                        it.terms += duplicate(v)
+                ]
+        }
        def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) {
                return createVLSFunction => [
                        it.constant = "object"
@@ -173,14 +189,16 @@ class Logic2VampireLanguageMapper_Support {
         */
        // QUANTIFIERS + VARIABLES
        def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper,
-                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, boolean isUniversal) {
+                QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables,
+                boolean isUniversal) {
                val variableMap = expression.quantifiedVariables.toInvertedMap [ v |
                        createVLSVariable => [it.name = toIDMultiple("V", v.name)]
                ]
                val typedefs = new ArrayList<VLSTerm>
                for (variable : expression.quantifiedVariables) {
-                        val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap))
+                        val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate),
+                                variable.lookup(variableMap))
                        typedefs.add(eq)
                }
                if (isUniversal) {
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 e12180fa..4c4247ce 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
@@ -1,12 +1,12 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
 import java.util.ArrayList
@@ -14,7 +14,6 @@ import java.util.Collection
 import java.util.List
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
-import java.util.Collections
 class Logic2VampireLanguageMapper_TypeMapper {
        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -28,10 +27,8 @@ class Logic2VampireLanguageMapper_TypeMapper {
        def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements,
                Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
-//              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
-//              trace.typeMapperTrace = typeTrace
                val VLSVariable variable = createVLSVariable => [it.name = "A"]
+                var globalCounter = 0
                // 1. Each type (class) is a predicate with a single variable as input
                for (type : types) {
@@ -39,94 +36,109 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
                                it.terms += support.duplicate(variable)
                        ]
-//                      typeTrace.type2Predicate.put(type, typePred)
                        trace.type2Predicate.put(type, typePred)
                }
                // 2. Map each ENUM type definition to fof formula
                for (type : types.filter(TypeDefinition)) {
+                        // Create a VLSFunction for each Enum Element
                        val List<VLSFunction> orElems = newArrayList
                        for (e : type.elements) {
                                val enumElemPred = createVLSFunction => [
                                        val splitName = e.name.split(" ")
-                                        if( splitName.length > 2) {
+                                        if (splitName.length > 2) {
                                                it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
-                                        }
+                                        } else {
-                                        else {
                                                it.constant = support.toIDMultiple("e", splitName.get(0))
                                        }
                                        it.terms += support.duplicate(variable)
                                ]
-//                              typeTrace.element2Predicate.put(e, enumElemPred)
                                trace.element2Predicate.put(e, enumElemPred)
-                                orElems.add(enumElemPred)
                        }
+                        // Similar to InheritanceHierarchy for the Enum
+                        val List<VLSTerm> possibleNots = newArrayList
+                        val List<VLSTerm> typeDefs = newArrayList
+                        for (t1 : type.elements) {
+                                for (t2 : type.elements) {
+                                        if (t1 == t2) {
+                                                val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable)
+                                                possibleNots.add(fct)
+                                        } else {
+                                                val op = support.duplicate(t2.lookup(trace.element2Predicate), variable)
+                                                val negFct = createVLSUnaryNegation => [
+                                                        it.operand = op
+                                                ]
+                                                possibleNots.add(negFct)
+                                        }
+                                }
+                                typeDefs.add(support.unfoldAnd(possibleNots))
+                                possibleNots.clear
+                        }
+                        // Implement Enum Inheritence Hierarchy
                        val res = createVLSFofFormula => [
                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
-                                // below is temporary solution
                                it.fofRole = "axiom"
                                it.fofFormula = createVLSUniversalQuantifier => [
                                        it.variables += support.duplicate(variable)
                                        it.operand = createVLSEquivalent => [
                                                it.left = type.lookup(trace.type2Predicate)
-                                                it.right = support.unfoldOr(orElems)
+                                                it.right = createVLSAnd => [
+                                                        it.left = support.topLevelTypeFunc(variable)
+                                                        it.right = support.unfoldOr(typeDefs)
+                                                ]
+//                                              it.right = support.unfoldOr((typeDefs))
                                        ]
                                ]
                        ]
                        trace.specification.formulas += res
-                        // Create objects for the enum elements
+                        for (var i = globalCounter; i < globalCounter+type.elements.length; i++) {
-                        val List<VLSTerm> enumScopeElems = newArrayList
+                                // Create objects for the enum elements
-                        for (var i = 0; i < type.elements.length; i++) {
                                val num = i + 1
                                val cstTerm = createVLSFunctionAsTerm => [
                                        it.functor = "eo" + num
                                ]
                                val cst = support.toConstant(cstTerm)
                                trace.uniqueInstances.add(cst)
-                                val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm)
-                                enumScopeElems.add(fct)
+                                val index = i
-                                
+                                val enumScope = createVLSFofFormula => [
-                                //For paradox Only
+                                        it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0),
-                                for (var j = 0; j < type.elements.length; j++) {
+                                                type.elements.get(index).name.split(" ").get(0))
-                                        if(j != i) {
+                                        it.fofRole = "axiom"
-                                                val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm)
+                                        it.fofFormula = createVLSUniversalQuantifier => [
-                                                val negFct = createVLSUnaryNegation => [
+                                                it.variables += support.duplicate(variable)
-                                                        it.operand = op
+                                                it.operand = createVLSEquivalent => [
+                                                        it.left = createVLSEquality => [
+                                                                it.left = support.duplicate(variable)
+                                                                it.right = support.duplicate(support.toConstant(cstTerm))
+                                                        ]
+                                                        it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate),
+                                                                variable)
                                                ]
-                                                enumScopeElems.add(negFct)
+                                        ]
-                                        }
+                                ]
-                                }
-                                //End Paradox
+                                trace.specification.formulas += enumScope
-//                              enumScopeElems.add(support.topLevelTypeFunc(cstTerm))
                        }
-                        
+                        globalCounter+=type.elements.size
-                        
-                        
-                        val enumScope = createVLSFofFormula => [
-                                it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0))
-                                // below is temporary solution
-                                it.fofRole = "axiom"                    
-                                it.fofFormula = support.unfoldAnd(enumScopeElems)
-                        ]
-                        
-                        trace.specification.formulas += enumScope
                }
                // HIERARCHY HANDLER
                // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
                // and store in a map
-//              println(types.filter[!isIsAbstract])
+                for (t1 : types.filter[!isIsAbstract]) {
-                for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) {
                        for (t2 : types) {
                                // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
                                if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
-//                                      typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
                                        trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
                                } else {
-//                                      typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
                                        trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
                                                it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
                                        ])
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 052e0175..8e50f399 100644
--- 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
Binary files differ
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 1296bf9e..99ba52b8 100644
--- 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
Binary files differ
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 fd625384..7b01a284 100644
--- 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
Binary files differ
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
new file mode 100644
index 00000000..9f455fdd
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
Binary files differ
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 978571d2..0b91349d 100644
--- 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
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index b98f0332..07e249ce 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
Binary files differ
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 8238a89e..115249ba 100644
--- 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
Binary files differ
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 f64a218b..2e86d0c7 100644
--- 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
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
index ec8107e8..8a9aa4bb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
@@ -38,3 +38,5 @@
 /.VampireSolutionModel.java._trace
 /.VampireCallerWithTimeout.java._trace
 /.Logic2VampireLanguageMapper_ScopeMapper.java._trace
+/.Logic2VampireLanguageMapper_Containment.java._trace
+/.Logic2VampireLanguageMapper_ContainmentMapper.java._trace
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index afe77bbe..36a727b2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper;
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
@@ -83,6 +84,9 @@ public class Logic2VampireLanguageMapper {
  private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this);
  
  @Accessors(AccessorType.PUBLIC_GETTER)
+  private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this);
+  
+  @Accessors(AccessorType.PUBLIC_GETTER)
  private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this);
  
  @Accessors(AccessorType.PUBLIC_GETTER)
@@ -114,12 +118,13 @@ public class Logic2VampireLanguageMapper {
      this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);
    }
    this.scopeMapper.transformScope(config, trace);
-    trace.constantDefinitions = this.collectConstantDefinitions(problem);
    trace.relationDefinitions = this.collectRelationDefinitions(problem);
    final Consumer<Relation> _function_3 = (Relation it) -> {
      this.relationMapper.transformRelation(it, trace);
    };
    problem.getRelations().forEach(_function_3);
+    this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace);
+    trace.constantDefinitions = this.collectConstantDefinitions(problem);
    final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {
      this.constantMapper.transformConstantDefinitionSpecification(it, trace);
    };
@@ -428,6 +433,11 @@ public class Logic2VampireLanguageMapper {
  }
  
  @Pure
+  public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() {
+    return this.containmentMapper;
+  }
+  
+  @Pure
  public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() {
    return this.relationMapper;
  }
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
new file mode 100644
index 00000000..da0e5615
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -0,0 +1,180 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
+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.TypeReference;
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;
+import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
+import java.util.ArrayList;
+import java.util.List;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.Extension;
+import org.eclipse.xtext.xbase.lib.ObjectExtensions;
+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
+@SuppressWarnings("all")
+public class Logic2VampireLanguageMapper_ContainmentMapper {
+  @Extension
+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
+  
+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
+  
+  private final Logic2VampireLanguageMapper base;
+  
+  private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> {
+    it.setName("A");
+  }));
+  
+  public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) {
+    this.base = base;
+  }
+  
+  public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) {
+    final ContainmentHierarchy hierarchy = hierarchies.get(0);
+    final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy();
+    final EList<Relation> relationsList = hierarchy.getContainmentRelations();
+    for (final Relation l : relationsList) {
+      {
+        TypeReference _get = l.getParameters().get(1);
+        Type _referred = ((ComplexTypeReference) _get).getReferred();
+        Type pointingTo = ((Type) _referred);
+        containmentListCopy.remove(pointingTo);
+        EList<Type> _subtypes = pointingTo.getSubtypes();
+        for (final Type c : _subtypes) {
+          containmentListCopy.remove(c);
+        }
+      }
+    }
+    final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString();
+    final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate));
+    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
+    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
+      it.setName(this.support.toIDMultiple("containment_topLevel", topName));
+      it.setFofRole("axiom");
+      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
+      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
+        EList<VLSVariable> _variables = it_1.getVariables();
+        VLSVariable _duplicate = this.support.duplicate(this.variable);
+        _variables.add(_duplicate);
+        VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
+        final Procedure1<VLSEquivalent> _function_2 = (VLSEquivalent it_2) -> {
+          it_2.setLeft(topTerm);
+          VLSEquality _createVLSEquality = this.factory.createVLSEquality();
+          final Procedure1<VLSEquality> _function_3 = (VLSEquality it_3) -> {
+            it_3.setLeft(this.support.duplicate(this.variable));
+            VLSConstant _createVLSConstant = this.factory.createVLSConstant();
+            final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> {
+              it_4.setName("o1");
+            };
+            VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4);
+            it_3.setRight(_doubleArrow);
+          };
+          VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3);
+          it_2.setRight(_doubleArrow);
+        };
+        VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_2);
+        it_1.setOperand(_doubleArrow);
+      };
+      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
+      it.setFofFormula(_doubleArrow);
+    };
+    final VLSFofFormula contTop = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
+    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
+    _formulas.add(contTop);
+    VLSVariable _createVLSVariable = this.factory.createVLSVariable();
+    final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> {
+      it.setName("A");
+    };
+    final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);
+    VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
+    final Procedure1<VLSVariable> _function_2 = (VLSVariable it) -> {
+      it.setName("B");
+    };
+    final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);
+    final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA);
+    for (final Relation l_1 : relationsList) {
+      {
+        final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString();
+        TypeReference _get = l_1.getParameters().get(0);
+        Type _referred = ((ComplexTypeReference) _get).getReferred();
+        final Type fromType = ((Type) _referred);
+        TypeReference _get_1 = l_1.getParameters().get(1);
+        Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred();
+        final Type toType = ((Type) _referred_1);
+        VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
+        final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> {
+          it.setName(this.support.toIDMultiple("containment", relName));
+          it.setFofRole("axiom");
+          VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
+          final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> {
+            EList<VLSVariable> _variables = it_1.getVariables();
+            VLSVariable _duplicate = this.support.duplicate(varA);
+            _variables.add(_duplicate);
+            VLSImplies _createVLSImplies = this.factory.createVLSImplies();
+            final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> {
+              it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA));
+              VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
+              final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> {
+                EList<VLSVariable> _variables_1 = it_3.getVariables();
+                VLSVariable _duplicate_1 = this.support.duplicate(varB);
+                _variables_1.add(_duplicate_1);
+                VLSAnd _createVLSAnd = this.factory.createVLSAnd();
+                final Procedure1<VLSAnd> _function_7 = (VLSAnd it_4) -> {
+                  it_4.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(fromType, trace.type2Predicate), varB));
+                  it_4.setRight(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList));
+                };
+                VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_7);
+                it_3.setOperand(_doubleArrow);
+              };
+              VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6);
+              it_2.setRight(_doubleArrow);
+              VLSEquality _createVLSEquality = this.factory.createVLSEquality();
+              final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {
+                it_3.setLeft(this.support.duplicate(this.variable));
+                VLSConstant _createVLSConstant = this.factory.createVLSConstant();
+                final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> {
+                  it_4.setName("o1");
+                };
+                VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8);
+                it_3.setRight(_doubleArrow_1);
+              };
+              ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);
+            };
+            VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5);
+            it_1.setOperand(_doubleArrow);
+          };
+          VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4);
+          it.setFofFormula(_doubleArrow);
+        };
+        final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3);
+        EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
+        _formulas_1.add(relFormula);
+        TypeReference _get_2 = l_1.getParameters().get(1);
+        Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred();
+        Type pointingTo = ((Type) _referred_2);
+        containmentListCopy.remove(pointingTo);
+        EList<Type> _subtypes = pointingTo.getSubtypes();
+        for (final Type c : _subtypes) {
+          containmentListCopy.remove(c);
+        }
+      }
+    }
+  }
+}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index 1950cad0..d2a6bff2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
@@ -48,16 +49,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
  public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
    final int GLOBAL_MIN = config.typeScopes.minNewElements;
    final int GLOBAL_MAX = config.typeScopes.maxNewElements;
-    final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList();
+    final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();
    if ((GLOBAL_MIN != 0)) {
      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false);
+      for (final VLSConstant i : trace.uniqueInstances) {
+        localInstances.add(this.support.duplicate(i));
+      }
      this.makeFofFormula(localInstances, trace, true, null);
    }
    if ((GLOBAL_MAX != 0)) {
      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true);
-      this.makeFofFormula(localInstances, trace, false, null);
+      this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);
    }
-    int i = 0;
+    int i_1 = 1;
    int minNum = (-1);
    Map<Type, Integer> startPoints = new HashMap<Type, Integer>();
    Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet();
@@ -65,10 +69,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
      {
        minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue();
        if ((minNum != 0)) {
-          this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false);
+          this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false);
-          startPoints.put(t, Integer.valueOf(i));
+          startPoints.put(t, Integer.valueOf(i_1));
-          int _i = i;
+          int _i = i_1;
-          i = (_i + minNum);
+          i_1 = (_i + minNum);
          this.makeFofFormula(localInstances, trace, true, t);
        }
      }
@@ -83,8 +87,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
          this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false);
        }
        if (((maxNum).intValue() != minNum)) {
-          int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum));
+          int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum));
-          this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false);
+          this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false);
          this.makeFofFormula(localInstances, trace, false, t_1);
        }
      }
@@ -126,18 +130,24 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
  
  protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) {
    String nm = "";
-    VLSFunction tm = null;
+    VLSTerm tm = null;
    if ((type == null)) {
      nm = "object";
      tm = this.support.topLevelTypeFunc();
    } else {
      nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString();
-      tm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate));
+      VLSAnd _createVLSAnd = this.factory.createVLSAnd();
+      final Procedure1<VLSAnd> _function = (VLSAnd it) -> {
+        it.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate)));
+        it.setRight(this.support.topLevelTypeFunc());
+      };
+      VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);
+      tm = _doubleArrow;
    }
    final String name = nm;
-    final VLSFunction term = tm;
+    final VLSTerm term = tm;
    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
+    final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
      String _xifexpression = null;
      if (minimum) {
        _xifexpression = "min";
@@ -147,53 +157,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
      it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name));
      it.setFofRole("axiom");
      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
+      final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
        EList<VLSVariable> _variables = it_1.getVariables();
        VLSVariable _duplicate = this.support.duplicate(this.variable);
        _variables.add(_duplicate);
        VLSImplies _createVLSImplies = this.factory.createVLSImplies();
-        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
+        final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
          if (minimum) {
-            final Function1<VLSTerm, VLSEquality> _function_3 = (VLSTerm i) -> {
+            final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> {
              VLSEquality _createVLSEquality = this.factory.createVLSEquality();
-              final Procedure1<VLSEquality> _function_4 = (VLSEquality it_3) -> {
+              final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {
                VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-                final Procedure1<VLSVariable> _function_5 = (VLSVariable it_4) -> {
+                final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {
                  it_4.setName(this.variable.getName());
                };
-                VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_5);
+                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);
-                it_3.setLeft(_doubleArrow);
+                it_3.setLeft(_doubleArrow_1);
                it_3.setRight(i);
              };
-              return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4);
+              return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);
            };
-            it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3)));
+            it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4)));
            it_2.setRight(term);
          } else {
            it_2.setLeft(term);
-            final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> {
+            final Function1<VLSTerm, VLSEquality> _function_5 = (VLSTerm i) -> {
              VLSEquality _createVLSEquality = this.factory.createVLSEquality();
-              final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {
+              final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> {
                VLSVariable _createVLSVariable = this.factory.createVLSVariable();
-                final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {
+                final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> {
                  it_4.setName(this.variable.getName());
                };
-                VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);
+                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_7);
-                it_3.setLeft(_doubleArrow);
+                it_3.setLeft(_doubleArrow_1);
                it_3.setRight(i);
              };
-              return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);
+              return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6);
            };
-            it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4)));
+            it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_5)));
          }
        };
-        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
+        VLSImplies _doubleArrow_1 = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);
-        it_1.setOperand(_doubleArrow);
+        it_1.setOperand(_doubleArrow_1);
      };
-      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
+      VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
-      it.setFofFormula(_doubleArrow);
+      it.setFofFormula(_doubleArrow_1);
    };
-    final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
+    final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
    _formulas.add(cstDec);
  }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index e2ff7a0e..119d01f1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -104,6 +104,19 @@ public class Logic2VampireLanguageMapper_Support {
    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
  }
  
+  protected VLSFunction duplicate(final VLSFunction term, final List<VLSVariable> vars) {
+    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
+      it.setConstant(term.getConstant());
+      for (final VLSVariable v : vars) {
+        EList<VLSTerm> _terms = it.getTerms();
+        VLSVariable _duplicate = this.duplicate(v);
+        _terms.add(_duplicate);
+      }
+    };
+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
+  }
+  
  protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) {
    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
@@ -138,6 +151,17 @@ public class Logic2VampireLanguageMapper_Support {
    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
  }
  
+  protected VLSFunction topLevelTypeFunc(final VLSVariable v) {
+    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
+    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
+      it.setConstant("object");
+      EList<VLSTerm> _terms = it.getTerms();
+      VLSVariable _duplicate = this.duplicate(v);
+      _terms.add(_duplicate);
+    };
+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
+  }
+  
  protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) {
    VLSFunction _createVLSFunction = this.factory.createVLSFunction();
    final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
@@ -284,7 +308,8 @@ public class Logic2VampireLanguageMapper_Support {
      for (final Variable variable : _quantifiedVariables) {
        {
          TypeReference _range = variable.getRange();
-          final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap));
+          final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), 
+            CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap));
          typedefs.add(eq);
        }
      }
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 b8d74f36..ec759ebf 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
@@ -3,8 +3,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
@@ -18,7 +20,6 @@ import com.google.common.base.Objects;
 import com.google.common.collect.Iterables;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
@@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
        it.setName("A");
      };
      final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
+      int globalCounter = 0;
      for (final Type type : types) {
        {
          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
@@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper {
              };
              final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
              trace.element2Predicate.put(e, enumElemPred);
-              orElems.add(enumElemPred);
+            }
+          }
+          final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList();
+          final List<VLSTerm> typeDefs = CollectionLiterals.<VLSTerm>newArrayList();
+          EList<DefinedElement> _elements_1 = type_1.getElements();
+          for (final DefinedElement t1 : _elements_1) {
+            {
+              EList<DefinedElement> _elements_2 = type_1.getElements();
+              for (final DefinedElement t2 : _elements_2) {
+                boolean _equals = Objects.equal(t1, t2);
+                if (_equals) {
+                  final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);
+                  possibleNots.add(fct);
+                } else {
+                  final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);
+                  VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
+                  final Procedure1<VLSUnaryNegation> _function_1 = (VLSUnaryNegation it) -> {
+                    it.setOperand(op);
+                  };
+                  final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1);
+                  possibleNots.add(negFct);
+                }
+              }
+              typeDefs.add(this.support.unfoldAnd(possibleNots));
+              possibleNots.clear();
            }
          }
          VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
@@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper {
              VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
              final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {
                it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));
-                it_2.setRight(this.support.unfoldOr(orElems));
+                VLSAnd _createVLSAnd = this.factory.createVLSAnd();
+                final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> {
+                  it_3.setLeft(this.support.topLevelTypeFunc(variable));
+                  it_3.setRight(this.support.unfoldOr(typeDefs));
+                };
+                VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4);
+                it_2.setRight(_doubleArrow);
              };
              VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);
              it_1.setOperand(_doubleArrow);
@@ -118,8 +150,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
          final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
          EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
          _formulas.add(res);
-          final List<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList();
+          for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) {
-          for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) {
            {
              final int num = (i + 1);
              VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
@@ -129,38 +160,50 @@ public class Logic2VampireLanguageMapper_TypeMapper {
              final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);
              final VLSConstant cst = this.support.toConstant(cstTerm);
              trace.uniqueInstances.add(cst);
-              final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm);
+              final int index = i;
-              enumScopeElems.add(fct);
+              VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
-              for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) {
+              final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> {
-                if ((j != i)) {
+                it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], 
-                  final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm);
+                  type_1.getElements().get(index).getName().split(" ")[0]));
-                  VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
+                it.setFofRole("axiom");
-                  final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
+                VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-                    it.setOperand(op);
+                final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> {
+                  EList<VLSVariable> _variables = it_1.getVariables();
+                  VLSVariable _duplicate = this.support.duplicate(variable);
+                  _variables.add(_duplicate);
+                  VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
+                  final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> {
+                    VLSEquality _createVLSEquality = this.factory.createVLSEquality();
+                    final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> {
+                      it_3.setLeft(this.support.duplicate(variable));
+                      it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm)));
+                    };
+                    VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6);
+                    it_2.setLeft(_doubleArrow);
+                    it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable));
                  };
-                  final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
+                  VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5);
-                  enumScopeElems.add(negFct);
+                  it_1.setOperand(_doubleArrow);
-                }
+                };
-              }
+                VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4);
+                it.setFofFormula(_doubleArrow);
+              };
+              final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3);
+              EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
+              _formulas_1.add(enumScope);
            }
          }
-          VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
+          int _globalCounter = globalCounter;
-          final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
+          int _size = type_1.getElements().size();
-            it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0]));
+          globalCounter = (_globalCounter + _size);
-            it.setFofRole("axiom");
-            it.setFofFormula(this.support.unfoldAnd(enumScopeElems));
-          };
-          final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);
-          EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
-          _formulas_1.add(enumScope);
        }
      }
      final Function1<Type, Boolean> _function_1 = (Type it) -> {
        boolean _isIsAbstract = it.isIsAbstract();
        return Boolean.valueOf((!_isIsAbstract));
      };
-      Iterable<TypeDeclaration> _filter_1 = Iterables.<TypeDeclaration>filter(IterableExtensions.<Type>filter(types, _function_1), TypeDeclaration.class);
+      Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);
-      for (final TypeDeclaration t1 : _filter_1) {
+      for (final Type t1 : _filter_1) {
        {
          for (final Type t2 : types) {
            if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
index 265e7762..3109ccc2 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp
@@ -1,14 +1,16 @@
 % This is an initial Test Comment
-fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( e_Root_FunctionType ( A ) | ( e_Intermediate_FunctionType ( A ) | e_Leaf_FunctionType ( A ) ) ) ) ) .
+fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( object ( A ) & ( ( e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ( ~ e_Root_FunctionType ( A ) & ( e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ~ e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & e_Leaf_FunctionType ( A ) ) ) ) ) ) ) ) .
-fof ( enumScope_FunctionType , axiom , e_Root_FunctionType ( eo1 ) & ( ~ e_Intermediate_FunctionType ( eo1 ) & ( ~ e_Leaf_FunctionType ( eo1 ) & ( e_Intermediate_FunctionType ( eo2 ) & ( ~ e_Root_FunctionType ( eo2 ) & ( ~ e_Leaf_FunctionType ( eo2 ) & ( e_Leaf_FunctionType ( eo3 ) & ( ~ e_Root_FunctionType ( eo3 ) & ~ e_Intermediate_FunctionType ( eo3 ) ) ) ) ) ) ) ) ) .
+fof ( enumScope_FunctionType_Root , axiom , ! [ A ] : ( A = eo1 <=> e_Root_FunctionType ( A ) ) ) .
-fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_InformationLink ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
+fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) .
-fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | A = o6 ) ) ) ) ) => object ( A ) ) ) .
+fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) .
-fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) ) ) ) ) .
+fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
-fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( A = o1 => t_FunctionalOutput ( A ) ) ) .
+fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) ) ) => object ( A ) ) ) .
-fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( ( A = o2 | ( A = o3 | A = o4 ) ) => t_Function ( A ) ) ) .
+fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) ) ) ) ) ) ) ) .
-fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o5 | A = o6 ) => t_FunctionalInterface ( A ) ) ) .
+fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o2 | A = o3 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) .
-fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( t_FunctionalOutput ( A ) => ( A = o1 | ( A = o7 | A = o8 ) ) ) ) .
+fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o4 => ( t_Function ( A ) & object ( A ) ) ) ) .
-fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( t_Function ( A ) => ( A = o2 | ( A = o3 | ( A = o4 | ( A = o7 | A = o8 ) ) ) ) ) ) .
+fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o5 | ( A = o6 | A = o7 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) .
+fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => ( A = o4 | A = o8 ) ) ) .
+fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) .
 fof ( typeUniqueness , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo2 != eo3 & ( eo1 != o1 & ( eo2 != o1 & ( eo3 != o1 & ( eo1 != o2 & ( eo2 != o2 & ( eo3 != o2 & ( o1 != o2 & ( eo1 != o3 & ( eo2 != o3 & ( eo3 != o3 & ( o1 != o3 & ( o2 != o3 & ( eo1 != o4 & ( eo2 != o4 & ( eo3 != o4 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( eo1 != o5 & ( eo2 != o5 & ( eo3 != o5 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & ( o4 != o5 & ( eo1 != o6 & ( eo2 != o6 & ( eo3 != o6 & ( o1 != o6 & ( o2 != o6 & ( o3 != o6 & ( o4 != o6 & ( o5 != o6 & ( eo1 != o7 & ( eo2 != o7 & ( eo3 != o7 & ( o1 != o7 & ( o2 != o7 & ( o3 != o7 & ( o4 != o7 & ( o5 != o7 & ( o6 != o7 & ( eo1 != o8 & ( eo2 != o8 & ( eo3 != o8 & ( o1 != o8 & ( o2 != o8 & ( o3 != o8 & ( o4 != o8 & ( o5 != o8 & ( o6 != o8 & o7 != o8 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
 fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
 fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) .
@@ -25,6 +27,13 @@ fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_
 fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) .
 fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) .
 fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) .
+fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) .
+fof ( containment_r_interface_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : ( t_FunctionalElement ( B ) & r_interface_FunctionalElement ( B , A ) ) ) ) .
+fof ( containment_r_rootElements_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( t_FunctionalArchitectureModel ( B ) & r_rootElements_FunctionalArchitectureModel ( B , A ) ) ) ) .
+fof ( containment_r_subElements_Function , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( t_Function ( B ) & r_subElements_Function ( B , A ) ) ) ) .
+fof ( containment_r_data_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : ( t_FunctionalInterface ( B ) & r_data_FunctionalInterface ( B , A ) ) ) ) .
+fof ( containment_r_outgoingLinks_FunctionalOutput , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : ( t_FunctionalOutput ( B ) & r_outgoingLinks_FunctionalOutput ( B , A ) ) ) ) .
+fof ( containment_r_terminator_FunctionalData , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : ( t_FunctionalData ( B ) & r_terminator_FunctionalData ( B , A ) ) ) ) .
 fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalElement ( V_src , V_trg_1 ) & r_interface_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
 fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ V_src ] : ( t_FunctionalElement ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalArchitectureModel ( V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_1 ) ) ) ) .
 fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalArchitectureModel ( V_trg_1 ) & t_FunctionalArchitectureModel ( V_trg_2 ) ) ) => ( ( r_model_FunctionalElement ( V_src , V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) .
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
index b67a867a..86c9092a 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
@@ -65,13 +65,13 @@ class GeneralTest {
                // Minimum Scope
                typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, 
                        list2MapMin.get(Function.simpleName)
-                ), 3)
+                ), 1)
                typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, 
                        list2MapMin.get(functionalarchitecture.FunctionalInterface.simpleName)
                ), 2)
                typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, 
                        list2MapMin.get(FunctionalOutput.simpleName)
-                ), 1)
+                ), 3)
                // Maximum Scope
                typeMapMax.put(ecore2Logic.TypeofEClass(
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index ff2a8e18..ce6042ea 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
index 7d3be50d..13a0e74a 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
@@ -85,13 +85,13 @@ public class GeneralTest {
        final Map<String, EClass> list2MapMax = IterableExtensions.<String, EClass>toMap(metamodel.getClasses(), _function_1);
        typeMapMin.put(
          ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), 
-            list2MapMin.get(Function.class.getSimpleName())), Integer.valueOf(3));
+            list2MapMin.get(Function.class.getSimpleName())), Integer.valueOf(1));
        typeMapMin.put(
          ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), 
            list2MapMin.get(functionalarchitecture.FunctionalInterface.class.getSimpleName())), Integer.valueOf(2));
        typeMapMin.put(
          ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), 
-            list2MapMin.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(1));
+            list2MapMin.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(3));
        typeMapMax.put(
          ecore2Logic.TypeofEClass(
            modelGenerationProblem.getTrace(),
author	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-03-14 03:45:46 -0400
committer	ArenBabikian <aren.babikian@mail.mcgill.ca>	2019-03-14 03:45:46 -0400
commit	56df1f808fa2289c3e97d45d84bce8acc8937280 (patch)
tree	8956a784e9bc76f5f05411e891da86776c10629d
parent	Implement type scope for specific types (diff)
download	VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.tar.gz VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.tar.zst VIATRA-Generator-56df1f808fa2289c3e97d45d84bce8acc8937280.zip