Implement Containment mapping (partially) and revisit enum mapping

14 files changed, 334 insertions, 64 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index 052e0175..8e50f399 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 1296bf9e..99ba52b8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index fd625384..7b01a284 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
new file mode 100644
index 00000000..9f455fdd
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 978571d2..0b91349d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index b98f0332..07e249ce 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 8238a89e..115249ba 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index f64a218b..2e86d0c7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
index ec8107e8..8a9aa4bb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
@@ -38,3 +38,5 @@
 /.VampireSolutionModel.java._trace
 /.VampireCallerWithTimeout.java._trace
 /.Logic2VampireLanguageMapper_ScopeMapper.java._trace
+/.Logic2VampireLanguageMapper_Containment.java._trace
+/.Logic2VampireLanguageMapper_ContainmentMapper.java._trace
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index afe77bbe..36a727b2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

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

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

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper;

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

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

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

@@ -83,6 +84,9 @@ public class Logic2VampireLanguageMapper {
   private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this);

   

   @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this);

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

   private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this);

   

   @Accessors(AccessorType.PUBLIC_GETTER)

@@ -114,12 +118,13 @@ public class Logic2VampireLanguageMapper {
       this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);

     }

     this.scopeMapper.transformScope(config, trace);

-    trace.constantDefinitions = this.collectConstantDefinitions(problem);

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

     final Consumer<Relation> _function_3 = (Relation it) -> {

       this.relationMapper.transformRelation(it, trace);

     };

     problem.getRelations().forEach(_function_3);

+    this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace);

+    trace.constantDefinitions = this.collectConstantDefinitions(problem);

     final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {

       this.constantMapper.transformConstantDefinitionSpecification(it, trace);

     };

@@ -428,6 +433,11 @@ public class Logic2VampireLanguageMapper {
   }

   

   @Pure

+  public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() {

+    return this.containmentMapper;

+  }

+  

+  @Pure

   public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() {

     return this.relationMapper;

   }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
new file mode 100644
index 00000000..da0e5615
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -0,0 +1,180 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

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

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+import java.util.ArrayList;

+import java.util.List;

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_ContainmentMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> {

+    it.setName("A");

+  }));

+  

+  public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) {

+    final ContainmentHierarchy hierarchy = hierarchies.get(0);

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

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

+    for (final Relation l : relationsList) {

+      {

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

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

+        Type pointingTo = ((Type) _referred);

+        containmentListCopy.remove(pointingTo);

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

+        for (final Type c : _subtypes) {

+          containmentListCopy.remove(c);

+        }

+      }

+    }

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

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

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

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

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

+      it.setFofRole("axiom");

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

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

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

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

+        _variables.add(_duplicate);

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

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

+          it_2.setLeft(topTerm);

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

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

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

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

+            final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> {

+              it_4.setName("o1");

+            };

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

+            it_3.setRight(_doubleArrow);

+          };

+          VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3);

+          it_2.setRight(_doubleArrow);

+        };

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

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(contTop);

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

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

+      it.setName("A");

+    };

+    final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1);

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

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

+      it.setName("B");

+    };

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

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

+    for (final Relation l_1 : relationsList) {

+      {

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

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

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

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

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

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

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

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

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

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

+          it.setFofRole("axiom");

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

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

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

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

+            _variables.add(_duplicate);

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

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

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

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

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

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

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

+                _variables_1.add(_duplicate_1);

+                VLSAnd _createVLSAnd = this.factory.createVLSAnd();

+                final Procedure1<VLSAnd> _function_7 = (VLSAnd it_4) -> {

+                  it_4.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(fromType, trace.type2Predicate), varB));

+                  it_4.setRight(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList));

+                };

+                VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_7);

+                it_3.setOperand(_doubleArrow);

+              };

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

+              it_2.setRight(_doubleArrow);

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

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

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

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

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

+                  it_4.setName("o1");

+                };

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

+                it_3.setRight(_doubleArrow_1);

+              };

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

+            };

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

+            it_1.setOperand(_doubleArrow);

+          };

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

+          it.setFofFormula(_doubleArrow);

+        };

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

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

+        _formulas_1.add(relFormula);

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

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

+        Type pointingTo = ((Type) _referred_2);

+        containmentListCopy.remove(pointingTo);

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

+        for (final Type c : _subtypes) {

+          containmentListCopy.remove(c);

+        }

+      }

+    }

+  }

+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index 1950cad0..d2a6bff2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

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

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

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

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

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

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

@@ -48,16 +49,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
   public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

     final int GLOBAL_MIN = config.typeScopes.minNewElements;

     final int GLOBAL_MAX = config.typeScopes.maxNewElements;

-    final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList();

+    final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();

     if ((GLOBAL_MIN != 0)) {

       this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false);

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

+        localInstances.add(this.support.duplicate(i));

+      }

       this.makeFofFormula(localInstances, trace, true, null);

     }

     if ((GLOBAL_MAX != 0)) {

       this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true);

-      this.makeFofFormula(localInstances, trace, false, null);

+      this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

     }

-    int i = 0;

+    int i_1 = 1;

     int minNum = (-1);

     Map<Type, Integer> startPoints = new HashMap<Type, Integer>();

     Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet();

@@ -65,10 +69,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       {

         minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue();

         if ((minNum != 0)) {

-          this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false);

-          startPoints.put(t, Integer.valueOf(i));

-          int _i = i;

-          i = (_i + minNum);

+          this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false);

+          startPoints.put(t, Integer.valueOf(i_1));

+          int _i = i_1;

+          i_1 = (_i + minNum);

           this.makeFofFormula(localInstances, trace, true, t);

         }

       }

@@ -83,8 +87,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
           this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false);

         }

         if (((maxNum).intValue() != minNum)) {

-          int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum));

-          this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false);

+          int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum));

+          this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false);

           this.makeFofFormula(localInstances, trace, false, t_1);

         }

       }

@@ -126,18 +130,24 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
   

   protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) {

     String nm = "";

-    VLSFunction tm = null;

+    VLSTerm tm = null;

     if ((type == null)) {

       nm = "object";

       tm = this.support.topLevelTypeFunc();

     } else {

       nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString();

-      tm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate));

+      VLSAnd _createVLSAnd = this.factory.createVLSAnd();

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

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

+        it.setRight(this.support.topLevelTypeFunc());

+      };

+      VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);

+      tm = _doubleArrow;

     }

     final String name = nm;

-    final VLSFunction term = tm;

+    final VLSTerm term = tm;

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

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

       String _xifexpression = null;

       if (minimum) {

         _xifexpression = "min";

@@ -147,53 +157,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
       it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name));

       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

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

         _variables.add(_duplicate);

         VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

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

           if (minimum) {

-            final Function1<VLSTerm, VLSEquality> _function_3 = (VLSTerm i) -> {

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

               VLSEquality _createVLSEquality = this.factory.createVLSEquality();

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

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

                 VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

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

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

                 };

-                VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_5);

-                it_3.setLeft(_doubleArrow);

+                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);

+                it_3.setLeft(_doubleArrow_1);

                 it_3.setRight(i);

               };

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

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

             };

-            it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3)));

+            it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4)));

             it_2.setRight(term);

           } else {

             it_2.setLeft(term);

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

+            final Function1<VLSTerm, VLSEquality> _function_5 = (VLSTerm i) -> {

               VLSEquality _createVLSEquality = this.factory.createVLSEquality();

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

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

                 VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

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

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

                 };

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

-                it_3.setLeft(_doubleArrow);

+                VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_7);

+                it_3.setLeft(_doubleArrow_1);

                 it_3.setRight(i);

               };

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

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

             };

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

+            it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_5)));

           }

         };

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

-        it_1.setOperand(_doubleArrow);

+        VLSImplies _doubleArrow_1 = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);

+        it_1.setOperand(_doubleArrow_1);

       };

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

-      it.setFofFormula(_doubleArrow);

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

+      it.setFofFormula(_doubleArrow_1);

     };

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

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

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

     _formulas.add(cstDec);

   }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
index e2ff7a0e..119d01f1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -104,6 +104,19 @@ public class Logic2VampireLanguageMapper_Support {
     return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

   }

   

+  protected VLSFunction duplicate(final VLSFunction term, final List<VLSVariable> vars) {

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

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

+      it.setConstant(term.getConstant());

+      for (final VLSVariable v : vars) {

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

+        VLSVariable _duplicate = this.duplicate(v);

+        _terms.add(_duplicate);

+      }

+    };

+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+  }

+  

   protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) {

     VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

@@ -138,6 +151,17 @@ public class Logic2VampireLanguageMapper_Support {
     return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

   }

   

+  protected VLSFunction topLevelTypeFunc(final VLSVariable v) {

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

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

+      it.setConstant("object");

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

+      VLSVariable _duplicate = this.duplicate(v);

+      _terms.add(_duplicate);

+    };

+    return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+  }

+  

   protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) {

     VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

@@ -284,7 +308,8 @@ public class Logic2VampireLanguageMapper_Support {
       for (final Variable variable : _quantifiedVariables) {

         {

           TypeReference _range = variable.getRange();

-          final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap));

+          final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), 

+            CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap));

           typedefs.add(eq);

         }

       }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index b8d74f36..ec759ebf 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -3,8 +3,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;

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

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

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

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

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

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

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

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

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

@@ -18,7 +20,6 @@ import com.google.common.base.Objects;
 import com.google.common.collect.Iterables;

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

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

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration;

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

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

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

@@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
         it.setName("A");

       };

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

+      int globalCounter = 0;

       for (final Type type : types) {

         {

           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

@@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               };

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

               trace.element2Predicate.put(e, enumElemPred);

-              orElems.add(enumElemPred);

+            }

+          }

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

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

+          EList<DefinedElement> _elements_1 = type_1.getElements();

+          for (final DefinedElement t1 : _elements_1) {

+            {

+              EList<DefinedElement> _elements_2 = type_1.getElements();

+              for (final DefinedElement t2 : _elements_2) {

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

+                if (_equals) {

+                  final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);

+                  possibleNots.add(fct);

+                } else {

+                  final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);

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

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

+                    it.setOperand(op);

+                  };

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

+                  possibleNots.add(negFct);

+                }

+              }

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

+              possibleNots.clear();

             }

           }

           VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

@@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

                 it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));

-                it_2.setRight(this.support.unfoldOr(orElems));

+                VLSAnd _createVLSAnd = this.factory.createVLSAnd();

+                final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> {

+                  it_3.setLeft(this.support.topLevelTypeFunc(variable));

+                  it_3.setRight(this.support.unfoldOr(typeDefs));

+                };

+                VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4);

+                it_2.setRight(_doubleArrow);

               };

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

               it_1.setOperand(_doubleArrow);

@@ -118,8 +150,7 @@ public class Logic2VampireLanguageMapper_TypeMapper {
           final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);

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

           _formulas.add(res);

-          final List<VLSTerm> enumScopeElems = CollectionLiterals.<VLSTerm>newArrayList();

-          for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) {

+          for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) {

             {

               final int num = (i + 1);

               VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();

@@ -129,38 +160,50 @@ public class Logic2VampireLanguageMapper_TypeMapper {
               final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);

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

               trace.uniqueInstances.add(cst);

-              final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm);

-              enumScopeElems.add(fct);

-              for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) {

-                if ((j != i)) {

-                  final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm);

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

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

-                    it.setOperand(op);

+              final int index = i;

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

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

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

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

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

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

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

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

+                      it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm)));

+                    };

+                    VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6);

+                    it_2.setLeft(_doubleArrow);

+                    it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable));

                   };

-                  final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);

-                  enumScopeElems.add(negFct);

-                }

-              }

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

+                  it_1.setOperand(_doubleArrow);

+                };

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

+                it.setFofFormula(_doubleArrow);

+              };

+              final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3);

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

+              _formulas_1.add(enumScope);

             }

           }

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

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

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

-            it.setFofRole("axiom");

-            it.setFofFormula(this.support.unfoldAnd(enumScopeElems));

-          };

-          final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);

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

-          _formulas_1.add(enumScope);

+          int _globalCounter = globalCounter;

+          int _size = type_1.getElements().size();

+          globalCounter = (_globalCounter + _size);

         }

       }

       final Function1<Type, Boolean> _function_1 = (Type it) -> {

         boolean _isIsAbstract = it.isIsAbstract();

         return Boolean.valueOf((!_isIsAbstract));

       };

-      Iterable<TypeDeclaration> _filter_1 = Iterables.<TypeDeclaration>filter(IterableExtensions.<Type>filter(types, _function_1), TypeDeclaration.class);

-      for (final TypeDeclaration t1 : _filter_1) {

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

+      for (final Type t1 : _filter_1) {

         {

           for (final Type t2 : types) {

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