22 files changed, 365 insertions, 126 deletions

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 ff5a192e..820d0db2 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
@@ -1,16 +1,19 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder

 

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory

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

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

-import java.util.List

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

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

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

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

+import java.util.HashMap

+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.RelationDeclaration

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

 

 class Logic2VampireLanguageMapper_ContainmentMapper {

         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE

@@ -74,54 +77,121 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
                 // for each edge, if the pointedTo element exists,the edge must exist also

                 val varA = createVLSVariable => [it.name = "A"]

                 val varB = createVLSVariable => [it.name = "B"]

+                val varC = createVLSVariable => [it.name = "C"]

                 val varList = newArrayList(varB, varA)

-

+                val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap

                 for (l : relationsList) {

-                        val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString

-                        val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type

-                        val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type

+                        val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)

+//                      val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type

+                        val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type)

+                        val toFunc = toType.lookup(trace.type2Predicate)

+

+                        addToMap(type2cont, toFunc, rel)

 

-                        val listForAnd = newArrayList

-//                      listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))

-                        listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))

+                        for (c : toType.subtypes) {

+                                addToMap(type2cont, toFunc, rel)

+                        }

+

+//                      val listForAnd = newArrayList

+////                    listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB))

+//                      listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList))

 //                      listForAnd.add(createVLSInequality => [

 //                              it.left = support.duplicate(varA)

 //                              it.right = support.duplicate(varB)

 //                      ])

+                        // remove subtypes of elements being pointed to

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

+//                      containmentListCopy.remove(pointingTo)

+//                      for (c : pointingTo.subtypes) {

+//                              containmentListCopy.remove(c)

+//                      }

+                        // STEP 3

+                        // Ensure that an objct only has 1 parent

+                        val relFormula = createVLSFofFormula => [

+                                it.name = support.toIDMultiple("noDupCont", rel.constant.toString)

+                                it.fofRole = "axiom"

+                                it.fofFormula = createVLSExistentialQuantifier => [

+                                        it.variables += support.duplicate(varA)

+                                        it.variables += support.duplicate(varB)

+                                        it.operand = createVLSImplies => [

+                                                it.left = support.duplicate(rel, newArrayList(varA, varB))

+                                                it.right = createVLSUnaryNegation => [

+                                                        it.operand = createVLSExistentialQuantifier => [

+                                                                it.variables += support.duplicate(varC)

+                                                                it.variables += support.duplicate(varB)

+                                                                it.operand = support.duplicate(rel, newArrayList(varC, varB))

+

+                                                        ]

+                                                ]

+                                        ]

+                                ]

+                        ]

+                        trace.specification.formulas += relFormula

 

+                }

+

+// STEP  CONT'D

+                for (e : type2cont.entrySet) {

                         val relFormula = createVLSFofFormula => [

-                                it.name = support.toIDMultiple("containment", relName)

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

                                 it.fofRole = "axiom"

 

                                 it.fofFormula = createVLSUniversalQuantifier => [

                                         it.variables += support.duplicate(varA)

                                         it.operand = createVLSImplies => [

-                                                it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA)

+                                                it.left = support.duplicate(e.key, varA)

                                                 it.right = createVLSExistentialQuantifier => [

                                                         it.variables += support.duplicate(varB)

-                                                        it.operand = support.unfoldAnd(listForAnd)

-                                                ]

+                                                        if (e.value.length > 1) {

+                                                                it.operand = makeUnique(e.value)

+                                                        } else {

+                                                                it.operand = e.value.get(0)

+                                                        }

 

-                                                createVLSEquality => [

-                                                        it.left = support.duplicate(variable)

-                                                        it.right = createVLSConstant => [

-                                                                it.name = "o1"

-                                                        ]

                                                 ]

                                         ]

                                 ]

                         ]

                         trace.specification.formulas += relFormula

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

-                        containmentListCopy.remove(pointingTo)

-                        for (c : pointingTo.subtypes) {

-                                containmentListCopy.remove(c)

-                        }

+

                 }

 

-        // STEP 3

-        // Ensure that an objct only has 1 parent

         // STEP 4

         // Ensure that there are no cycles in the hierarchy (maybe same as for step3?)

         }

+

+        protected def VLSTerm makeUnique(List<VLSFunction> list) {

+                val List<VLSTerm> possibleNots = newArrayList

+                val List<VLSTerm> uniqueRels = newArrayList

+

+                for (t1 : list) {

+                        for (t2 : list) {

+                                if (t1 == t2) {

+                                        val fct = support.duplicate(t2)

+                                        possibleNots.add(fct)

+                                } else {

+                                        val op = support.duplicate(t2)

+                                        val negFct = createVLSUnaryNegation => [

+                                                it.operand = op

+                                        ]

+                                        possibleNots.add(negFct)

+                                }

+                        }

+                        uniqueRels.add(support.unfoldAnd(possibleNots))

+                        possibleNots.clear

+                }

+                return support.unfoldOr(uniqueRels)

+        }

+

+        protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) {

+                if (!type2cont.containsKey(toFunc)) {

+                        type2cont.put(toFunc, newArrayList(rel))

+                } else {

+                        if (!type2cont.get(toFunc).contains(rel)) {

+                                type2cont.get(toFunc).add(rel)

+                        // type2cont.replace(toFunc, newArrayList(firstRel))

+                        }

+

+                }

+        }

 }

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 548deda4..bc87d3b7 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
@@ -38,10 +38,10 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 // Handling Minimum_General

                 if (GLOBAL_MIN != 0) {

                         getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)

-                        for(i : trace.uniqueInstances){

+                        for (i : trace.uniqueInstances) {

                                 localInstances.add(support.duplicate(i))

                         }

-                        

+

                         makeFofFormula(localInstances, trace, true, null)

                 }

 

@@ -83,14 +83,15 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

 // 3. Specify uniqueness of elements

                 if (trace.uniqueInstances.length != 0) {

-                        val uniqueness = createVLSFofFormula => [

-                                it.name = "typeUniqueness"

-                                it.fofRole = "axiom"

-                                it.fofFormula = support.establishUniqueness(trace.uniqueInstances)

-                        ]

-                        trace.specification.formulas += uniqueness

+                        for (e : trace.uniqueInstances) {

+                                val uniqueness = createVLSFofFormula => [

+                                        it.name = support.toIDMultiple("t_uniqueness", e.name)

+                                        it.fofRole = "axiom"

+                                        it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e)

+                                ]

+                                trace.specification.formulas += uniqueness

+                        }

                 }

-

         }

 

         def protected void getInstanceConstants(int endInd, int startInd, ArrayList list,

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 8d00d3e7..d1ea2a15 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
@@ -92,7 +92,7 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                 ]
         }
-        
+
         def protected VLSFunction topLevelTypeFunc(VLSVariable v) {
                 return createVLSFunction => [
                         it.constant = "object"
@@ -108,15 +108,26 @@ class Logic2VampireLanguageMapper_Support {
         }
 
         // TODO Make more general
-        def establishUniqueness(List<VLSConstant> terms) {
+        def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) {
+//              val List<VLSInequality> eqs = newArrayList
+//              for (t1 : terms.subList(1, terms.length)) {
+//                      for (t2 : terms.subList(0, terms.indexOf(t1))) {
+//                              val eq = createVLSInequality => [
+//                                      // TEMP
+//                                      it.left = createVLSConstant => [it.name = t2.name]
+//                                      it.right = createVLSConstant => [it.name = t1.name]
+//                              // TEMP
+//                              ]
+//                              eqs.add(eq)
+//                      }
+//              }
+//              return unfoldAnd(eqs)
                 val List<VLSInequality> eqs = newArrayList
-                for (t1 : terms.subList(1, terms.length)) {
-                        for (t2 : terms.subList(0, terms.indexOf(t1))) {
+                for (t1 : terms) {
+                        if (t1 != t2) {
                                 val eq = createVLSInequality => [
-                                        // TEMP
                                         it.left = createVLSConstant => [it.name = t2.name]
                                         it.right = createVLSConstant => [it.name = t1.name]
-                                // TEMP
                                 ]
                                 eqs.add(eq)
                         }
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 4c4247ce..1719bbcc 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
@@ -91,13 +91,12 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                                         it.right = support.unfoldOr(typeDefs)
                                                 ]
 //                                              it.right = support.unfoldOr((typeDefs))
-
                                         ]
                                 ]
                         ]
                         trace.specification.formulas += res
 
-                        for (var i = globalCounter; i < globalCounter+type.elements.length; i++) {
+                        for (var i = globalCounter; i < globalCounter + type.elements.length; i++) {
                                 // Create objects for the enum elements
                                 val num = i + 1
                                 val cstTerm = createVLSFunctionAsTerm => [
@@ -127,7 +126,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
                                 trace.specification.formulas += enumScope
 
                         }
-                        globalCounter+=type.elements.size
+                        globalCounter += type.elements.size
                 }
 
                 // HIERARCHY HANDLER
@@ -148,9 +147,35 @@ class Logic2VampireLanguageMapper_TypeMapper {
 //                      typeTrace.type2PossibleNot.clear
                         trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
                         trace.type2PossibleNot.clear
+
+                }
+
+                // 4. case where an object is not an object
+                val List<VLSTerm> type2Not = newArrayList
+                
+                for(t : types) {
+                        type2Not.add(createVLSUnaryNegation => [
+                                it.operand = support.duplicate(t.lookup(trace.type2Predicate))
+                        ])
                 }
 
-                // 5. create fof function that is an or with all the elements in map
+                val notObj = createVLSFofFormula => [
+                        it.name = "notObjectHandler"
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                it.variables += support.duplicate(variable)
+                                it.operand = createVLSEquivalent => [
+                                        it.left = createVLSUnaryNegation => [
+                                                it.operand = support.topLevelTypeFunc
+                                        ]
+                                        it.right = support.unfoldAnd(type2Not)
+                                ]
+                        ]
+                ]
+
+                trace.specification.formulas += notObj
+
+                // 4. create fof function that is an or with all the elements in map
                 val hierarch = createVLSFofFormula => [
                         it.name = "inheritanceHierarchyHandler"
                         it.fofRole = "axiom"
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 be554f99..b2e83781 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 0ee9b884..ec4554da 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 8e96ba14..85d288b2 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 ee720e29..f43d3267 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 528da797..a49422be 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 a1204329..e9060301 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 3413fc3f..ca19d1c9 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 a53a998a..bd348286 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 f265f6a3..274a1261 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 efde8350..2e16b79c 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 2cabecc8..b363474f 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 57844580..82ee023c 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 24898f59..e378eda2 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 a9589e7e..427ec9c1 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 8c0ae38d..7bc70e9d 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
@@ -10,9 +10,12 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;

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

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

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

+import com.google.common.base.Objects;

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

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

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

@@ -21,9 +24,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;

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

 import java.util.ArrayList;

+import java.util.HashMap;

 import java.util.List;

+import java.util.Map;

+import java.util.Set;

 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.ObjectExtensions;

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

@@ -107,69 +114,155 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
       it.setName("B");

     };

     final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);

+    VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();

+    final Procedure1<VLSVariable> _function_3 = (VLSVariable it) -> {

+      it.setName("C");

+    };

+    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) {

       {

-        final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString();

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

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

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

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

-        final Type fromType = ((Type) _referred);

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

-        Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred();

-        final Type toType = ((Type) _referred_1);

-        final ArrayList<VLSFunction> listForAnd = CollectionLiterals.<VLSFunction>newArrayList();

-        listForAnd.add(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList));

+        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 : _subtypes) {

+          this.addToMap(type2cont, toFunc, rel);

+        }

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

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

+          it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString()));

+          it.setFofRole("axiom");

+          VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

+          final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> {

+            EList<VLSVariable> _variables = it_1.getVariables();

+            VLSVariable _duplicate = this.support.duplicate(varA);

+            _variables.add(_duplicate);

+            EList<VLSVariable> _variables_1 = it_1.getVariables();

+            VLSVariable _duplicate_1 = this.support.duplicate(varB);

+            _variables_1.add(_duplicate_1);

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

+            final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> {

+              it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varA, varB)));

+              VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

+              final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {

+                VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier();

+                final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> {

+                  EList<VLSVariable> _variables_2 = it_4.getVariables();

+                  VLSVariable _duplicate_2 = this.support.duplicate(varC);

+                  _variables_2.add(_duplicate_2);

+                  EList<VLSVariable> _variables_3 = it_4.getVariables();

+                  VLSVariable _duplicate_3 = this.support.duplicate(varB);

+                  _variables_3.add(_duplicate_3);

+                  it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB)));

+                };

+                VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8);

+                it_3.setOperand(_doubleArrow);

+              };

+              VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_7);

+              it_2.setRight(_doubleArrow);

+            };

+            VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6);

+            it_1.setOperand(_doubleArrow);

+          };

+          VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_5);

+          it.setFofFormula(_doubleArrow);

+        };

+        final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);

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

+        _formulas_1.add(relFormula);

+      }

+    }

+    Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet();

+    for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) {

+      {

         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

-          it.setName(this.support.toIDMultiple("containment", relName));

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

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

           it.setFofRole("axiom");

           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

             EList<VLSVariable> _variables = it_1.getVariables();

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

             _variables.add(_duplicate);

             VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

-              it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA));

+            final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> {

+              it_2.setLeft(this.support.duplicate(e.getKey(), varA));

               VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();

-              final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> {

+              final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> {

                 EList<VLSVariable> _variables_1 = it_3.getVariables();

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

                 _variables_1.add(_duplicate_1);

-                it_3.setOperand(this.support.unfoldAnd(listForAnd));

+                int _length = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length;

+                boolean _greaterThan = (_length > 1);

+                if (_greaterThan) {

+                  it_3.setOperand(this.makeUnique(e.getValue()));

+                } else {

+                  it_3.setOperand(e.getValue().get(0));

+                }

               };

-              VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6);

+              VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7);

               it_2.setRight(_doubleArrow);

-              VLSEquality _createVLSEquality = this.factory.createVLSEquality();

-              final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {

-                it_3.setLeft(this.support.duplicate(this.variable));

-                VLSConstant _createVLSConstant = this.factory.createVLSConstant();

-                final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> {

-                  it_4.setName("o1");

-                };

-                VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8);

-                it_3.setRight(_doubleArrow_1);

-              };

-              ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);

             };

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

+            VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6);

             it_1.setOperand(_doubleArrow);

           };

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

+          VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);

           it.setFofFormula(_doubleArrow);

         };

-        final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3);

+        final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);

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

         _formulas_1.add(relFormula);

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

-        Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred();

-        Type pointingTo = ((Type) _referred_2);

-        containmentListCopy.remove(pointingTo);

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

-        for (final Type c : _subtypes) {

-          containmentListCopy.remove(c);

+      }

+    }

+  }

+  

+  protected VLSTerm makeUnique(final List<VLSFunction> list) {

+    final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList();

+    final List<VLSTerm> uniqueRels = CollectionLiterals.<VLSTerm>newArrayList();

+    for (final VLSFunction t1 : list) {

+      {

+        for (final VLSFunction t2 : list) {

+          boolean _equals = Objects.equal(t1, t2);

+          if (_equals) {

+            final VLSFunction fct = this.support.duplicate(t2);

+            possibleNots.add(fct);

+          } else {

+            final VLSFunction op = this.support.duplicate(t2);

+            VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

+            final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> {

+              it.setOperand(op);

+            };

+            final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function);

+            possibleNots.add(negFct);

+          }

         }

+        uniqueRels.add(this.support.unfoldAnd(possibleNots));

+        possibleNots.clear();

+      }

+    }

+    return this.support.unfoldOr(uniqueRels);

+  }

+  

+  protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) {

+    Object _xifexpression = null;

+    boolean _containsKey = type2cont.containsKey(toFunc);

+    boolean _not = (!_containsKey);

+    if (_not) {

+      _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel));

+    } else {

+      boolean _xifexpression_1 = false;

+      boolean _contains = type2cont.get(toFunc).contains(rel);

+      boolean _not_1 = (!_contains);

+      if (_not_1) {

+        _xifexpression_1 = type2cont.get(toFunc).add(rel);

       }

+      _xifexpression = Boolean.valueOf(_xifexpression_1);

     }

+    return _xifexpression;

   }

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index d2a6bff2..7aca7633 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -96,15 +96,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;

     boolean _notEquals = (_length != 0);

     if (_notEquals) {

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

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

-        it.setName("typeUniqueness");

-        it.setFofRole("axiom");

-        it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances));

-      };

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

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

-      _formulas.add(uniqueness);

+      for (final VLSConstant e : trace.uniqueInstances) {

+        {

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

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

+            it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));

+            it.setFofRole("axiom");

+            it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e));

+          };

+          final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

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

+          _formulas.add(uniqueness);

+        }

+      }

     }

   }

   

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 119d01f1..64129bf3 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
@@ -14,6 +14,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;

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

 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.QuantifiedExpression;

@@ -173,31 +174,28 @@ public class Logic2VampireLanguageMapper_Support {
     return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

   }

   

-  public VLSTerm establishUniqueness(final List<VLSConstant> terms) {

+  public VLSTerm establishUniqueness(final List<VLSConstant> terms, final VLSConstant t2) {

     final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList();

-    List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length);

-    for (final VLSConstant t1 : _subList) {

-      List<VLSConstant> _subList_1 = terms.subList(0, terms.indexOf(t1));

-      for (final VLSConstant t2 : _subList_1) {

-        {

-          VLSInequality _createVLSInequality = this.factory.createVLSInequality();

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

-            VLSConstant _createVLSConstant = this.factory.createVLSConstant();

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

-              it_1.setName(t2.getName());

-            };

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

-            it.setLeft(_doubleArrow);

-            VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant();

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

-              it_1.setName(t1.getName());

-            };

-            VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2);

-            it.setRight(_doubleArrow_1);

+    for (final VLSConstant t1 : terms) {

+      boolean _notEquals = (!Objects.equal(t1, t2));

+      if (_notEquals) {

+        VLSInequality _createVLSInequality = this.factory.createVLSInequality();

+        final Procedure1<VLSInequality> _function = (VLSInequality it) -> {

+          VLSConstant _createVLSConstant = this.factory.createVLSConstant();

+          final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> {

+            it_1.setName(t2.getName());

           };

-          final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function);

-          eqs.add(eq);

-        }

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

+          it.setLeft(_doubleArrow);

+          VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant();

+          final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> {

+            it_1.setName(t1.getName());

+          };

+          VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2);

+          it.setRight(_doubleArrow_1);

+        };

+        final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function);

+        eqs.add(eq);

       }

     }

     return this.unfoldAnd(eqs);

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 ec759ebf..9b8f049d 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
@@ -223,31 +223,68 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           trace.type2PossibleNot.clear();

         }

       }

+      final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList();

+      for (final Type t : types) {

+        VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

+        final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {

+          it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate)));

+        };

+        VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);

+        type2Not.add(_doubleArrow);

+      }

       VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

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

+        it.setName("notObjectHandler");

+        it.setFofRole("axiom");

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

+        final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> {

+          EList<VLSVariable> _variables = it_1.getVariables();

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

+          _variables.add(_duplicate);

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

+          final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> {

+            VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation();

+            final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_3) -> {

+              it_3.setOperand(this.support.topLevelTypeFunc());

+            };

+            VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6);

+            it_2.setLeft(_doubleArrow_1);

+            it_2.setRight(this.support.unfoldAnd(type2Not));

+          };

+          VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5);

+          it_1.setOperand(_doubleArrow_1);

+        };

+        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4);

+        it.setFofFormula(_doubleArrow_1);

+      };

+      final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3);

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

+      _formulas.add(notObj);

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

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

         it.setName("inheritanceHierarchyHandler");

         it.setFofRole("axiom");

         VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

           EList<VLSVariable> _variables = it_1.getVariables();

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

           _variables.add(_duplicate);

           VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

+          final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> {

             it_2.setLeft(this.support.topLevelTypeFunc());

             Collection<VLSTerm> _values = trace.type2And.values();

             final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values);

             it_2.setRight(this.support.unfoldOr(reversedList));

           };

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

-          it_1.setOperand(_doubleArrow);

+          VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6);

+          it_1.setOperand(_doubleArrow_1);

         };

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

-        it.setFofFormula(_doubleArrow);

+        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);

+        it.setFofFormula(_doubleArrow_1);

       };

-      final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);

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

-      _xblockexpression = _formulas.add(hierarch);

+      final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);

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

+      _xblockexpression = _formulas_1.add(hierarch);

     }

     return _xblockexpression;

   }