25 files changed, 167 insertions, 125 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index e2c15b75..54c44c72 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -238,7 +238,7 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
                 return createVLSFunction => [
-                        it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name)
+                        it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name)
                         it.terms += instanceOf.value.transformTerm(trace, variables)
                 ]
         }
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 60653a42..6f3b13ef 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
@@ -39,7 +39,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2VLS.put(variable, v)
 
                         val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", variable.name)
                                 ]
@@ -47,7 +47,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2TypeDecComply.put(variable, varTypeComply)
                         
                         val varTypeRes = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", variable.name)
                                 ]
@@ -136,7 +136,7 @@ class Logic2VampireLanguageMapper_RelationMapper {
                         relationVar2VLS.add(v)
 
                         val varTypeComply = createVLSFunction => [
-                                it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name)
+                                it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = support.toIDMultiple("Var", i.toString)
                                 ]
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 84aa521d..4b7ea3d0 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
@@ -18,7 +18,6 @@ class Logic2VampireLanguageMapper_ScopeMapper {
         def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {

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

 

-                

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

                 val List<VLSConstant> instances = newArrayList

                 for (var i = 0; i < config.typeScopes.minNewElements; i++) {

@@ -28,47 +27,37 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                         ]

                         instances.add(cst)

                 }

-                

-                

-                // TODO: specify for the max

-

 

-                // 2. Create initial fof formula to specify the number of elems

-                val cstDec = createVLSFofFormula => [

-                        it.name = "typeScope"

-                        it.fofRole = "axiom"

-                        it.fofFormula = createVLSUniversalQuantifier => [

-                                it.variables += support.duplicate(variable)

-                                // check below

-                                it.operand = createVLSEquivalent => [

-                                        it.left = support.topLevelTypeFunc

-                                        it.right = support.unfoldOr(instances.map [ i |

-                                                createVLSEquality => [

-                                                        it.left = createVLSVariable => [it.name = variable.name]

-                                                        it.right = i

-                                                ]

-                                        ])

+                // TODO: specify for the max

+                if (config.typeScopes.minNewElements != 0) {

+                        // 2. Create initial fof formula to specify the number of elems

+                        val cstDec = createVLSFofFormula => [

+                                it.name = "typeScope"

+                                it.fofRole = "axiom"

+                                it.fofFormula = createVLSUniversalQuantifier => [

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

+                                        // check below

+                                        it.operand = createVLSEquivalent => [

+                                                it.left = support.topLevelTypeFunc

+                                                it.right = support.unfoldOr(instances.map [ i |

+                                                        createVLSEquality => [

+                                                                it.left = createVLSVariable => [it.name = variable.name]

+                                                                it.right = i

+                                                        ]

+                                                ])

+                                        ]

                                 ]

                         ]

-                ]

-                trace.specification.formulas += cstDec

-

-

-                // TODO: specify for scope per type

-

-

-

-                // 3. Specify uniqueness of elements

-                val uniqueness = createVLSFofFormula => [

-                        it.name = "typeUniqueness"

-                        it.fofRole = "axiom"

-                        it.fofFormula = support.unfoldOr(instances.map [ i |

-                                createVLSEquality => [

-                                        it.left = createVLSVariable => [it.name = variable.name]

-                                        it.right = i

-                                ]

-                        ])

-                ]

-                trace.specification.formulas += cstDec

+                        trace.specification.formulas += cstDec

+

+                        // TODO: specify for scope per type

+                        // 3. Specify uniqueness of elements

+                        val uniqueness = createVLSFofFormula => [

+                                it.name = "typeUniqueness"

+                                it.fofRole = "axiom"

+                                it.fofFormula = support.establishUniqueness(instances)

+                        ]

+                        trace.specification.formulas += uniqueness

+                }

         }

 }

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 e69f0d51..06ec585c 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
@@ -13,6 +13,8 @@ import java.util.HashMap
 import java.util.List
 import java.util.Map
 import org.eclipse.emf.common.util.EList
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality
 
 class Logic2VampireLanguageMapper_Support {
         private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -26,6 +28,7 @@ class Logic2VampireLanguageMapper_Support {
                 ids.split("\\s+").join("_")
         }
 
+        //TODO Make more general
         def protected VLSVariable duplicate(VLSVariable vrbl) {
                 return createVLSVariable => [it.name = vrbl.name]
         }
@@ -38,6 +41,25 @@ class Logic2VampireLanguageMapper_Support {
                         ]
                 ]
         }
+        
+        //TODO Make more general
+        def establishUniqueness(List<VLSConstant> terms) {
+                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)
+                
+        }
 
         // Support Functions
         // booleans
@@ -111,7 +133,7 @@ class Logic2VampireLanguageMapper_Support {
                 val typedefs = new ArrayList<VLSTerm>
                 for (variable : expression.quantifiedVariables) {
                         val eq = createVLSFunction => [
-                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = toIDMultiple("Var", variable.name)
                                 ]
@@ -138,7 +160,7 @@ class Logic2VampireLanguageMapper_Support {
                 val typedefs = new ArrayList<VLSTerm>
                 for (variable : expression.quantifiedVariables) {
                         val eq = createVLSFunction => [
-                                it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name)
+                                it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
                                 it.terms += createVLSVariable => [
                                         it.name = toIDMultiple("Var", variable.name)
                                 ]
@@ -157,5 +179,7 @@ class Logic2VampireLanguageMapper_Support {
         def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {
                 new HashMap(map1) => [putAll(map2)]
         }
+        
+        
 
 }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
index eed10656..88e1e23a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -89,27 +89,25 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                 
                 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
                 // and store in a map
-//              val List<VLSTerm> type2PossibleNot = new ArrayList
-//              val List<VLSTerm> type2And = new ArrayList
-                for (type : types.filter[!isIsAbstract]) {
-                        for (type2 : types) {
+                for (t1 : types.filter[!isIsAbstract]) {
+                        for (t2 : types) {
                                 // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
-                                if (type == type2 || dfsSupertypeCheck(type, type2)) {
-                                        typeTrace.type2PossibleNot.put(type2, createVLSFunction => [
-                                                it.constant = type2.lookup(typeTrace.type2Predicate).constant
-                                                it.terms += createVLSVariable => [it.name = "A"]
+                                if (t1 == t2 || dfsSupertypeCheck(t1, t2)) {
+                                        typeTrace.type2PossibleNot.put(t2, createVLSFunction => [
+                                                it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                it.terms += support.duplicate(variable)
                                         ])
                                 } else {
-                                        typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [
+                                        typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
                                                 it.operand = createVLSFunction => [
-                                                        it.constant = type2.lookup(typeTrace.type2Predicate).constant
-                                                        it.terms += createVLSVariable => [it.name = "A"]
+                                                        it.constant = t2.lookup(typeTrace.type2Predicate).constant
+                                                        it.terms += support.duplicate(variable)
                                                 ]
                                         ])
                                 }
 //                              typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate))
                         }
-                        typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
+                        typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
 //                      typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) )
                         typeTrace.type2PossibleNot.clear
                 }
@@ -123,7 +121,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
                         it.name = "hierarchyHandler"
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
-                                it.variables += createVLSVariable => [it.name = "A"]
+                                it.variables += support.duplicate(variable)
                                 it.operand = createVLSEquivalent => [
                                         it.left = support.topLevelTypeFunc
                                         it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
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 9a2a1b15..4a4eedf5 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 ce05b92c..55f0ac1e 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 379d0683..e91f89cc 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 76dd192f..154ff393 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 936ab9ca..5d6ad730 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_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 e0f442f5..7c787543 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 493ff288..34f3b285 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 13281767..f8d6cd3f 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 1a777880..7b2b11f8 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/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
index e8658e7b..7e8336e2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
index aec1688a..a2229dba 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.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 e77b9866..d82649ff 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 100a52b8..030a0be9 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 231c1995..87203ed8 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 b67a307c..65689b0c 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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index 89c9637e..6643576f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -273,7 +273,7 @@ public class Logic2VampireLanguageMapper {
     VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

       TypeReference _range = instanceOf.getRange();

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

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

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

       VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables);

       _terms.add(_transformTerm);

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 561402a7..bce50fcc 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
@@ -61,7 +61,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

           TypeReference _range = variable.getRange();

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

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

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

           VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

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

@@ -75,7 +75,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();

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

           TypeReference _range = variable.getRange();

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

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

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

           VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

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

@@ -215,7 +215,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

           TypeReference _get = r.getParameters().get((i).intValue());

-          it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName()));

+          it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName()));

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

           VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();

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

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 86d8b648..8967839d 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
@@ -51,42 +51,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
         instances.add(cst);

       }

     }

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

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

-      it.setName("typeScope");

-      it.setFofRole("axiom");

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

-      final Procedure1<VLSUniversalQuantifier> _function_2 = (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_3 = (VLSEquivalent it_2) -> {

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

-          final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> {

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

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

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

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

-                it_4.setName(variable.getName());

+    if ((config.typeScopes.minNewElements != 0)) {

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

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

+        it.setName("typeScope");

+        it.setFofRole("axiom");

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

+        final Procedure1<VLSUniversalQuantifier> _function_2 = (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_3 = (VLSEquivalent it_2) -> {

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

+            final Function1<VLSConstant, VLSEquality> _function_4 = (VLSConstant i) -> {

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

+              final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {

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

+                final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {

+                  it_4.setName(variable.getName());

+                };

+                VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6);

+                it_3.setLeft(_doubleArrow);

+                it_3.setRight(i);

               };

-              VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6);

-              it_3.setLeft(_doubleArrow);

-              it_3.setRight(i);

+              return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);

             };

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

+            it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4)));

           };

-          it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSConstant, VLSEquality>map(instances, _function_4)));

+          VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);

+          it_1.setOperand(_doubleArrow);

         };

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

-        it_1.setOperand(_doubleArrow);

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

+        it.setFofFormula(_doubleArrow);

       };

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

-      it.setFofFormula(_doubleArrow);

-    };

-    final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

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

-    _formulas.add(cstDec);

+      final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

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

+      _formulas.add(cstDec);

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

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

+        it.setName("typeUniqueness");

+        it.setFofRole("axiom");

+        it.setFofFormula(this.support.establishUniqueness(instances));

+      };

+      final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);

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

+      _formulas_1.add(uniqueness);

+    }

   }

   

   public void transformScope(final LogicSolverConfiguration config, 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 b111732f..dfe624be 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
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

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

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

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

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

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

@@ -25,6 +26,7 @@ import java.util.List;
 import java.util.Map;

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

 import org.eclipse.xtend2.lib.StringConcatenation;

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

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

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

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

@@ -73,6 +75,36 @@ public class Logic2VampireLanguageMapper_Support {
     return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

   }

   

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

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

+          };

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

+          eqs.add(eq);

+        }

+      }

+    }

+    return this.unfoldAnd(eqs);

+  }

+  

   protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) {

     int _size = operands.size();

     boolean _equals = (_size == 1);

@@ -180,7 +212,7 @@ public class Logic2VampireLanguageMapper_Support {
           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

             TypeReference _range = variable.getRange();

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

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

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

             VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

@@ -229,7 +261,7 @@ public class Logic2VampireLanguageMapper_Support {
           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

             TypeReference _range = variable.getRange();

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

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

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

             VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
index 71e98871..1e845d94 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
@@ -115,47 +115,39 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       return Boolean.valueOf((!_isIsAbstract));

     };

     Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);

-    for (final Type type_2 : _filter_1) {

+    for (final Type t1 : _filter_1) {

       {

-        for (final Type type2 : types) {

-          if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) {

+        for (final Type t2 : types) {

+          if ((Objects.equal(t1, t2) || this.dfsSupertypeCheck(t1, t2))) {

             VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-              it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());

+              it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant());

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

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

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

-                it_1.setName("A");

-              };

-              VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);

-              _terms.add(_doubleArrow);

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

+              _terms.add(_duplicate);

             };

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

-            typeTrace.type2PossibleNot.put(type2, _doubleArrow);

+            typeTrace.type2PossibleNot.put(t2, _doubleArrow);

           } else {

             VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();

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

               VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();

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

-                it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());

+                it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(t2, typeTrace.type2Predicate).getConstant());

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

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

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

-                  it_2.setName("A");

-                };

-                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_5);

-                _terms.add(_doubleArrow_1);

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

+                _terms.add(_duplicate);

               };

               VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4);

               it.setOperand(_doubleArrow_1);

             };

             VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);

-            typeTrace.type2PossibleNot.put(type2, _doubleArrow_1);

+            typeTrace.type2PossibleNot.put(t2, _doubleArrow_1);

           }

         }

         Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values();

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

-        typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList));

+        typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList));

         typeTrace.type2PossibleNot.clear();

       }

     }

@@ -166,21 +158,17 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

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

-          it_2.setName("A");

-        };

-        VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_4);

-        _variables.add(_doubleArrow);

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

+        _variables.add(_duplicate);

         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

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

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

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

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

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

         };

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

-        it_1.setOperand(_doubleArrow_1);

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

+        it_1.setOperand(_doubleArrow);

       };

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

       it.setFofFormula(_doubleArrow);