38 files changed, 2113 insertions, 0 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
new file mode 100644
index 00000000..b86e8068
--- /dev/null
+++ 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
new file mode 100644
index 00000000..8e50f399
--- /dev/null
+++ 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore
new file mode 100644
index 00000000..70f60102
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore
@@ -0,0 +1,10 @@
+/.VampireSolver.java._trace
+/.TypeMappingTechnique.java._trace
+/.VampireBackendSolver.java._trace
+/.VampireSolverConfiguration.java._trace
+/.VampireAnalyzerConfiguration.xtendbin
+/.VampireSolver.xtendbin
+/TypeMappingTechnique.java
+/VampireBackendSolver.java
+/VampireSolver.java
+/VampireSolverConfiguration.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java
new file mode 100644
index 00000000..8ffba2f1
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java
@@ -0,0 +1,6 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner;

+

+@SuppressWarnings("all")

+public enum TypeMappingTechnique {

+  FilteredTypes;

+}

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

+

+@SuppressWarnings("all")

+public enum VampireBackendSolver {

+}

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

+

+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup;

+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

+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.Vampire2LogicMapper;

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

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException;

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;

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

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;

+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;

+import java.util.List;

+import org.eclipse.xtend2.lib.StringConcatenation;

+

+@SuppressWarnings("all")

+public class VampireSolver extends LogicReasoner {

+  public VampireSolver() {

+    VampireLanguagePackage.eINSTANCE.eClass();

+    final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated();

+    VampireLanguageStandaloneSetup.doSetup();

+  }

+  

+  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper();

+  

+  private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper();

+  

+  private final VampireHandler handler = new VampireHandler();

+  

+  private final String fileName = "vampireProblem.tptp";

+  

+  @Override

+  public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException {

+    final VampireSolverConfiguration vampireConfig = this.asConfig(config);

+    final long transformationStart = System.currentTimeMillis();

+    final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);

+    final VampireModel vampireProblem = result.getOutput();

+    final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

+    String fileURI = null;

+    String vampireCode = null;

+    vampireCode = workspace.writeModelToString(vampireProblem, this.fileName);

+    final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || 

+      (vampireConfig.documentationLevel == DocumentationLevel.FULL));

+    if (writeFile) {

+      fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString();

+    }

+    long _currentTimeMillis = System.currentTimeMillis();

+    final long transformationTime = (_currentTimeMillis - transformationStart);

+    return null;

+  }

+  

+  public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) {

+    if ((configuration instanceof VampireSolverConfiguration)) {

+      return ((VampireSolverConfiguration)configuration);

+    } else {

+      StringConcatenation _builder = new StringConcatenation();

+      _builder.append("The configuration have to be an ");

+      String _simpleName = VampireSolverConfiguration.class.getSimpleName();

+      _builder.append(_simpleName);

+      _builder.append("!");

+      throw new IllegalArgumentException(_builder.toString());

+    }

+  }

+  

+  @Override

+  public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) {

+    return null;

+  }

+}

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

+

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;

+

+@SuppressWarnings("all")

+public class VampireSolverConfiguration extends LogicSolverConfiguration {

+}

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
new file mode 100644
index 00000000..99ba52b8
--- /dev/null
+++ 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
new file mode 100644
index 00000000..0210a300
--- /dev/null
+++ 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
new file mode 100644
index 00000000..7b01a284
--- /dev/null
+++ 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
new file mode 100644
index 00000000..0b91349d
--- /dev/null
+++ 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
new file mode 100644
index 00000000..07e249ce
--- /dev/null
+++ 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
new file mode 100644
index 00000000..115249ba
--- /dev/null
+++ 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
new file mode 100644
index 00000000..2e86d0c7
--- /dev/null
+++ 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
new file mode 100644
index 00000000..e870dabc
--- /dev/null
+++ 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
new file mode 100644
index 00000000..ed198ef6
--- /dev/null
+++ 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
new file mode 100644
index 00000000..cf8e4acd
--- /dev/null
+++ 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
new file mode 100644
index 00000000..07d5b7b4
--- /dev/null
+++ 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
new file mode 100644
index 00000000..983108a2
--- /dev/null
+++ 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
new file mode 100644
index 00000000..4442cdea
--- /dev/null
+++ 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/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
new file mode 100644
index 00000000..8a9aa4bb
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
@@ -0,0 +1,42 @@
+/.Logic2VampireLanguageMapper_ConstantMapper.java._trace
+/.Logic2VampireLanguageMapper.java._trace
+/.Logic2VampireLanguageMapperTrace.java._trace
+/.Logic2VampireLanguageMapper_TypeMapperTrace.java._trace
+/.VampireModelInterpretation_TypeInterpretation.java._trace
+/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.java._trace
+/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java._trace
+/.Logic2VampireLanguageMapper_TypeMapper.java._trace
+/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace
+/.Logic2VampireLanguageMapper_Support.java._trace
+/.Logic2VampireLanguageMapper_RelationMapper.java._trace
+/.Logic2VampireLanguageMapper.xtendbin
+/.Logic2VampireLanguageMapperTrace.xtendbin
+/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+/.Logic2VampireLanguageMapper_Support.xtendbin
+/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin
+/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin
+/.VampireModelInterpretation_TypeInterpretation.xtendbin
+/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+/Logic2VampireLanguageMapper.java
+/Logic2VampireLanguageMapperTrace.java
+/Logic2VampireLanguageMapper_ConstantMapper.java
+/Logic2VampireLanguageMapper_RelationMapper.java
+/Logic2VampireLanguageMapper_Support.java
+/Logic2VampireLanguageMapper_TypeMapper.java
+/Logic2VampireLanguageMapper_TypeMapperTrace.java
+/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java
+/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
+/VampireModelInterpretation_TypeInterpretation.java
+/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java
+/.Vampire2LogicMapper.java._trace
+/.VampireHandler.java._trace
+/.MonitoredVampireSolution.java._trace
+/.SolverConfiguration.java._trace
+/.VampireSolverException.java._trace
+/.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
new file mode 100644
index 00000000..36a727b2
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -0,0 +1,454 @@
+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;

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

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

+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.VLSFofFormula;

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

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

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

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

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

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

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

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

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

+import com.google.common.collect.Iterables;

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;

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

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

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

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

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

+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.Distinct;

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

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

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

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

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

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

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

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

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

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

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

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

+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.SymbolicDeclaration;

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

+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 hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;

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

+import java.util.Arrays;

+import java.util.Collections;

+import java.util.HashMap;

+import java.util.List;

+import java.util.Map;

+import java.util.function.Consumer;

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

+import org.eclipse.xtend.lib.annotations.AccessorType;

+import org.eclipse.xtend.lib.annotations.Accessors;

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

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

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

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

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

+  private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this);

+  

+  @Accessors(AccessorType.PUBLIC_GETTER)

+  private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this);

+  

+  public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) {

+    VLSComment _createVLSComment = this.factory.createVLSComment();

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

+      it.setComment("This is an initial Test Comment");

+    };

+    final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function);

+    VampireModel _createVampireModel = this.factory.createVampireModel();

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

+      EList<VLSComment> _comments = it.getComments();

+      _comments.add(initialComment);

+    };

+    final VampireModel specification = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1);

+    Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace();

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

+      it.specification = specification;

+    };

+    final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.<Logic2VampireLanguageMapperTrace>operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2);

+    boolean _isEmpty = problem.getTypes().isEmpty();

+    boolean _not = (!_isEmpty);

+    if (_not) {

+      this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);

+    }

+    this.scopeMapper.transformScope(config, trace);

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

+    };

+    Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4);

+    EList<Assertion> _assertions = problem.getAssertions();

+    for (final Assertion assertion : _assertions) {

+      this.transformAssertion(assertion, trace);

+    }

+    return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace);

+  }

+  

+  protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) {

+    return null;

+  }

+  

+  private HashMap<ConstantDeclaration, ConstantDefinition> collectConstantDefinitions(final LogicProblem problem) {

+    final HashMap<ConstantDeclaration, ConstantDefinition> res = new HashMap<ConstantDeclaration, ConstantDefinition>();

+    final Function1<ConstantDefinition, Boolean> _function = (ConstantDefinition it) -> {

+      ConstantDeclaration _defines = it.getDefines();

+      return Boolean.valueOf((_defines != null));

+    };

+    final Consumer<ConstantDefinition> _function_1 = (ConstantDefinition it) -> {

+      res.put(it.getDefines(), it);

+    };

+    IterableExtensions.<ConstantDefinition>filter(Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1);

+    return res;

+  }

+  

+  private HashMap<RelationDeclaration, RelationDefinition> collectRelationDefinitions(final LogicProblem problem) {

+    final HashMap<RelationDeclaration, RelationDefinition> res = new HashMap<RelationDeclaration, RelationDefinition>();

+    final Function1<RelationDefinition, Boolean> _function = (RelationDefinition it) -> {

+      RelationDeclaration _defines = it.getDefines();

+      return Boolean.valueOf((_defines != null));

+    };

+    final Consumer<RelationDefinition> _function_1 = (RelationDefinition it) -> {

+      res.put(it.getDefines(), it);

+    };

+    IterableExtensions.<RelationDefinition>filter(Iterables.<RelationDefinition>filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1);

+    return res;

+  }

+  

+  protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) {

+    boolean _xblockexpression = false;

+    {

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

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

+        it.setName(this.support.toID(assertion.getName()));

+        it.setFofRole("axiom");

+        it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP));

+      };

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

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

+      _xblockexpression = _formulas.add(res);

+    }

+    return _xblockexpression;

+  }

+  

+  protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSTerm _xifexpression = null;

+    boolean _isValue = literal.isValue();

+    boolean _equals = (_isValue == true);

+    if (_equals) {

+      _xifexpression = this.factory.createVLSTrue();

+    } else {

+      _xifexpression = this.factory.createVLSFalse();

+    }

+    return _xifexpression;

+  }

+  

+  protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSInt _createVLSInt = this.factory.createVLSInt();

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

+      it.setValue(Integer.valueOf(literal.getValue()).toString());

+    };

+    return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    VLSReal _createVLSReal = this.factory.createVLSReal();

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

+      it.setValue(literal.getValue().toString());

+    };

+    return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setOperand(this.transformTerm(not.getOperand(), trace, variables));

+    };

+    return ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    final Function1<Term, VLSTerm> _function = (Term it) -> {

+      return this.transformTerm(it, trace, variables);

+    };

+    return this.support.unfoldAnd(ListExtensions.<Term, VLSTerm>map(and.getOperands(), _function));

+  }

+  

+  protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    final Function1<Term, VLSTerm> _function = (Term it) -> {

+      return this.transformTerm(it, trace, variables);

+    };

+    return this.support.unfoldOr(ListExtensions.<Term, VLSTerm>map(or.getOperands(), _function));

+  }

+  

+  protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables));

+      it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables));

+    };

+    return ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables));

+      it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables));

+    };

+    return ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function);

+  }

+  

+  protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables));

+      it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables));

+    };

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

+  }

+  

+  protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables);

+  }

+  

+  protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.support.createQuantifiedExpression(this, forall, trace, variables, true);

+  }

+  

+  protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.support.createQuantifiedExpression(this, exists, trace, variables, false);

+  }

+  

+  protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      TypeReference _range = instanceOf.getRange();

+      it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant());

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

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

+      _terms.add(_transformTerm);

+    };

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

+  }

+  

+  protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables);

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.typeMapper.transformReference(referred, trace);

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setName(this.support.toID(constant.getName()));

+    };

+    final VLSConstant res = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);

+    return res;

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return null;

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables));

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return null;

+  }

+  

+  protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    return null;

+  }

+  

+  /**

+   * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,

+   *    List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,

+   *    Map<Variable, VLSVariable> variables) {

+   *    if (trace.relationDefinitions.containsKey(relation)) {

+   *            this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),

+   *                    parameterSubstitutions, trace, variables)

+   *    }

+   *    else {

+   * //                                         if (relationMapper.transformToHostedField(relation, trace)) {

+   * //                                                 val VLSRelation = relation.lookup(trace.relationDeclaration2Field)

+   * //                                                 // R(a,b) =>

+   * //                                                 // b in a.R

+   * //                                                 return createVLSSubset => [

+   * //                                                         it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)

+   * //                                                         it.rightOperand = createVLSJoin => [

+   * //                                                                 it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)

+   * //                                                                 it.rightOperand = createVLSReference => [it.referred = VLSRelation]

+   * //                                                         ]

+   * //                                                 ]

+   * //                                         } else {

+   * //                                                 val target = createVLSJoin => [

+   * //                                                         leftOperand = createVLSReference => [referred = trace.logicLanguage]

+   * //                                                         rightOperand = createVLSReference => [

+   * //                                                                 referred = relation.lookup(trace.relationDeclaration2Global)

+   * //                                                         ]

+   * //                                                 ]

+   * //                                                 val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)

+   * //

+   * //                                                 return createVLSSubset => [

+   * //                                                         leftOperand = source

+   * //                                                         rightOperand = target

+   * //                                                 ]

+   * //                                         }

+   *    }

+   * }

+   */

+  protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

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

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

+      it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant());

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

+      final Function1<Term, VLSTerm> _function_1 = (Term p) -> {

+        return this.transformTerm(p, trace, variables);

+      };

+      List<VLSTerm> _map = ListExtensions.<Term, VLSTerm>map(parameterSubstitutions, _function_1);

+      Iterables.<VLSTerm>addAll(_terms, _map);

+    };

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

+  }

+  

+  protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) {

+    return _transformTypeReference(boolTypeReference, trace);

+  }

+  

+  protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    if (and instanceof And) {

+      return _transformTerm((And)and, trace, variables);

+    } else if (and instanceof BoolLiteral) {

+      return _transformTerm((BoolLiteral)and, trace, variables);

+    } else if (and instanceof Distinct) {

+      return _transformTerm((Distinct)and, trace, variables);

+    } else if (and instanceof Equals) {

+      return _transformTerm((Equals)and, trace, variables);

+    } else if (and instanceof Exists) {

+      return _transformTerm((Exists)and, trace, variables);

+    } else if (and instanceof Forall) {

+      return _transformTerm((Forall)and, trace, variables);

+    } else if (and instanceof Iff) {

+      return _transformTerm((Iff)and, trace, variables);

+    } else if (and instanceof Impl) {

+      return _transformTerm((Impl)and, trace, variables);

+    } else if (and instanceof IntLiteral) {

+      return _transformTerm((IntLiteral)and, trace, variables);

+    } else if (and instanceof Not) {

+      return _transformTerm((Not)and, trace, variables);

+    } else if (and instanceof Or) {

+      return _transformTerm((Or)and, trace, variables);

+    } else if (and instanceof RealLiteral) {

+      return _transformTerm((RealLiteral)and, trace, variables);

+    } else if (and instanceof InstanceOf) {

+      return _transformTerm((InstanceOf)and, trace, variables);

+    } else if (and instanceof SymbolicValue) {

+      return _transformTerm((SymbolicValue)and, trace, variables);

+    } else {

+      throw new IllegalArgumentException("Unhandled parameter types: " +

+        Arrays.<Object>asList(and, trace, variables).toString());

+    }

+  }

+  

+  protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    if (constant instanceof ConstantDeclaration) {

+      return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof ConstantDefinition) {

+      return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof FunctionDeclaration) {

+      return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof FunctionDefinition) {

+      return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof DefinedElement) {

+      return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof Relation) {

+      return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables);

+    } else if (constant instanceof Variable) {

+      return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables);

+    } else {

+      throw new IllegalArgumentException("Unhandled parameter types: " +

+        Arrays.<Object>asList(constant, parameterSubstitutions, trace, variables).toString());

+    }

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() {

+    return this.constantMapper;

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() {

+    return this.containmentMapper;

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() {

+    return this.relationMapper;

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() {

+    return this.scopeMapper;

+  }

+  

+  @Pure

+  public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() {

+    return this.typeMapper;

+  }

+}

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
new file mode 100644
index 00000000..24df5fcd
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -0,0 +1,51 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

+import ca.mcgill.ecse.dslreasoner.vampireLanguage.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.List;

+import java.util.Map;

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapperTrace {

+  public VampireModel specification;

+  

+  public VLSFofFormula logicLanguageBody;

+  

+  public VLSTerm formula;

+  

+  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 final List<VLSConstant> uniqueInstances = CollectionLiterals.<VLSConstant>newArrayList();

+  

+  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_ConstantMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java
new file mode 100644
index 00000000..e5f42e73
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java
@@ -0,0 +1,34 @@
+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.VampireLanguageFactory;

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_ConstantMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_ConstantMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  protected Object _transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) {

+    return null;

+  }

+  

+  protected Object transformConstantDefinitionSpecification(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) {

+    return null;

+  }

+  

+  protected Object transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) {

+    return _transformConstant(constant, trace);

+  }

+}

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_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
new file mode 100644
index 00000000..d5745333
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -0,0 +1,260 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

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

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

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

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

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

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

+import java.util.ArrayList;

+import java.util.Arrays;

+import java.util.Collection;

+import java.util.HashMap;

+import java.util.List;

+import java.util.Map;

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

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

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

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

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

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

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

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

+    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("r", nameArray[0], nameArray[2]));

+            for (final VLSVariable v_1 : relVar2VLS) {

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

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

+              _terms.add(_duplicate_1);

+            }

+          };

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

+          trace.rel2Predicate.put(r, rel);

+          it_2.setLeft(this.support.duplicate(rel));

+          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 = reldef.getVariables();

+    for (final Variable variable : _variables) {

+      {

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

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

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

+        };

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

+        relationVar2VLS.put(variable, v);

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

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

+          TypeReference _range = variable.getRange();

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

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

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

+          _terms.add(_duplicate);

+        };

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

+        relationVar2TypeDecComply.put(variable, varTypeComply);

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

+      }

+    }

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

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

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

+      int _length = nameArray.length;

+      int _minus = (_length - 2);

+      int _length_1 = nameArray.length;

+      int _minus_1 = (_length_1 - 1);

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

+        nameArray[_minus_1]));

+      it.setFofRole("axiom");

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

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

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

+        for (final Variable variable_1 : _variables_1) {

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

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

+          _variables_2.add(_duplicate);

+        }

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

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

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

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

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

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

+            for (final Variable variable_2 : _variables_3) {

+              {

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

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

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

+                };

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

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

+                _terms.add(v);

+              }

+            }

+          };

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

+          it_2.setLeft(_doubleArrow);

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

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

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

+        };

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

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

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

+      int _length = nameArray.length;

+      int _minus = (_length - 2);

+      int _length_1 = nameArray.length;

+      int _minus_1 = (_length_1 - 1);

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

+        nameArray[_minus_1]));

+      it.setFofRole("axiom");

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

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

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

+        for (final Variable variable_1 : _variables_1) {

+          {

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

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

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

+            };

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

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

+            _variables_2.add(v);

+          }

+        }

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

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

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

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

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

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

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

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

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

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

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

+              for (final Variable variable_2 : _variables_2) {

+                {

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

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

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

+                  };

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

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

+                  _terms.add(v);

+                }

+              }

+            };

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

+            it_3.setLeft(_doubleArrow);

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

+          };

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

+          it_2.setRight(_doubleArrow);

+        };

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

+        it_1.setOperand(_doubleArrow);

+      };

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

+      it.setFofFormula(_doubleArrow);

+    };

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

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

+    _formulas.add(comply);

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

+    _formulas_1.add(res);

+  }

+  

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

+    if (r instanceof RelationDeclaration) {

+      _transformRelation((RelationDeclaration)r, trace);

+      return;

+    } else if (r instanceof RelationDefinition) {

+      _transformRelation((RelationDefinition)r, trace);

+      return;

+    } else {

+      throw new IllegalArgumentException("Unhandled parameter types: " +

+        Arrays.<Object>asList(r, trace).toString());

+    }

+  }

+}

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
new file mode 100644
index 00000000..d2a6bff2
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -0,0 +1,215 @@
+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;

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

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

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

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

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

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

+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;

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

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

+import java.util.ArrayList;

+import java.util.HashMap;

+import java.util.Map;

+import java.util.Set;

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

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

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

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

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_ScopeMapper {

+  @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_ScopeMapper(final Logic2VampireLanguageMapper base) {

+    this.base = base;

+  }

+  

+  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<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(((ArrayList) trace.uniqueInstances), trace, false, null);

+    }

+    int i_1 = 1;

+    int minNum = (-1);

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

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

+    for (final Type t : _keySet) {

+      {

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

+        if ((minNum != 0)) {

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

+        }

+      }

+    }

+    Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet();

+    for (final Type t_1 : _keySet_1) {

+      {

+        Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType);

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

+        Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints);

+        if ((minNum != 0)) {

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

+        }

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

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

+        }

+      }

+    }

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

+    boolean _notEquals = (_length != 0);

+    if (_notEquals) {

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

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

+        it.setName("typeUniqueness");

+        it.setFofRole("axiom");

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

+      };

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

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

+      _formulas.add(uniqueness);

+    }

+  }

+  

+  protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) {

+    if (clear) {

+      list.clear();

+    }

+    for (int i = startInd; (i < endInd); i++) {

+      {

+        final int num = (i + 1);

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

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

+          it.setName(("o" + Integer.valueOf(num)));

+        };

+        final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);

+        if (addToTrace) {

+          trace.uniqueInstances.add(cst);

+        }

+        list.add(cst);

+      }

+    }

+  }

+  

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

+    String nm = "";

+    VLSTerm tm = null;

+    if ((type == null)) {

+      nm = "object";

+      tm = this.support.topLevelTypeFunc();

+    } else {

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

+      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 VLSTerm term = tm;

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

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

+      String _xifexpression = null;

+      if (minimum) {

+        _xifexpression = "min";

+      } else {

+        _xifexpression = "max";

+      }

+      it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name));

+      it.setFofRole("axiom");

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

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

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

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

+        _variables.add(_duplicate);

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

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

+          if (minimum) {

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

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

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

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

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

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

+                };

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

+            };

+            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_5 = (VLSTerm i) -> {

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

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

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

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

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

+                };

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

+            };

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

+          }

+        };

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

+        it_1.setOperand(_doubleArrow_1);

+      };

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

+      it.setFofFormula(_doubleArrow_1);

+    };

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

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

+    _formulas.add(cstDec);

+  }

+  

+  public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {

+    _transformScope(config, trace);

+    return;

+  }

+}

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
new file mode 100644
index 00000000..119d01f1
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
@@ -0,0 +1,383 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

+

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+import com.google.common.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 hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

+import java.util.ArrayList;

+import java.util.Collection;

+import java.util.HashMap;

+import java.util.List;

+import java.util.Map;

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

+import org.eclipse.xtend2.lib.StringConcatenation;

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

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

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

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

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

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

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_Support {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  protected String toIDMultiple(final String... ids) {

+    final Function1<String, String> _function = (String it) -> {

+      return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(it.split("\\s+"))), "_");

+    };

+    return IterableExtensions.join(ListExtensions.<String, String>map(((List<String>)Conversions.doWrapArray(ids)), _function), "_");

+  }

+  

+  protected String toID(final String ids) {

+    return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_");

+  }

+  

+  protected VLSVariable duplicate(final VLSVariable term) {

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

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

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

+    };

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

+  }

+  

+  protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) {

+    VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();

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

+      it.setFunctor(term.getFunctor());

+    };

+    return ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function);

+  }

+  

+  protected VLSConstant duplicate(final VLSConstant term) {

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

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

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

+    };

+    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _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 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) -> {

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

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

+      VLSFunctionAsTerm _duplicate = this.duplicate(v);

+      _terms.add(_duplicate);

+    };

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

+  }

+  

+  protected VLSConstant toConstant(final VLSFunctionAsTerm term) {

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

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

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

+    };

+    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);

+  }

+  

+  protected VLSFunction topLevelTypeFunc() {

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

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

+      it.setConstant("object");

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

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

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

+        it_1.setName("A");

+      };

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

+      _terms.add(_doubleArrow);

+    };

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

+      it.setConstant("object");

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

+      VLSFunctionAsTerm _duplicate = this.duplicate(v);

+      _terms.add(_duplicate);

+    };

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

+  }

+  

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

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

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

+    for (final VLSConstant t1 : _subList) {

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

+      for (final VLSConstant t2 : _subList_1) {

+        {

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

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

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

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

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

+            };

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

+            it.setLeft(_doubleArrow);

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

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

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

+            };

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

+            it.setRight(_doubleArrow_1);

+          };

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

+          eqs.add(eq);

+        }

+      }

+    }

+    return this.unfoldAnd(eqs);

+  }

+  

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

+    int _size = operands.size();

+    boolean _equals = (_size == 1);

+    if (_equals) {

+      return IterableExtensions.head(operands);

+    } else {

+      int _size_1 = operands.size();

+      boolean _greaterThan = (_size_1 > 1);

+      if (_greaterThan) {

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

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

+          it.setLeft(IterableExtensions.head(operands));

+          it.setRight(this.unfoldAnd(operands.subList(1, operands.size())));

+        };

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

+      } else {

+        StringConcatenation _builder = new StringConcatenation();

+        _builder.append("Logic operator with 0 operands!");

+        throw new UnsupportedOperationException(_builder.toString());

+      }

+    }

+  }

+  

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

+    int _size = operands.size();

+    boolean _equals = (_size == 1);

+    if (_equals) {

+      return IterableExtensions.head(operands);

+    } else {

+      int _size_1 = operands.size();

+      boolean _greaterThan = (_size_1 > 1);

+      if (_greaterThan) {

+        VLSOr _createVLSOr = this.factory.createVLSOr();

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

+          it.setLeft(IterableExtensions.head(operands));

+          it.setRight(this.unfoldOr(operands.subList(1, operands.size())));

+        };

+        return ObjectExtensions.<VLSOr>operator_doubleArrow(_createVLSOr, _function);

+      } else {

+        StringConcatenation _builder = new StringConcatenation();

+        _builder.append("Logic operator with 0 operands!");

+        throw new UnsupportedOperationException(_builder.toString());

+      }

+    }

+  }

+  

+  protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList<Term> operands, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {

+    int _size = operands.size();

+    boolean _equals = (_size == 1);

+    if (_equals) {

+      return m.transformTerm(IterableExtensions.<Term>head(operands), trace, variables);

+    } else {

+      int _size_1 = operands.size();

+      boolean _greaterThan = (_size_1 > 1);

+      if (_greaterThan) {

+        int _size_2 = operands.size();

+        int _size_3 = operands.size();

+        int _multiply = (_size_2 * _size_3);

+        int _divide = (_multiply / 2);

+        final ArrayList<VLSTerm> notEquals = new ArrayList<VLSTerm>(_divide);

+        int _size_4 = operands.size();

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

+        for (final Integer i : _doubleDotLessThan) {

+          int _size_5 = operands.size();

+          ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true);

+          for (final Integer j : _doubleDotLessThan_1) {

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

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

+              it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables));

+              it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables));

+            };

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

+            notEquals.add(_doubleArrow);

+          }

+        }

+        return this.unfoldAnd(notEquals);

+      } else {

+        StringConcatenation _builder = new StringConcatenation();

+        _builder.append("Logic operator with 0 operands!");

+        throw new UnsupportedOperationException(_builder.toString());

+      }

+    }

+  }

+  

+  /**

+   * def protected  String toID(List<String> ids) {

+   *    ids.map[it.split("\\s+").join("'")].join("'")

+   * }

+   */

+  protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables, final boolean isUniversal) {

+    VLSTerm _xblockexpression = null;

+    {

+      final Function1<Variable, VLSVariable> _function = (Variable v) -> {

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

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

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

+        };

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

+      };

+      final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function);

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

+      EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables();

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

+          typedefs.add(eq);

+        }

+      }

+      VLSTerm _xifexpression = null;

+      if (isUniversal) {

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

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

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

+          Collection<VLSVariable> _values = variableMap.values();

+          Iterables.<VLSVariable>addAll(_variables, _values);

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

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

+            it_1.setLeft(this.unfoldAnd(typedefs));

+            it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));

+          };

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

+          it.setOperand(_doubleArrow);

+        };

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

+      } else {

+        VLSExistentialQuantifier _xblockexpression_1 = null;

+        {

+          typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap)));

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

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

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

+            Collection<VLSVariable> _values = variableMap.values();

+            Iterables.<VLSVariable>addAll(_variables, _values);

+            it.setOperand(this.unfoldAnd(typedefs));

+          };

+          _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2);

+        }

+        _xifexpression = _xblockexpression_1;

+      }

+      _xblockexpression = _xifexpression;

+    }

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

+      it.putAll(map2);

+    };

+    return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function);

+  }

+}

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
new file mode 100644
index 00000000..ec759ebf
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -0,0 +1,281 @@
+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;

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

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

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

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

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

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

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

+import 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.TypeDefinition;

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

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

+import java.util.ArrayList;

+import java.util.Collection;

+import java.util.List;

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

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

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

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

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

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

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

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

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_TypeMapper {

+  @Extension

+  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;

+  

+  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();

+  

+  private final Logic2VampireLanguageMapper base;

+  

+  public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) {

+    LogicproblemPackage.eINSTANCE.getClass();

+    this.base = base;

+  }

+  

+  protected boolean transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

+    boolean _xblockexpression = false;

+    {

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

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

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

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

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

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

+        }

+      }

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

+      for (final TypeDefinition type_1 : _filter) {

+        {

+          final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();

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

+          for (final DefinedElement e : _elements) {

+            {

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

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

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

+                int _length = splitName.length;

+                boolean _greaterThan = (_length > 2);

+                if (_greaterThan) {

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

+                } else {

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

+                }

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

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

+                _terms.add(_duplicate);

+              };

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

+              trace.element2Predicate.put(e, 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();

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

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

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

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

+              _variables.add(_duplicate);

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

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

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

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

+            };

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

+            it.setFofFormula(_doubleArrow);

+          };

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

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

+          _formulas.add(res);

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

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

+                it.setFunctor(("eo" + Integer.valueOf(num)));

+              };

+              final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2);

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

+              trace.uniqueInstances.add(cst);

+              final int index = i;

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

+                  };

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

+            }

+          }

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

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

+            } else {

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

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

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

+              };

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

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

+            }

+          }

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

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

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

+          trace.type2PossibleNot.clear();

+        }

+      }

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

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

+        it.setName("inheritanceHierarchyHandler");

+        it.setFofRole("axiom");

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

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

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

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

+          _variables.add(_duplicate);

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

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

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

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

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

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

+          };

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

+          it_1.setOperand(_doubleArrow);

+        };

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

+        it.setFofFormula(_doubleArrow);

+      };

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

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

+      _xblockexpression = _formulas.add(hierarch);

+    }

+    return _xblockexpression;

+  }

+  

+  protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {

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

+  }

+  

+  protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {

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

+  }

+  

+  protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) {

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

+  }

+  

+  protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {

+    VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();

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

+      String _name = referred.getName();

+      String _plus = ("\"a" + _name);

+      String _plus_1 = (_plus + "\"");

+      it.setValue(_plus_1);

+    };

+    return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function);

+  }

+  

+  protected void getTypeInterpreter() {

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

+  }

+}

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

+

+@SuppressWarnings("all")

+public interface Logic2VampireLanguageMapper_TypeMapperTrace {

+}

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

+

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

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

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

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

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

+import java.util.HashMap;

+import java.util.Map;

+

+@SuppressWarnings("all")

+public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_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>();

+}

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

+

+@SuppressWarnings("all")

+public class Vampire2LogicMapper {

+}

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

+

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

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

+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;

+

+@SuppressWarnings("all")

+public class VampireHandler {

+  public Object callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration, final String vampireCode) {

+    return null;

+  }

+}

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

+

+@SuppressWarnings("all")

+public interface VampireModelInterpretation_TypeInterpretation {

+}

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

+

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

+

+@SuppressWarnings("all")

+public class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation {

+}

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

+

+import org.eclipse.xtend.lib.annotations.Data;

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

+import org.eclipse.xtext.xbase.lib.util.ToStringBuilder;

+

+@Data

+@SuppressWarnings("all")

+public class VampireSolutionModel {

+  @Override

+  @Pure

+  public int hashCode() {

+    return 1;

+  }

+  

+  @Override

+  @Pure

+  public boolean equals(final Object obj) {

+    if (this == obj)

+      return true;

+    if (obj == null)

+      return false;

+    if (getClass() != obj.getClass())

+      return false;

+    return true;

+  }

+  

+  @Override

+  @Pure

+  public String toString() {

+    ToStringBuilder b = new ToStringBuilder(this);

+    return b.toString();

+  }

+}

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

+

+import java.util.List;

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

+

+@SuppressWarnings("all")

+public class VampireSolverException extends Exception {

+  public VampireSolverException(final String s) {

+    super(s);

+  }

+  

+  public VampireSolverException(final String s, final Exception e) {

+    super(s, e);

+  }

+  

+  public VampireSolverException(final String s, final List<String> errors, final Exception e) {

+    super(((s + "\n") + IterableExtensions.join(errors, "\n")), e);

+  }

+}