VAMPIRE: close #22, improve test structure for #39, .vql file trouble

37 files changed, 169 insertions, 279 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 024dcab9..10495630 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 7e128ad1..295d9ec2 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 0bf8ccc6..83b00f77 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 58a18bbb..f8a7a2f3 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 205afcc4..544f5811 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 b388bd43..62aac4ca 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 3092be97..31d4543e 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 8b23f34d..7b230b65 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 84682c47..a24c2795 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 e3f67a0c..b35605ae 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 bf354098..5e9cd3bd 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 da62f4c1..0001d80f 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 482b884e..b189414a 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 81c1f803..b4eec95c 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/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 395b4305..8e0e0b11 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
@@ -39,7 +39,15 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                 for (l : relationsList) {

                         var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type

                         containmentListCopy.remove(pointingTo)

-                        for (c : pointingTo.subtypes) {

+                        var List<Type> allSubtypes = newArrayList

+                        support.listSubtypes(pointingTo, allSubtypes)

+                        for (c : allSubtypes) {

+                                containmentListCopy.remove(c)

+                        }

+                }

+                

+                for (c : containmentListCopy) {

+                        if(c.isIsAbstract) {

                                 containmentListCopy.remove(c)

                         }

                 }

@@ -135,7 +143,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 // STEP 2 CONT'D

                 for (e : type2cont.entrySet) {

                         val relFormula = createVLSFofFormula => [

-                                it.name = support.toIDMultiple("containment", e.key.constant.toString)

+                                it.name = support.toIDMultiple("containment_contained", e.key.constant.toString)

                                 it.fofRole = "axiom"

 

                                 it.fofFormula = createVLSUniversalQuantifier => [

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 0ae06bc3..2dec281d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
+                //deciding name of relation
+                val nameArray = r.name.split(" ")
+                var relNameVar = ""
+                if (nameArray.length == 3) {
+                        relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                }
+                else {
+                        relNameVar = r.name
+                }
+                val relName = relNameVar
+                
                 val comply = createVLSFofFormula=> [
-                        val nameArray = r.name.split(" ")
-                        it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))
+                        
+                        it.name = support.toIDMultiple("compliance", relName)
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
                                 for (v : relVar2VLS) {
@@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                                 }
                                 it.operand = createVLSImplies => [
                                         val rel = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2))
+                                                it.constant = support.toIDMultiple("r", relName)
                                                 for (v : relVar2VLS) {
                                                         it.terms += support.duplicate(v)
                                                 }
@@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
         def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
 
-                // 1. store all variables in support wrt their name
-                // 1.1 if variable has type, creating list of type declarations
-//              val VLSVariable variable = createVLSVariable => [it.name = "A"]
-                val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
-                val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
-                val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
-                val typedefs = new ArrayList<VLSTerm>
-
-                for (variable : reldef.variables) {
-                        val v = createVLSVariable => [
-                                it.name = support.toIDMultiple("V", variable.name)
-                        ]
-                        relationVar2VLS.put(variable, v)
-
-                        val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-                                it.terms += support.duplicate(v)
-                        ]
-                        relationVar2TypeDecComply.put(variable, varTypeComply)
-                        relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
-                }
-                val nameArray = reldef.name.split(" ")
-                val comply = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
-                                nameArray.get(nameArray.length - 1))
-                        it.fofRole = "axiom"
-                        it.fofFormula = createVLSUniversalQuantifier => [
-                                for (variable : reldef.variables) {
-                                        it.variables += support.duplicate(variable.lookup(relationVar2VLS))
-
-                                }
-                                it.operand = createVLSImplies => [
-                                        it.left = createVLSFunction => [
-                                                it.constant = support.toIDMultiple("rel", reldef.name)
-                                                for (variable : reldef.variables) {
-                                                        val v = createVLSVariable => [
-                                                                it.name = variable.lookup(relationVar2VLS).name
-                                                        ]
-                                                        it.terms += v
-                                                }
-                                        ]
-                                        it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
-                                ]
-                        ]
-                ]
-
-                val res = createVLSFofFormula => [
-                        it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
-                                nameArray.get(nameArray.length - 1))
-                        it.fofRole = "axiom"
-                        it.fofFormula = createVLSUniversalQuantifier => [
-                                for (variable : reldef.variables) {
-                                        val v = createVLSVariable => [
-                                                it.name = variable.lookup(relationVar2VLS).name
-                                        ]
-                                        it.variables += v
-
-                                }
-                                it.operand = createVLSImplies => [
-                                        it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
-                                        it.right = createVLSEquivalent => [
-                                                it.left = createVLSFunction => [
-                                                        it.constant = support.toIDMultiple("rel", reldef.name)
-                                                        for (variable : reldef.variables) {
-                                                                val v = createVLSVariable => [
-                                                                        it.name = variable.lookup(relationVar2VLS).name
-                                                                ]
-                                                                it.terms += v
-
-                                                        }
-                                                ]
-                                                it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
-                                        ]
-
-                                ]
-
-                        ]
-
-                ]
-
-                // trace.relationDefinition2Predicate.put(r,res)
-                trace.specification.formulas += comply;
-                trace.specification.formulas += res;
+//              // 1. store all variables in support wrt their name
+//              // 1.1 if variable has type, creating list of type declarations
+////            val VLSVariable variable = createVLSVariable => [it.name = "A"]
+//              val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
+//              val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
+//              val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
+//              val typedefs = new ArrayList<VLSTerm>
+//
+//              for (variable : reldef.variables) {
+//                      val v = createVLSVariable => [
+//                              it.name = support.toIDMultiple("V", variable.name)
+//                      ]
+//                      relationVar2VLS.put(variable, v)
+//
+//                      val varTypeComply = createVLSFunction => [
+//                              it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
+//                              it.terms += support.duplicate(v)
+//                      ]
+//                      relationVar2TypeDecComply.put(variable, varTypeComply)
+//                      relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
+//              }
+//              val nameArray = reldef.name.split(" ")
+//              val comply = createVLSFofFormula => [
+//                      it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
+//                              nameArray.get(nameArray.length - 1))
+//                      it.fofRole = "axiom"
+//                      it.fofFormula = createVLSUniversalQuantifier => [
+//                              for (variable : reldef.variables) {
+//                                      it.variables += support.duplicate(variable.lookup(relationVar2VLS))
+//
+//                              }
+//                              it.operand = createVLSImplies => [
+//                                      it.left = createVLSFunction => [
+//                                              it.constant = support.toIDMultiple("rel", reldef.name)
+//                                              for (variable : reldef.variables) {
+//                                                      val v = createVLSVariable => [
+//                                                              it.name = variable.lookup(relationVar2VLS).name
+//                                                      ]
+//                                                      it.terms += v
+//                                              }
+//                                      ]
+//                                      it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
+//                              ]
+//                      ]
+//              ]
+//
+//              val res = createVLSFofFormula => [
+//                      it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
+//                              nameArray.get(nameArray.length - 1))
+//                      it.fofRole = "axiom"
+//                      it.fofFormula = createVLSUniversalQuantifier => [
+//                              for (variable : reldef.variables) {
+//                                      val v = createVLSVariable => [
+//                                              it.name = variable.lookup(relationVar2VLS).name
+//                                      ]
+//                                      it.variables += v
+//
+//                              }
+//                              it.operand = createVLSImplies => [
+//                                      it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
+//                                      it.right = createVLSEquivalent => [
+//                                              it.left = createVLSFunction => [
+//                                                      it.constant = support.toIDMultiple("rel", reldef.name)
+//                                                      for (variable : reldef.variables) {
+//                                                              val v = createVLSVariable => [
+//                                                                      it.name = variable.lookup(relationVar2VLS).name
+//                                                              ]
+//                                                              it.terms += v
+//
+//                                                      }
+//                                              ]
+//                                              it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
+//                                      ]
+//
+//                              ]
+//
+//                      ]
+//
+//              ]
+//
+//              // trace.relationDefinition2Predicate.put(r,res)
+//              trace.specification.formulas += comply;
+//              trace.specification.formulas += res;
 
         }
 
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 0a8812e4..4a8d2827 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
@@ -29,6 +29,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 //              TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS

 //              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_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index 195b89bb..680213ab 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
@@ -273,15 +273,11 @@ class Logic2VampireLanguageMapper_Support {
                 }
         }
 
-        def protected List<Type> listSubtypes(Type t) {
-                var List<Type> allSubtypes = newArrayList
-                if (!t.subtypes.isEmpty) {
-                        for (subt : t.subtypes) {
-                                allSubtypes.add(subt)
-                                allSubtypes = listSubtypes(subt)
-                        }
+        def protected void listSubtypes(Type t, List<Type> allSubtypes) {
+                for (subt : t.subtypes) {
+                        allSubtypes.add(subt)
+                        listSubtypes(subt, allSubtypes)
                 }
-                return allSubtypes
         }
 
         def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {
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 3bc945df..2f3af593 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
@@ -44,14 +44,19 @@ class Logic2VampireLanguageMapper_TypeMapper {
 
                         // Create a VLSFunction for each Enum Element
                         val List<VLSFunction> orElems = newArrayList
+
                         for (e : type.elements) {
+                                val nameArray = e.name.split(" ")
+                                var relNameVar = ""
+                                if (nameArray.length == 3) {
+                                        relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                                } else {
+                                        relNameVar = e.name
+                                }
+                                val relName = relNameVar
+                                
                                 val enumElemPred = createVLSFunction => [
-                                        val splitName = e.name.split(" ")
-                                        if (splitName.length > 2) {
-                                                it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
-                                        } else {
-                                                it.constant = support.toIDMultiple("e", splitName.get(0))
-                                        }
+                                        it.constant = support.toIDMultiple("e", relName)
                                         it.terms += support.duplicate(variable)
                                 ]
                                 trace.element2Predicate.put(e, enumElemPred)
@@ -80,7 +85,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
 
                         // Implement Enum Inheritence Hierarchy
                         val res = createVLSFofFormula => [
-                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
+                                it.name = support.toIDMultiple("typeDef", type.lookup(trace.type2Predicate).constant.toString)
                                 it.fofRole = "axiom"
                                 it.fofFormula = createVLSUniversalQuantifier => [
                                         it.variables += support.duplicate(variable)
@@ -105,9 +110,9 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                 val cst = support.toConstant(cstTerm)
                                 trace.uniqueInstances.add(cst)
 
-                                val index = i
+                                val index = i-globalCounter
                                 val enumScope = createVLSFofFormula => [
-                                        it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0),
+                                        it.name = support.toIDMultiple("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 43e1e477..1ea7e30a 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 4e6f6ca0..ee06cb39 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 707a6089..648d9600 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 3171324f..a02821a5 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 301df7fa..b01f92a6 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 5e53ea26..7634af4b 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 b378ed09..4906adfc 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 605ac88c..e2c945e3 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 0c289e29..f465506c 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 cb72fd90..e046604a 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 cfe1e8cd..aff62dca 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 c2079147..7212cce7 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 3c70bc14..d23bacad 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 9ef20b23..be78cace 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/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 4cdc7e6a..9deab87f 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
@@ -64,12 +64,19 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         Type _referred = ((ComplexTypeReference) _get).getReferred();

         Type pointingTo = ((Type) _referred);

         containmentListCopy.remove(pointingTo);

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

-        for (final Type c : _subtypes) {

+        List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList();

+        this.support.listSubtypes(pointingTo, allSubtypes);

+        for (final Type c : allSubtypes) {

           containmentListCopy.remove(c);

         }

       }

     }

+    for (final Type c : containmentListCopy) {

+      boolean _isIsAbstract = c.isIsAbstract();

+      if (_isIsAbstract) {

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

@@ -132,7 +139,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
         final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);

         this.addToMap(type2cont, toFunc, rel);

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

-        for (final Type c : _subtypes) {

+        for (final Type c_1 : _subtypes) {

           this.addToMap(type2cont, toFunc, rel);

         }

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

@@ -184,7 +191,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
       {

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

-          it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString()));

+          it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString()));

           it.setFofRole("axiom");

           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

           final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index d5745333..c6565f6a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -3,7 +3,6 @@ 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.VLSEquivalent;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;

@@ -17,14 +16,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;

 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.logiclanguage.Variable;

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

 import java.util.ArrayList;

 import java.util.Arrays;

-import java.util.Collection;

-import java.util.HashMap;

 import java.util.List;

-import java.util.Map;

 import org.eclipse.emf.common.util.EList;

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

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

@@ -64,10 +59,19 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         relVar2TypeDecComply.add(varTypeComply);

       }

     }

+    final String[] nameArray = r.getName().split(" ");

+    String relNameVar = "";

+    int _length_1 = nameArray.length;

+    boolean _equals = (_length_1 == 3);

+    if (_equals) {

+      relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);

+    } else {

+      relNameVar = r.getName();

+    }

+    final String relName = relNameVar;

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-      final String[] nameArray = r.getName().split(" ");

-      it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2]));

+      it.setName(this.support.toIDMultiple("compliance", relName));

       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

       final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

@@ -80,7 +84,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {

           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

           final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {

-            it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2]));

+            it_3.setConstant(this.support.toIDMultiple("r", relName));

             for (final VLSVariable v_1 : relVar2VLS) {

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

               VLSVariable _duplicate_1 = this.support.duplicate(v_1);

@@ -104,145 +108,6 @@ public class Logic2VampireLanguageMapper_RelationMapper {
   }

   

   public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) {

-    final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();

-    final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>();

-    final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>();

-    final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();

-    EList<Variable> _variables = reldef.getVariables();

-    for (final Variable variable : _variables) {

-      {

-        VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

-          it.setName(this.support.toIDMultiple("V", variable.getName()));

-        };

-        final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

-        relationVar2VLS.put(variable, v);

-        VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-          TypeReference _range = variable.getRange();

-          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));

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

-          VLSVariable _duplicate = this.support.duplicate(v);

-          _terms.add(_duplicate);

-        };

-        final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);

-        relationVar2TypeDecComply.put(variable, varTypeComply);

-        relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply));

-      }

-    }

-    final String[] nameArray = reldef.getName().split(" ");

-    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-      int _length = nameArray.length;

-      int _minus = (_length - 2);

-      int _length_1 = nameArray.length;

-      int _minus_1 = (_length_1 - 1);

-      it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], 

-        nameArray[_minus_1]));

-      it.setFofRole("axiom");

-      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

-      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {

-        EList<Variable> _variables_1 = reldef.getVariables();

-        for (final Variable variable_1 : _variables_1) {

-          EList<VLSVariable> _variables_2 = it_1.getVariables();

-          VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS));

-          _variables_2.add(_duplicate);

-        }

-        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

-        final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {

-          VLSFunction _createVLSFunction = this.factory.createVLSFunction();

-          final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {

-            it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName()));

-            EList<Variable> _variables_3 = reldef.getVariables();

-            for (final Variable variable_2 : _variables_3) {

-              {

-                VLSVariable _createVLSVariable = this.factory.createVLSVariable();

-                final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {

-                  it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());

-                };

-                final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);

-                EList<VLSTerm> _terms = it_3.getTerms();

-                _terms.add(v);

-              }

-            }

-          };

-          VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);

-          it_2.setLeft(_doubleArrow);

-          Collection<VLSFunction> _values = relationVar2TypeDecComply.values();

-          ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

-          it_2.setRight(this.support.unfoldAnd(_arrayList));

-        };

-        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);

-        it_1.setOperand(_doubleArrow);

-      };

-      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);

-      it.setFofFormula(_doubleArrow);

-    };

-    final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

-    VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

-      int _length = nameArray.length;

-      int _minus = (_length - 2);

-      int _length_1 = nameArray.length;

-      int _minus_1 = (_length_1 - 1);

-      it.setName(this.support.toIDMultiple("relation", nameArray[_minus], 

-        nameArray[_minus_1]));

-      it.setFofRole("axiom");

-      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

-      final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

-        EList<Variable> _variables_1 = reldef.getVariables();

-        for (final Variable variable_1 : _variables_1) {

-          {

-            VLSVariable _createVLSVariable = this.factory.createVLSVariable();

-            final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {

-              it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());

-            };

-            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3);

-            EList<VLSVariable> _variables_2 = it_1.getVariables();

-            _variables_2.add(v);

-          }

-        }

-        VLSImplies _createVLSImplies = this.factory.createVLSImplies();

-        final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {

-          Collection<VLSFunction> _values = relationVar2TypeDecRes.values();

-          ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);

-          it_2.setLeft(this.support.unfoldAnd(_arrayList));

-          VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

-          final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> {

-            VLSFunction _createVLSFunction = this.factory.createVLSFunction();

-            final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> {

-              it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName()));

-              EList<Variable> _variables_2 = reldef.getVariables();

-              for (final Variable variable_2 : _variables_2) {

-                {

-                  VLSVariable _createVLSVariable = this.factory.createVLSVariable();

-                  final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> {

-                    it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());

-                  };

-                  final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);

-                  EList<VLSTerm> _terms = it_4.getTerms();

-                  _terms.add(v);

-                }

-              }

-            };

-            VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);

-            it_3.setLeft(_doubleArrow);

-            it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS));

-          };

-          VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);

-          it_2.setRight(_doubleArrow);

-        };

-        VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);

-        it_1.setOperand(_doubleArrow);

-      };

-      VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);

-      it.setFofFormula(_doubleArrow);

-    };

-    final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1);

-    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

-    _formulas.add(comply);

-    EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();

-    _formulas_1.add(res);

   }

   

   public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) {

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 89633ca1..f1d73bec 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
@@ -403,20 +403,14 @@ public class Logic2VampireLanguageMapper_Support {
     return _xifexpression;

   }

   

-  protected List<Type> listSubtypes(final Type t) {

-    List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList();

-    boolean _isEmpty = t.getSubtypes().isEmpty();

-    boolean _not = (!_isEmpty);

-    if (_not) {

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

-      for (final Type subt : _subtypes) {

-        {

-          allSubtypes.add(subt);

-          allSubtypes = this.listSubtypes(subt);

-        }

+  protected void listSubtypes(final Type t, final List<Type> allSubtypes) {

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

+    for (final Type subt : _subtypes) {

+      {

+        allSubtypes.add(subt);

+        this.listSubtypes(subt, allSubtypes);

       }

     }

-    return allSubtypes;

   }

   

   protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) {

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 9b8f049d..b9c1d28d 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
@@ -78,16 +78,19 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           EList<DefinedElement> _elements = type_1.getElements();

           for (final DefinedElement e : _elements) {

             {

+              final String[] nameArray = e.getName().split(" ");

+              String relNameVar = "";

+              int _length = nameArray.length;

+              boolean _equals = (_length == 3);

+              if (_equals) {

+                relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);

+              } else {

+                relNameVar = e.getName();

+              }

+              final String relName = relNameVar;

               VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-                final String[] splitName = e.getName().split(" ");

-                int _length = splitName.length;

-                boolean _greaterThan = (_length > 2);

-                if (_greaterThan) {

-                  it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2]));

-                } else {

-                  it.setConstant(this.support.toIDMultiple("e", splitName[0]));

-                }

+                it.setConstant(this.support.toIDMultiple("e", relName));

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

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

                 _terms.add(_duplicate);

@@ -123,7 +126,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           }

           VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-            it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0]));

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

             it.setFofRole("axiom");

             VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

             final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {

@@ -160,10 +163,10 @@ 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 int index = i;

+              final int index = (i - globalCounter);

               VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

-                it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], 

+                it.setName(this.support.toIDMultiple("enumScope", 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();