19 files changed, 173 insertions, 186 deletions

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 4a4eedf5..bda7463e 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 55f0ac1e..a062fcec 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 e91f89cc..5fc0da27 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 154ff393..562b9bbf 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 5d6ad730..dd7bdf86 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 7c787543..496d27b3 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 34f3b285..4a03f2ce 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 f8d6cd3f..511f4a1f 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 7b2b11f8..37e9480c 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 7e8336e2..f473c4bc 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 a2229dba..e53791d6 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 d82649ff..1b112c56 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 030a0be9..c8284658 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 87203ed8..89d4c657 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 65689b0c..3c98bd64 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index 855815f8..2b491209 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -8,8 +8,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;

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

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

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

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

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

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

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

 import java.util.HashMap;

 import java.util.Map;

@@ -24,10 +26,20 @@ public class Logic2VampireLanguageMapperTrace {
   

   public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace;

   

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

+  

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

+  

+  public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>();

+  

+  public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>();

+  

   public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions;

   

   public Map<RelationDeclaration, RelationDefinition> relationDefinitions;

   

+  public Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap<RelationDeclaration, VLSFunction>();

+  

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

   

   public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>();

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 bce50fcc..4f5c6acc 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
@@ -15,6 +15,7 @@ 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.RelationDefinition;

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

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

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

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

@@ -44,17 +45,84 @@ public class Logic2VampireLanguageMapper_RelationMapper {
     this.base = base;

   }

   

-  public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) {

+  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {

+    final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>();

+    final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();

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

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

+    ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);

+    for (final Integer i : _doubleDotLessThan) {

+      {

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

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

+          it.setName(this.support.toIDMultiple("V", i.toString()));

+        };

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

+        relVar2VLS.add(v);

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

+        final Type relType = ((ComplexTypeReference) _get).getReferred();

+        final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v);

+        relVar2TypeDecComply.add(varTypeComply);

+      }

+    }

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

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

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

+      it.setName(this.support.toIDMultiple("compliance", nameArray[0], 

+        nameArray[2]));

+      it.setFofRole("axiom");

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

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

+        for (final VLSVariable v : relVar2VLS) {

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

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

+          _variables.add(_duplicate);

+        }

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

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

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

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

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

+            int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

+            ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true);

+            for (final Integer i_1 : _doubleDotLessThan_1) {

+              {

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

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

+                  it_4.setName(relVar2VLS.get((i_1).intValue()).getName());

+                };

+                final VLSVariable v_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);

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

+                _terms.add(v_1);

+              }

+            }

+          };

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

+          it_2.setLeft(_doubleArrow);

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

+        };

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

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(comply);

+  }

+  

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

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

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

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

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

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

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

     for (final Variable variable : _variables) {

       {

         VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

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

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

         };

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

         relationVar2VLS.put(variable, v);

@@ -63,56 +131,39 @@ public class Logic2VampireLanguageMapper_RelationMapper {
           TypeReference _range = variable.getRange();

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

-            it_1.setName(this.support.toIDMultiple("Var", variable.getName()));

-          };

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

-          _terms.add(_doubleArrow);

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

+          _terms.add(_duplicate);

         };

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

         relationVar2TypeDecComply.put(variable, varTypeComply);

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

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

-          TypeReference _range = variable.getRange();

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

-            it_1.setName(this.support.toIDMultiple("Var", variable.getName()));

-          };

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

-          _terms.add(_doubleArrow);

-        };

-        final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2);

-        relationVar2TypeDecRes.put(variable, varTypeRes);

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

       }

     }

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-      it.setName(this.support.toIDMultiple("compliance", r.getName()));

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

+      int _length = nameArray.length;

+      int _minus = (_length - 2);

+      int _length_1 = nameArray.length;

+      int _minus_1 = (_length_1 - 1);

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

+        nameArray[_minus_1]));

       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

         for (final Variable variable_1 : _variables_1) {

-          {

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

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

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

-            };

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

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

-            _variables_2.add(v);

-          }

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

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

+          _variables_2.add(_duplicate);

         }

         VLSImplies _createVLSImplies = this.factory.createVLSImplies();

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

           VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

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

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

-            for (final Variable variable_2 : _variables_2) {

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

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

+            for (final Variable variable_2 : _variables_3) {

               {

                 VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

@@ -139,11 +190,11 @@ public class Logic2VampireLanguageMapper_RelationMapper {
     final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

     VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();

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

-      it.setName(this.support.toIDMultiple("relation", r.getName()));

+      it.setName(this.support.toIDMultiple("relation", reldef.getName()));

       it.setFofRole("axiom");

       VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

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

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

         for (final Variable variable_1 : _variables_1) {

           {

             VLSVariable _createVLSVariable = this.factory.createVLSVariable();

@@ -164,8 +215,8 @@ public class Logic2VampireLanguageMapper_RelationMapper {
           final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> {

             VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

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

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

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

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

               for (final Variable variable_2 : _variables_2) {

                 {

                   VLSVariable _createVLSVariable = this.factory.createVLSVariable();

@@ -180,7 +231,7 @@ public class Logic2VampireLanguageMapper_RelationMapper {
             };

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

             it_3.setLeft(_doubleArrow);

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

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

           };

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

           it_2.setRight(_doubleArrow);

@@ -198,89 +249,6 @@ public class Logic2VampireLanguageMapper_RelationMapper {
     _formulas_1.add(res);

   }

   

-  public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {

-    final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>();

-    final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>();

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

-    int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

-    ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);

-    for (final Integer i : _doubleDotLessThan) {

-      {

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

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

-          it.setName(this.support.toIDMultiple("Var", i.toString()));

-        };

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

-        relationVar2VLS.add(v);

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

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

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

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

-            it_1.setName(this.support.toIDMultiple("Var", i.toString()));

-          };

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

-          _terms.add(_doubleArrow);

-        };

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

-        relationVar2TypeDecComply.add(varTypeComply);

-      }

-    }

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

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

-      it.setName(this.support.toIDMultiple("compliance", r.getName()));

-      it.setFofRole("axiom");

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

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

-        int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

-        ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true);

-        for (final Integer i_1 : _doubleDotLessThan_1) {

-          {

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

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

-              it_2.setName(relationVar2VLS.get((i_1).intValue()).getName());

-            };

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

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

-            _variables.add(v);

-          }

-        }

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

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

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

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

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

-            int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;

-            ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true);

-            for (final Integer i_2 : _doubleDotLessThan_2) {

-              {

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

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

-                  it_4.setName(relationVar2VLS.get((i_2).intValue()).getName());

-                };

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

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

-                _terms.add(v);

-              }

-            }

-          };

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

-          it_2.setLeft(_doubleArrow);

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

-        };

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

-        it_1.setOperand(_doubleArrow);

-      };

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

-      it.setFofFormula(_doubleArrow);

-    };

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

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

-    _formulas.add(comply);

-  }

-  

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

     if (r instanceof RelationDeclaration) {

       _transformRelation((RelationDeclaration)r, 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 dfe624be..35497eab 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
@@ -17,6 +17,7 @@ import com.google.common.collect.Iterables;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;

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

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

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

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

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

 import java.util.ArrayList;

@@ -52,14 +53,39 @@ public class Logic2VampireLanguageMapper_Support {
     return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");

   }

   

-  protected VLSVariable duplicate(final VLSVariable vrbl) {

+  protected VLSVariable duplicate(final VLSVariable term) {

     VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

-      it.setName(vrbl.getName());

+      it.setName(term.getName());

     };

     return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

   }

   

+  protected VLSFunction duplicate(final VLSFunction term) {

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

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

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

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

+      for (final VLSTerm v : _terms) {

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

+        VLSVariable _duplicate = this.duplicate(((VLSVariable) v));

+        _terms_1.add(_duplicate);

+      }

+    };

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

+  }

+  

+  protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) {

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

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

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

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

+      VLSVariable _duplicate = this.duplicate(v);

+      _terms.add(_duplicate);

+    };

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

+  }

+  

   protected VLSFunction topLevelTypeFunc() {

     VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

@@ -287,6 +313,30 @@ public class Logic2VampireLanguageMapper_Support {
     return _xblockexpression;

   }

   

+  protected boolean dfsSupertypeCheck(final Type type, final Type type2) {

+    boolean _xifexpression = false;

+    boolean _isEmpty = type.getSupertypes().isEmpty();

+    if (_isEmpty) {

+      return false;

+    } else {

+      boolean _xifexpression_1 = false;

+      boolean _contains = type.getSupertypes().contains(type2);

+      if (_contains) {

+        return true;

+      } else {

+        EList<Type> _supertypes = type.getSupertypes();

+        for (final Type supertype : _supertypes) {

+          boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2);

+          if (_dfsSupertypeCheck) {

+            return true;

+          }

+        }

+      }

+      _xifexpression = _xifexpression_1;

+    }

+    return _xifexpression;

+  }

+  

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

     HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1);

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

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 1e845d94..b582fb96 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
@@ -4,7 +4,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;

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

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

-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes;

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

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

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

@@ -46,8 +45,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
   

   @Override

   public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

-    final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes();

-    trace.typeMapperTrace = typeTrace;

     VLSVariable _createVLSVariable = this.factory.createVLSVariable();

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

       it.setName("A");

@@ -57,13 +54,13 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
       {

         VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-          it.setConstant(this.support.toIDMultiple("t", type.getName()));

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

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

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

           _terms.add(_duplicate);

         };

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

-        typeTrace.type2Predicate.put(type, typePred);

+        trace.type2Predicate.put(type, typePred);

       }

     }

     Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);

@@ -75,19 +72,19 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
           {

             VLSFunction _createVLSFunction = this.factory.createVLSFunction();

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

-              it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName()));

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

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

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

               _terms.add(_duplicate);

             };

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

-            typeTrace.element2Predicate.put(e, enumElemPred);

+            trace.element2Predicate.put(e, enumElemPred);

             orElems.add(enumElemPred);

           }

         }

         VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

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

-          it.setName(this.support.toIDMultiple("typeDef", type_1.getName()));

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

           it.setFofRole("axiom");

           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();

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

@@ -96,7 +93,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
             _variables.add(_duplicate);

             VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

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

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

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

             };

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

@@ -118,37 +115,21 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
     for (final Type t1 : _filter_1) {

       {

         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(t2, typeTrace.type2Predicate).getConstant());

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

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

-              _terms.add(_duplicate);

-            };

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

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

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

+            trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));

           } 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(t2, typeTrace.type2Predicate).getConstant());

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

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

-                _terms.add(_duplicate);

-              };

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

-              it.setOperand(_doubleArrow_1);

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

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

             };

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

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

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

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

           }

         }

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

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

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

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

-        typeTrace.type2PossibleNot.clear();

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

+        trace.type2PossibleNot.clear();

       }

     }

     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

@@ -163,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
         VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();

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

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

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

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

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

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

         };

@@ -178,30 +159,6 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log
     _formulas.add(hierarch);

   }

   

-  public boolean dfsSupertypeCheck(final Type type, final Type type2) {

-    boolean _xifexpression = false;

-    boolean _isEmpty = type.getSupertypes().isEmpty();

-    if (_isEmpty) {

-      return false;

-    } else {

-      boolean _xifexpression_1 = false;

-      boolean _contains = type.getSupertypes().contains(type2);

-      if (_contains) {

-        return true;

-      } else {

-        EList<Type> _supertypes = type.getSupertypes();

-        for (final Type supertype : _supertypes) {

-          boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2);

-          if (_dfsSupertypeCheck) {

-            return true;

-          }

-        }

-      }

-      _xifexpression = _xifexpression_1;

-    }

-    return _xifexpression;

-  }

-  

   @Override

   public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

     throw new UnsupportedOperationException("TODO: auto-generated method stub");