VAMPIRE: add to #40. I am tired

35 files changed, 142 insertions, 32 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
index 10495630..599f4b11 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
index 295d9ec2..39db4d8f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
index 83b00f77..261f76db 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
index f8a7a2f3..23282723 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
index 544f5811..df1b5191 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
index 62aac4ca..712d5877 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
index 31d4543e..52de9434 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
index 7b230b65..5074417c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
index a24c2795..9411e824 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
index b35605ae..bc079ba9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
index 5e9cd3bd..2f3d05aa 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
index 0001d80f..62275f93 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
index b189414a..c5c4ea67 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
index b4eec95c..45665484 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
index 22bd4ab5..b9928383 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -30,6 +30,8 @@ class Logic2VampireLanguageMapperTrace {
         //Necessary containers
         public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace
         
+        public var Map<DefinedElement, String> definedElement2String = new HashMap
+        
         public val Map<Type, VLSFunction> type2Predicate = new HashMap;
         public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
         public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
index 8e0e0b11..c56b54be 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -14,10 +14,11 @@ import java.util.List
 import java.util.Map

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition

 

 class Logic2VampireLanguageMapper_ContainmentMapper {

-        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

-        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

+        val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

+        val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support

         val Logic2VampireLanguageMapper base

         private val VLSVariable variable = createVLSVariable => [it.name = "A"]

 

@@ -34,6 +35,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 

                 val containmentListCopy = hierarchy.typesOrderedInHierarchy

                 val relationsList = hierarchy.containmentRelations

+                val toRemove = newArrayList

+                

                 // STEP 1

                 // Find root element

                 for (l : relationsList) {

@@ -46,16 +49,51 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                         }

                 }

                 

-                for (c : containmentListCopy) {

-                        if(c.isIsAbstract) {

-                                containmentListCopy.remove(c)

-                        }

-                }

-

+//              OLD

+//              for (c : containmentListCopy) {

+//                      if(c.isIsAbstract) {

+//                              toRemove.add(c)

+//                      }

+//              }

                 // State that there must exist 1 and only 1 root element

-                val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString

-                val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))

+//              val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString

+//              val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))

 

+                var topTermVar = containmentListCopy.get(0)

+                for (l : relationsList) {

+                        var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type

+                        if(containmentListCopy.contains(pointingFrom)) {

+                                //The correct topTerm will be identified

+                                topTermVar = pointingFrom

+                        }

+                }

+                

+                val topName = topTermVar.lookup(trace.type2Predicate).constant.toString

+                val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate))

+                

+                

+                

+                var topLvlIsInInitModel = false

+                var topLvlString = ""

+                for ( c : topTermVar.subtypes) {

+                        if (c.class.simpleName.equals("TypeDefinitionImpl") ) {
+                                

+                                for (d : (c as TypeDefinition).elements) {
+                                if (trace.definedElement2String.containsKey(d)) {

+                                        topLvlIsInInitModel = true

+                                        topLvlString = d.lookup(trace.definedElement2String)

+                                }

+                        }

+                        
+                        }

+                        

+                        

+                }

+                val topInIM = topLvlIsInInitModel

+                val topStr = topLvlString

+                print(topInIM)

+                print(topStr)

+                

                 val contTop = createVLSFofFormula => [

                         it.name = support.toIDMultiple("containment_topLevel", topName)

                         it.fofRole = "axiom"

@@ -67,7 +105,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                                         it.right = createVLSEquality => [

                                                 it.left = support.duplicate(variable)

                                                 it.right = createVLSConstant => [

-                                                        it.name = "o1"

+                                                        it.name = if (topInIM) topStr else "o1"

                                                 ]

                                         ]

                                 ]

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index 4a8d2827..c50aa770 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -30,6 +30,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 //              TODO HANDLE 

                 // 1. make a list of constants equaling the min number of specified objects

                 //These numbers do not include enums or initial model elements

+                

                 val GLOBAL_MIN = config.typeScopes.minNewElements

                 val GLOBAL_MAX = config.typeScopes.maxNewElements

 

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index 2f3af593..2a121446 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -33,14 +33,24 @@ class Logic2VampireLanguageMapper_TypeMapper {
                 // 1. Each type (class) is a predicate with a single variable as input
                 for (type : types) {
                         val typePred = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
+                                if(type.name.split(" ").length == 3) {
+                                        it.constant = support.toIDMultiple("t", type.name.split(" ").get(0), type.name.split(" ").get(2))
+                                }
+                                else {
+                                        it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
+                                }
                                 it.terms += support.duplicate(variable)
                         ]
                         trace.type2Predicate.put(type, typePred)
                 }
 
                 // 2. Map each ENUM type definition to fof formula
+                //    This also Handles initial Model stuff
                 for (type : types.filter(TypeDefinition)) {
+                        
+                        //Detect if is an Enum
+                        //Otherwise, it is a defined element (from initial model)
+                        val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract
 
                         // Create a VLSFunction for each Enum Element
                         val List<VLSFunction> orElems = newArrayList
@@ -104,15 +114,20 @@ class Logic2VampireLanguageMapper_TypeMapper {
                         for (var i = globalCounter; i < globalCounter + type.elements.length; i++) {
                                 // Create objects for the enum elements
                                 val num = i + 1
+                                val index = i-globalCounter
+                                
                                 val cstTerm = createVLSFunctionAsTerm => [
                                         it.functor = "eo" + num
                                 ]
+                                if (isNotEnum) {
+                                        trace.definedElement2String.put(type.elements.get(index),cstTerm.functor)
+                                }
+                                
                                 val cst = support.toConstant(cstTerm)
                                 trace.uniqueInstances.add(cst)
-
-                                val index = i-globalCounter
+                                
                                 val enumScope = createVLSFofFormula => [
-                                        it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString,
+                                        it.name = support.toIDMultiple(if(isNotEnum) "definedType" else "enumScope", type.lookup(trace.type2Predicate).constant.toString,
                                                 type.elements.get(index).name.split(" ").get(0))
                                         it.fofRole = "axiom"
                                         it.fofFormula = createVLSUniversalQuantifier => [
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index 1ea7e30a..cab2b7ec 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
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 ee06cb39..80a74b4c 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
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 648d9600..2dc1ce19 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index a02821a5..3c14aa6c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
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 b01f92a6..b51b8ceb 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index 7634af4b..02b4f393 100644
--- 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
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 4906adfc..1feb9930 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
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 e2c945e3..fbc106a5 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
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 f465506c..77ffdd4b 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
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 e046604a..070afd3c 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
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index aff62dca..cd1b994d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 7212cce7..2cc7c421 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index d23bacad..25a165b1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index be78cace..8697d473 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index 24df5fcd..621a6e58 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -29,6 +29,8 @@ public class Logic2VampireLanguageMapperTrace {
   

   public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace;

   

+  public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>();

+  

   public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();

   

   public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
index 9deab87f..855d7637 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -19,9 +19,11 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
 import com.google.common.base.Objects;

 import com.google.common.collect.Iterables;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;

 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

@@ -34,6 +36,7 @@ import org.eclipse.emf.common.util.EList;
 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

 import org.eclipse.xtext.xbase.lib.Conversions;

 import org.eclipse.xtext.xbase.lib.Extension;

+import org.eclipse.xtext.xbase.lib.InputOutput;

 import org.eclipse.xtext.xbase.lib.ObjectExtensions;

 import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

 

@@ -58,6 +61,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     final ContainmentHierarchy hierarchy = hierarchies.get(0);

     final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy();

     final EList<Relation> relationsList = hierarchy.getContainmentRelations();

+    final ArrayList<Object> toRemove = CollectionLiterals.<Object>newArrayList();

     for (final Relation l : relationsList) {

       {

         TypeReference _get = l.getParameters().get(1);

@@ -71,14 +75,40 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         }

       }

     }

-    for (final Type c : containmentListCopy) {

-      boolean _isIsAbstract = c.isIsAbstract();

-      if (_isIsAbstract) {

-        containmentListCopy.remove(c);

+    Type topTermVar = containmentListCopy.get(0);

+    for (final Relation l_1 : relationsList) {

+      {

+        TypeReference _get = l_1.getParameters().get(0);

+        Type _referred = ((ComplexTypeReference) _get).getReferred();

+        Type pointingFrom = ((Type) _referred);

+        boolean _contains = containmentListCopy.contains(pointingFrom);

+        if (_contains) {

+          topTermVar = pointingFrom;

+        }

+      }

+    }

+    final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString();

+    final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate));

+    boolean topLvlIsInInitModel = false;

+    String topLvlString = "";

+    EList<Type> _subtypes = topTermVar.getSubtypes();

+    for (final Type c : _subtypes) {

+      boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl");

+      if (_equals) {

+        EList<DefinedElement> _elements = ((TypeDefinition) c).getElements();

+        for (final DefinedElement d : _elements) {

+          boolean _containsKey = trace.definedElement2String.containsKey(d);

+          if (_containsKey) {

+            topLvlIsInInitModel = true;

+            topLvlString = CollectionsUtil.<DefinedElement, String>lookup(d, trace.definedElement2String);

+          }

+        }

       }

     }

-    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));

+    final boolean topInIM = topLvlIsInInitModel;

+    final String topStr = topLvlString;

+    InputOutput.<Boolean>print(Boolean.valueOf(topInIM));

+    InputOutput.<String>print(topStr);

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

     final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {

       it.setName(this.support.toIDMultiple("containment_topLevel", topName));

@@ -96,7 +126,13 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
             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");

+              String _xifexpression = null;

+              if (topInIM) {

+                _xifexpression = topStr;

+              } else {

+                _xifexpression = "o1";

+              }

+              it_4.setName(_xifexpression);

             };

             VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4);

             it_3.setRight(_doubleArrow);

@@ -130,16 +166,16 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
     final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3);

     final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA);

     final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>();

-    for (final Relation l_1 : relationsList) {

+    for (final Relation l_2 : relationsList) {

       {

-        final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList);

-        TypeReference _get = l_1.getParameters().get(1);

+        final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList);

+        TypeReference _get = l_2.getParameters().get(1);

         Type _referred = ((ComplexTypeReference) _get).getReferred();

         final Type toType = ((Type) _referred);

         final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);

         this.addToMap(type2cont, toFunc, rel);

-        EList<Type> _subtypes = toType.getSubtypes();

-        for (final Type c_1 : _subtypes) {

+        EList<Type> _subtypes_1 = toType.getSubtypes();

+        for (final Type c_1 : _subtypes_1) {

           this.addToMap(type2cont, toFunc, rel);

         }

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

@@ -244,9 +280,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         variables.add(_doubleArrow);

         for (int j = 0; (j < i); j++) {

           {

-            for (final Relation l_2 : relationsList) {

+            for (final Relation l_3 : relationsList) {

               {

-                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));

+                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));

                 disjunctionList.add(rel);

               }

             }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index b9c1d28d..2d9d566d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -62,7 +62,13 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         {

           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

           final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {

-            it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));

+            int _length = type.getName().split(" ").length;

+            boolean _equals = (_length == 3);

+            if (_equals) {

+              it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2]));

+            } else {

+              it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));

+            }

             EList<VLSTerm> _terms = it.getTerms();

             VLSVariable _duplicate = this.support.duplicate(variable);

             _terms.add(_duplicate);

@@ -74,6 +80,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
       Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

       for (final TypeDefinition type_1 : _filter) {

         {

+          final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract());

           final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();

           EList<DefinedElement> _elements = type_1.getElements();

           for (final DefinedElement e : _elements) {

@@ -156,17 +163,26 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) {

             {

               final int num = (i + 1);

+              final int index = (i - globalCounter);

               VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();

               final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> {

                 it.setFunctor(("eo" + Integer.valueOf(num)));

               };

               final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);

+              if (isNotEnum) {

+                trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());

+              }

               final VLSConstant cst = this.support.toConstant(cstTerm);

               trace.uniqueInstances.add(cst);

-              final int index = (i - globalCounter);

               VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

               final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> {

-                it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), 

+                String _xifexpression = null;

+                if (isNotEnum) {

+                  _xifexpression = "definedType";

+                } else {

+                  _xifexpression = "enumScope";

+                }

+                it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), 

                   type_1.getElements().get(index).getName().split(" ")[0]));

                 it.setFofRole("axiom");

                 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();