78 files changed, 65 insertions, 3261 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
deleted file mode 100644
index 8e73c63a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
deleted file mode 100644
index a5248945..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.gitignore
deleted file mode 100644
index 074a5969..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.gitignore
+++ /dev/null
@@ -1,6 +0,0 @@
-/.VampireLanguageIdeModule.java._trace
-/.VampireLanguageIdeSetup.java._trace
-/.VampireLanguageIdeModule.xtendbin
-/.VampireLanguageIdeSetup.xtendbin
-/VampireLanguageIdeModule.java
-/VampireLanguageIdeSetup.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/VampireLanguageIdeModule.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/VampireLanguageIdeModule.java
deleted file mode 100644
index 788815c4..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/VampireLanguageIdeModule.java
+++ /dev/null
@@ -1,13 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ide;
-import ca.mcgill.ecse.dslreasoner.ide.AbstractVampireLanguageIdeModule;
-/**
- * Use this class to register ide components.
- */
-@SuppressWarnings("all")
-public class VampireLanguageIdeModule extends AbstractVampireLanguageIdeModule {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/VampireLanguageIdeSetup.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/VampireLanguageIdeSetup.java
deleted file mode 100644
index 05decf8c..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/VampireLanguageIdeSetup.java
+++ /dev/null
@@ -1,24 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ide;
-import ca.mcgill.ecse.dslreasoner.VampireLanguageRuntimeModule;
-import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup;
-import ca.mcgill.ecse.dslreasoner.ide.VampireLanguageIdeModule;
-import com.google.inject.Guice;
-import com.google.inject.Injector;
-import org.eclipse.xtext.util.Modules2;
-/**
- * Initialization support for running Xtext languages as language servers.
- */
-@SuppressWarnings("all")
-public class VampireLanguageIdeSetup extends VampireLanguageStandaloneSetup {
-  @Override
-  public Injector createInjector() {
-    VampireLanguageRuntimeModule _vampireLanguageRuntimeModule = new VampireLanguageRuntimeModule();
-    VampireLanguageIdeModule _vampireLanguageIdeModule = new VampireLanguageIdeModule();
-    return Guice.createInjector(Modules2.mixin(_vampireLanguageRuntimeModule, _vampireLanguageIdeModule));
-  }
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.VampireLanguageParsingTest.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.VampireLanguageParsingTest.xtendbin
deleted file mode 100644
index e9f8c8b6..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.VampireLanguageParsingTest.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.gitignore
deleted file mode 100644
index 87f7264b..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageParsingTest.java._trace
-/.VampireLanguageParsingTest.xtendbin
-/VampireLanguageParsingTest.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.java
deleted file mode 100644
index 3bce3488..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.java
+++ /dev/null
@@ -1,38 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.tests;
-import ca.mcgill.ecse.dslreasoner.tests.VampireLanguageInjectorProvider;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
-import com.google.inject.Inject;
-import org.eclipse.xtend2.lib.StringConcatenation;
-import org.eclipse.xtext.testing.InjectWith;
-import org.eclipse.xtext.testing.XtextRunner;
-import org.eclipse.xtext.testing.util.ParseHelper;
-import org.eclipse.xtext.xbase.lib.Exceptions;
-import org.junit.Assert;
-import org.junit.Test;
-import org.junit.runner.RunWith;
-@RunWith(XtextRunner.class)
-@InjectWith(VampireLanguageInjectorProvider.class)
-@SuppressWarnings("all")
-public class VampireLanguageParsingTest {
-  @Inject
-  private ParseHelper<VampireModel> parseHelper;
-  
-  @Test
-  public void loadModel() {
-    try {
-      StringConcatenation _builder = new StringConcatenation();
-      _builder.append("Hello Xtext!");
-      _builder.newLine();
-      final VampireModel result = this.parseHelper.parse(_builder);
-      Assert.assertNotNull(result);
-      Assert.assertTrue(result.eResource().getErrors().isEmpty());
-    } catch (Throwable _e) {
-      throw Exceptions.sneakyThrow(_e);
-    }
-  }
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
deleted file mode 100644
index 20e0c17a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.gitignore
deleted file mode 100644
index 90c31edb..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageUiModule.java._trace
-/.VampireLanguageUiModule.xtendbin
-/VampireLanguageUiModule.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/VampireLanguageUiModule.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/VampireLanguageUiModule.java
deleted file mode 100644
index 96cac653..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/VampireLanguageUiModule.java
+++ /dev/null
@@ -1,19 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ui;
-import ca.mcgill.ecse.dslreasoner.ui.AbstractVampireLanguageUiModule;
-import org.eclipse.ui.plugin.AbstractUIPlugin;
-import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor;
-/**
- * Use this class to register components to be used within the Eclipse IDE.
- */
-@FinalFieldsConstructor
-@SuppressWarnings("all")
-public class VampireLanguageUiModule extends AbstractVampireLanguageUiModule {
-  public VampireLanguageUiModule(final AbstractUIPlugin plugin) {
-    super(plugin);
-  }
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
deleted file mode 100644
index f3d2dece..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.gitignore
deleted file mode 100644
index 47e411f4..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageProposalProvider.java._trace
-/.VampireLanguageProposalProvider.xtendbin
-/VampireLanguageProposalProvider.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/VampireLanguageProposalProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/VampireLanguageProposalProvider.java
deleted file mode 100644
index ca5ef1f5..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/VampireLanguageProposalProvider.java
+++ /dev/null
@@ -1,14 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ui.contentassist;
-import ca.mcgill.ecse.dslreasoner.ui.contentassist.AbstractVampireLanguageProposalProvider;
-/**
- * See https://www.eclipse.org/Xtext/documentation/304_ide_concepts.html#content-assist
- * on how to customize the content assistant.
- */
-@SuppressWarnings("all")
-public class VampireLanguageProposalProvider extends AbstractVampireLanguageProposalProvider {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
deleted file mode 100644
index 1d0354a7..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
deleted file mode 100644
index c64b5e2f..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.gitignore
deleted file mode 100644
index 8f778c6c..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.gitignore
+++ /dev/null
@@ -1,6 +0,0 @@
-/.VampireLanguageDescriptionLabelProvider.java._trace
-/.VampireLanguageLabelProvider.java._trace
-/.VampireLanguageDescriptionLabelProvider.xtendbin
-/.VampireLanguageLabelProvider.xtendbin
-/VampireLanguageDescriptionLabelProvider.java
-/VampireLanguageLabelProvider.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/VampireLanguageDescriptionLabelProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/VampireLanguageDescriptionLabelProvider.java
deleted file mode 100644
index 1a6a3a2a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/VampireLanguageDescriptionLabelProvider.java
+++ /dev/null
@@ -1,15 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ui.labeling;
-import org.eclipse.xtext.ui.label.DefaultDescriptionLabelProvider;
-/**
- * Provides labels for IEObjectDescriptions and IResourceDescriptions.
- * 
- * See https://www.eclipse.org/Xtext/documentation/304_ide_concepts.html#label-provider
- */
-@SuppressWarnings("all")
-public class VampireLanguageDescriptionLabelProvider extends DefaultDescriptionLabelProvider {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/VampireLanguageLabelProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/VampireLanguageLabelProvider.java
deleted file mode 100644
index 53f93e82..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/VampireLanguageLabelProvider.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ui.labeling;
-import com.google.inject.Inject;
-import org.eclipse.emf.edit.ui.provider.AdapterFactoryLabelProvider;
-import org.eclipse.xtext.ui.label.DefaultEObjectLabelProvider;
-/**
- * Provides labels for EObjects.
- * 
- * See https://www.eclipse.org/Xtext/documentation/304_ide_concepts.html#label-provider
- */
-@SuppressWarnings("all")
-public class VampireLanguageLabelProvider extends DefaultEObjectLabelProvider {
-  @Inject
-  public VampireLanguageLabelProvider(final AdapterFactoryLabelProvider delegate) {
-    super(delegate);
-  }
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
deleted file mode 100644
index ef4b984c..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.gitignore
deleted file mode 100644
index 7162ffad..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageOutlineTreeProvider.java._trace
-/.VampireLanguageOutlineTreeProvider.xtendbin
-/VampireLanguageOutlineTreeProvider.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/VampireLanguageOutlineTreeProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/VampireLanguageOutlineTreeProvider.java
deleted file mode 100644
index 45cb952e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/VampireLanguageOutlineTreeProvider.java
+++ /dev/null
@@ -1,15 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ui.outline;
-import org.eclipse.xtext.ui.editor.outline.impl.DefaultOutlineTreeProvider;
-/**
- * Customization of the default outline structure.
- * 
- * See https://www.eclipse.org/Xtext/documentation/310_eclipse_support.html#outline
- */
-@SuppressWarnings("all")
-public class VampireLanguageOutlineTreeProvider extends DefaultOutlineTreeProvider {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
deleted file mode 100644
index 38907aa5..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.gitignore
deleted file mode 100644
index b439e483..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageQuickfixProvider.java._trace
-/.VampireLanguageQuickfixProvider.xtendbin
-/VampireLanguageQuickfixProvider.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/VampireLanguageQuickfixProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/VampireLanguageQuickfixProvider.java
deleted file mode 100644
index 8b69829c..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/VampireLanguageQuickfixProvider.java
+++ /dev/null
@@ -1,15 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.ui.quickfix;
-import org.eclipse.xtext.ui.editor.quickfix.DefaultQuickfixProvider;
-/**
- * Custom quickfixes.
- * 
- * See https://www.eclipse.org/Xtext/documentation/310_eclipse_support.html#quick-fixes
- */
-@SuppressWarnings("all")
-public class VampireLanguageQuickfixProvider extends DefaultQuickfixProvider {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
deleted file mode 100644
index d1d2ff77..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
deleted file mode 100644
index 27afa8ba..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.gitignore
deleted file mode 100644
index 87793e06..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.gitignore
+++ /dev/null
@@ -1,6 +0,0 @@
-/.VampireLanguageRuntimeModule.java._trace
-/.VampireLanguageStandaloneSetup.java._trace
-/.VampireLanguageRuntimeModule.xtendbin
-/.VampireLanguageStandaloneSetup.xtendbin
-/VampireLanguageRuntimeModule.java
-/VampireLanguageStandaloneSetup.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.java
deleted file mode 100644
index 4592f574..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.java
+++ /dev/null
@@ -1,13 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner;
-import ca.mcgill.ecse.dslreasoner.AbstractVampireLanguageRuntimeModule;
-/**
- * Use this class to register components to be used at runtime / without the Equinox extension registry.
- */
-@SuppressWarnings("all")
-public class VampireLanguageRuntimeModule extends AbstractVampireLanguageRuntimeModule {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.java
deleted file mode 100644
index e33cd1fe..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.java
+++ /dev/null
@@ -1,16 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner;
-import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
-/**
- * Initialization support for running Xtext languages without Equinox extension registry.
- */
-@SuppressWarnings("all")
-public class VampireLanguageStandaloneSetup extends VampireLanguageStandaloneSetupGenerated {
-  public static void doSetup() {
-    new VampireLanguageStandaloneSetup().createInjectorAndDoEMFRegistration();
-  }
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
deleted file mode 100644
index d1a3a13d..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.gitignore
deleted file mode 100644
index 2e4f4654..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageFormatter.java._trace
-/.VampireLanguageFormatter.xtendbin
-/VampireLanguageFormatter.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java
deleted file mode 100644
index 48b973e7..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java
+++ /dev/null
@@ -1,79 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.formatting2;
-import ca.mcgill.ecse.dslreasoner.services.VampireLanguageGrammarAccess;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
-import com.google.inject.Inject;
-import java.util.Arrays;
-import org.eclipse.emf.common.util.EList;
-import org.eclipse.emf.ecore.EObject;
-import org.eclipse.xtext.formatting2.AbstractFormatter2;
-import org.eclipse.xtext.formatting2.IFormattableDocument;
-import org.eclipse.xtext.formatting2.IHiddenRegionFormatter;
-import org.eclipse.xtext.resource.XtextResource;
-import org.eclipse.xtext.xbase.lib.Extension;
-import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
-@SuppressWarnings("all")
-public class VampireLanguageFormatter extends AbstractFormatter2 {
-  @Inject
-  @Extension
-  private VampireLanguageGrammarAccess _vampireLanguageGrammarAccess;
-  
-  protected void _format(final VampireModel vampireModel, @Extension final IFormattableDocument document) {
-    EList<VLSComment> _comments = vampireModel.getComments();
-    for (final VLSComment vLSComment : _comments) {
-      document.<VLSComment>format(vLSComment);
-    }
-    EList<VLSFofFormula> _formulas = vampireModel.getFormulas();
-    for (final VLSFofFormula vLSFofFormula : _formulas) {
-      document.<VLSFofFormula>format(vLSFofFormula);
-    }
-  }
-  
-  protected void _format(final VLSFofFormula formula, @Extension final IFormattableDocument document) {
-    final Procedure1<IHiddenRegionFormatter> _function = (IHiddenRegionFormatter it) -> {
-      it.newLine();
-    };
-    document.<VLSFofFormula>append(formula, _function);
-  }
-  
-  protected void _format(final VLSComment comment, @Extension final IFormattableDocument document) {
-    final Procedure1<IHiddenRegionFormatter> _function = (IHiddenRegionFormatter it) -> {
-      it.newLine();
-    };
-    document.<VLSComment>append(comment, _function);
-  }
-  
-  public void format(final Object comment, final IFormattableDocument document) {
-    if (comment instanceof XtextResource) {
-      _format((XtextResource)comment, document);
-      return;
-    } else if (comment instanceof VLSComment) {
-      _format((VLSComment)comment, document);
-      return;
-    } else if (comment instanceof VLSFofFormula) {
-      _format((VLSFofFormula)comment, document);
-      return;
-    } else if (comment instanceof VampireModel) {
-      _format((VampireModel)comment, document);
-      return;
-    } else if (comment instanceof EObject) {
-      _format((EObject)comment, document);
-      return;
-    } else if (comment == null) {
-      _format((Void)null, document);
-      return;
-    } else if (comment != null) {
-      _format(comment, document);
-      return;
-    } else {
-      throw new IllegalArgumentException("Unhandled parameter types: " +
-        Arrays.<Object>asList(comment, document).toString());
-    }
-  }
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
deleted file mode 100644
index 6d2a9063..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.gitignore
deleted file mode 100644
index b3ec8dd5..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageGenerator.java._trace
-/.VampireLanguageGenerator.xtendbin
-/VampireLanguageGenerator.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.java
deleted file mode 100644
index 038c7c4f..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.generator;
-import org.eclipse.emf.ecore.resource.Resource;
-import org.eclipse.xtext.generator.AbstractGenerator;
-import org.eclipse.xtext.generator.IFileSystemAccess2;
-import org.eclipse.xtext.generator.IGeneratorContext;
-/**
- * Generates code from your model files on save.
- * 
- * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#code-generation
- */
-@SuppressWarnings("all")
-public class VampireLanguageGenerator extends AbstractGenerator {
-  @Override
-  public void doGenerate(final Resource resource, final IFileSystemAccess2 fsa, final IGeneratorContext context) {
-  }
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
deleted file mode 100644
index a9942913..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.gitignore
deleted file mode 100644
index ea4b064e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageScopeProvider.java._trace
-/.VampireLanguageScopeProvider.xtendbin
-/VampireLanguageScopeProvider.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.java
deleted file mode 100644
index 2ea3ee1e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.java
+++ /dev/null
@@ -1,16 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.scoping;
-import ca.mcgill.ecse.dslreasoner.scoping.AbstractVampireLanguageScopeProvider;
-/**
- * This class contains custom scoping description.
- * 
- * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping
- * on how and when to use it.
- */
-@SuppressWarnings("all")
-public class VampireLanguageScopeProvider extends AbstractVampireLanguageScopeProvider {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
deleted file mode 100644
index cd467bbd..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
+++ /dev/null
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.gitignore
deleted file mode 100644
index d7fe565a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/.VampireLanguageValidator.java._trace
-/.VampireLanguageValidator.xtendbin
-/VampireLanguageValidator.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.java
deleted file mode 100644
index 9d112239..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.java
+++ /dev/null
@@ -1,15 +0,0 @@
-/**
- * generated by Xtext 2.12.0
- */
-package ca.mcgill.ecse.dslreasoner.validation;
-import ca.mcgill.ecse.dslreasoner.validation.AbstractVampireLanguageValidator;
-/**
- * This class contains custom validation rules.
- * 
- * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#validation
- */
-@SuppressWarnings("all")
-public class VampireLanguageValidator extends AbstractVampireLanguageValidator {
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index 1fda24d9..c3b344eb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -8,7 +8,7 @@ class VampireSolverConfiguration
        public var int contCycleLevel = 0
        public var boolean uniquenessDuplicates = false
        public var int iteration = -1
-        public var BackendSolver solver = BackendSolver::VAMPIRE
+        public var BackendSolver solver = BackendSolver::LOCVAMP
        public var genModel = true
        public var server = false
        //choose needed backend solver
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index 59084843..4b8b10a9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -83,26 +83,27 @@ class VampireSolver extends LogicReasoner {
                                var done = false
                                print(" ")
                                while (!done) {
-                                        print("(x)")
+//                                      print("(x)")
                                        done = false
                                        response = support.sendPost(form)
                                        var responseFound = false
                                        ind = 0
-                                        while (!responseFound) {
+                                        while (!responseFound && ind<response.length) {
                                                var line = response.get(ind)
 //                                              println(line)
                                                if (line.length >= 5 && line.substring(0, 5) == "ERROR") {
                                                        done = false
                                                        responseFound = true
                                                } else {
-                                                        if (line == "</PRE>") {
+                                                        if (line == "</PRE>" && response.get(ind-1) != "<PRE>") {
                                                                done = true
                                                                responseFound = true
                                                        }
                                                }
                                                ind++
                                        }
+                                        if (!done) println("(Server call failed. Trying again...)")
                                }
                                val satRaw = response.get(ind - 3)
                                val modRaw = response.get(ind - 2)
@@ -118,10 +119,35 @@ class VampireSolver extends LogicReasoner {
                                println()
                                println(sat)
                                println(mod)
+                                
+                                return createUndecidableResult => [
+                                        it.statistics = createStatistics => [
+                                                it.transformationTime = transformationTime as int
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satOut"
+                                                        it.value = satOut
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satTime"
+                                                        it.value = satTime
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modOut"
+                                                        it.value = modOut
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modTime"
+                                                        it.value = modTime
+                                                ]
+                                        ]
+                                ]
+                                        
+                                /*
+                                 * TODO
                                return createModelResult => [
                                        it.problem = null
-                                        it.representation += createVampireModel => []
+                                        it.representation += createVampireModel => []//TODO Add something here
                                        it.trace = trace
                                        it.statistics = createStatistics => [
                                                it.transformationTime = transformationTime as int
@@ -144,6 +170,7 @@ class VampireSolver extends LogicReasoner {
                                        ]
                                ]
+                                */
 //                              return newArrayList(line1, line2)
                        } else {
@@ -172,8 +199,31 @@ class VampireSolver extends LogicReasoner {
                                }
                                
                                val realModOut=modOut
- 
                                
+                                return createUndecidableResult => [
+                                        it.statistics = createStatistics => [
+                                                it.transformationTime = transformationTime as int
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satOut"
+                                                        it.value = "-"
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "satTime"
+                                                        it.value = "-"
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modOut"
+                                                        it.value = realModOut
+                                                ]
+                                                it.entries += createStringStatisticEntry => [
+                                                        it.name = "modTime"
+                                                        it.value = (vampSol.solverTime/1000.0).toString
+                                                ]
+                                        ]
+                                ]
+                                
+                                /*
                                return createModelResult => [
                                        it.problem = null
                                        it.representation += createVampireModel => []
@@ -199,6 +249,7 @@ class VampireSolver extends LogicReasoner {
                                        ]
                                ]
+                                */
                        }
                }
 //              return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index 44efd84e..fa334322 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -299,23 +299,23 @@ class Logic2VampireLanguageMapper_Support {
        def getSolverSpecs(BackendSolver solver) {
                switch (solver) {
                        case BackendSolver::CVC4:
-                                return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT")
+                                return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT")//TODO Update
                        case BackendSolver::DARWINFM:
-                                return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s")
+                                return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s")//TODO Update
                        case BackendSolver::EDARWIN:
                                return newArrayList("E-Darwin---1.5",
-                                        "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s")
+                                        "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s")//TODO Update
                        case BackendSolver::GEOIII:
                                return newArrayList("Geo-III---2018C",
-                                        "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s")
+                                        "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s")//TODO Update
                        case BackendSolver::IPROVER:
-                                return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s")
+                                return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s")//TODO Update
                        case BackendSolver::PARADOX:
-                                return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s")
+                                return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s")//TODO Update
                        case BackendSolver::VAMPIRE:
-                                return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s")
+                                return newArrayList("Vampire---SAT-4.5", "vampire --mode casc_sat -t %d %s")
                        case BackendSolver::Z3:
-                                return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s")
+                                return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s")//TODO Update
                }
        }
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
deleted file mode 100644
index e999bce6..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 28154d14..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 70f60102..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore
+++ /dev/null
@@ -1,10 +0,0 @@
-/.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
deleted file mode 100644
index 8ffba2f1..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java
+++ /dev/null
@@ -1,6 +0,0 @@
-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/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
deleted file mode 100644
index eb6007ec..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ /dev/null
@@ -1,275 +0,0 @@
-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.Logic2VampireLanguageMapper_Support;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
-import com.google.common.base.Objects;
-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.LogicresultFactory;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;
-import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
-import java.util.ArrayList;
-import java.util.List;
-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.Exceptions;
-import org.eclipse.xtext.xbase.lib.Extension;
-import org.eclipse.xtext.xbase.lib.Functions.Function1;
-import org.eclipse.xtext.xbase.lib.InputOutput;
-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 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 Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
-  
-  @Extension
-  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;
-  
-  @Extension
-  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
-  
-  @Override
-  public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException {
-    try {
-      final VampireSolverConfiguration vampireConfig = this.asConfig(config);
-      String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + 
-        Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp");
-      final long transformationStart = System.currentTimeMillis();
-      final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);
-      long _currentTimeMillis = System.currentTimeMillis();
-      final long transformationTime = (_currentTimeMillis - transformationStart);
-      final VampireModel vampireProblem = result.getOutput();
-      final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();
-      String fileURI = null;
-      String vampireCode = null;
-      vampireCode = workspace.writeModelToString(vampireProblem, fileName);
-      final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || 
-        (vampireConfig.documentationLevel == DocumentationLevel.FULL));
-      if (writeFile) {
-        fileURI = workspace.writeModel(vampireProblem, fileName).toFileString();
-      }
-      if (vampireConfig.genModel) {
-        if (vampireConfig.server) {
-          final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit);
-          ArrayList<String> response = CollectionLiterals.<String>newArrayList();
-          int ind = 0;
-          boolean done = false;
-          InputOutput.<String>print(" ");
-          while ((!done)) {
-            {
-              InputOutput.<String>print("(x)");
-              done = false;
-              response = this.support.sendPost(form);
-              boolean responseFound = false;
-              ind = 0;
-              while ((!responseFound)) {
-                {
-                  String line = response.get(ind);
-                  if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) {
-                    done = false;
-                    responseFound = true;
-                  } else {
-                    boolean _equals = Objects.equal(line, "</PRE>");
-                    if (_equals) {
-                      done = true;
-                      responseFound = true;
-                    }
-                  }
-                  ind++;
-                }
-              }
-            }
-          }
-          final String satRaw = response.get((ind - 3));
-          final String modRaw = response.get((ind - 2));
-          final ArrayList<String> sat = CollectionLiterals.<String>newArrayList(satRaw.split(" "));
-          final ArrayList<String> mod = CollectionLiterals.<String>newArrayList(modRaw.split(" "));
-          final String satOut = sat.get(1);
-          final String modOut = mod.get(1);
-          final String satTime = sat.get(2);
-          final String modTime = mod.get(2);
-          InputOutput.println();
-          InputOutput.<ArrayList<String>>println(sat);
-          InputOutput.<ArrayList<String>>println(mod);
-          ModelResult _createModelResult = this.resultFactory.createModelResult();
-          final Procedure1<ModelResult> _function = (ModelResult it) -> {
-            it.setProblem(null);
-            EList<Object> _representation = it.getRepresentation();
-            VampireModel _createVampireModel = this.factory.createVampireModel();
-            final Procedure1<VampireModel> _function_1 = (VampireModel it_1) -> {
-            };
-            VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1);
-            _representation.add(_doubleArrow);
-            it.setTrace(it.getTrace());
-            Statistics _createStatistics = this.resultFactory.createStatistics();
-            final Procedure1<Statistics> _function_2 = (Statistics it_1) -> {
-              it_1.setTransformationTime(((int) transformationTime));
-              EList<StatisticEntry> _entries = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_3 = (StringStatisticEntry it_2) -> {
-                it_2.setName("satOut");
-                it_2.setValue(satOut);
-              };
-              StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_3);
-              _entries.add(_doubleArrow_1);
-              EList<StatisticEntry> _entries_1 = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> {
-                it_2.setName("satTime");
-                it_2.setValue(satTime);
-              };
-              StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_4);
-              _entries_1.add(_doubleArrow_2);
-              EList<StatisticEntry> _entries_2 = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {
-                it_2.setName("modOut");
-                it_2.setValue(modOut);
-              };
-              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_5);
-              _entries_2.add(_doubleArrow_3);
-              EList<StatisticEntry> _entries_3 = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {
-                it_2.setName("modTime");
-                it_2.setValue(modTime);
-              };
-              StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_6);
-              _entries_3.add(_doubleArrow_4);
-            };
-            Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_2);
-            it.setStatistics(_doubleArrow_1);
-          };
-          return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);
-        } else {
-          InputOutput.println();
-          final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);
-          String modOut_1 = "no";
-          boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated();
-          if (_isFiniteModelGenerated) {
-            modOut_1 = "FiniteModel";
-          }
-          final String realModOut = modOut_1;
-          ModelResult _createModelResult_1 = this.resultFactory.createModelResult();
-          final Procedure1<ModelResult> _function_1 = (ModelResult it) -> {
-            it.setProblem(null);
-            EList<Object> _representation = it.getRepresentation();
-            VampireModel _createVampireModel = this.factory.createVampireModel();
-            final Procedure1<VampireModel> _function_2 = (VampireModel it_1) -> {
-            };
-            VampireModel _doubleArrow = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_2);
-            _representation.add(_doubleArrow);
-            it.setTrace(it.getTrace());
-            Statistics _createStatistics = this.resultFactory.createStatistics();
-            final Procedure1<Statistics> _function_3 = (Statistics it_1) -> {
-              it_1.setTransformationTime(((int) transformationTime));
-              EList<StatisticEntry> _entries = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_4 = (StringStatisticEntry it_2) -> {
-                it_2.setName("satOut");
-                it_2.setValue("-");
-              };
-              StringStatisticEntry _doubleArrow_1 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry, _function_4);
-              _entries.add(_doubleArrow_1);
-              EList<StatisticEntry> _entries_1 = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_5 = (StringStatisticEntry it_2) -> {
-                it_2.setName("satTime");
-                it_2.setValue("-");
-              };
-              StringStatisticEntry _doubleArrow_2 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_1, _function_5);
-              _entries_1.add(_doubleArrow_2);
-              EList<StatisticEntry> _entries_2 = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_6 = (StringStatisticEntry it_2) -> {
-                it_2.setName("modOut");
-                it_2.setValue(realModOut);
-              };
-              StringStatisticEntry _doubleArrow_3 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_2, _function_6);
-              _entries_2.add(_doubleArrow_3);
-              EList<StatisticEntry> _entries_3 = it_1.getEntries();
-              StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry();
-              final Procedure1<StringStatisticEntry> _function_7 = (StringStatisticEntry it_2) -> {
-                it_2.setName("modTime");
-                long _solverTime = vampSol.getSolverTime();
-                it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString());
-              };
-              StringStatisticEntry _doubleArrow_4 = ObjectExtensions.<StringStatisticEntry>operator_doubleArrow(_createStringStatisticEntry_3, _function_7);
-              _entries_3.add(_doubleArrow_4);
-            };
-            Statistics _doubleArrow_1 = ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function_3);
-            it.setStatistics(_doubleArrow_1);
-          };
-          return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult_1, _function_1);
-        }
-      }
-      return null;
-    } catch (Throwable _e) {
-      throw Exceptions.sneakyThrow(_e);
-    }
-  }
-  
-  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) {
-    List<VampireModelInterpretation> _xblockexpression = null;
-    {
-      final EList<Object> sols = modelResult.getRepresentation();
-      final Function1<Object, VampireModelInterpretation> _function = (Object it) -> {
-        Object _trace = modelResult.getTrace();
-        return new VampireModelInterpretation(
-          ((VampireModel) it), 
-          ((Logic2VampireLanguageMapperTrace) _trace));
-      };
-      _xblockexpression = ListExtensions.<Object, VampireModelInterpretation>map(sols, _function);
-    }
-    return _xblockexpression;
-  }
-}
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
deleted file mode 100644
index c094872e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
+++ /dev/null
@@ -1,19 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
-@SuppressWarnings("all")
-public class VampireSolverConfiguration extends LogicSolverConfiguration {
-  public int contCycleLevel = 0;
-  
-  public boolean uniquenessDuplicates = false;
-  
-  public int iteration = (-1);
-  
-  public BackendSolver solver = BackendSolver.VAMPIRE;
-  
-  public boolean genModel = true;
-  
-  public boolean server = false;
-}
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
deleted file mode 100644
index 18da19a9..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 37c845cd..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index d8c61adc..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 1a86a55f..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 216b3a4b..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 8733e530..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 634dab6a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 28c93f34..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index faef07c1..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 3d96efbf..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index b3756706..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index f75b4eaf..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ /dev/null
Binary files differ
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
deleted file mode 100644
index 8a9aa4bb..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore
+++ /dev/null
@@ -1,42 +0,0 @@
-/.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
deleted file mode 100644
index dc5ec788..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ /dev/null
@@ -1,510 +0,0 @@
-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.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.base.Objects;
-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.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.logiclanguage.impl.RelationDeclarationImpl;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl;
-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.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;
-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);
-    }
-    trace.relationDefinitions = this.collectRelationDefinitions(problem);
-    final Function1<Relation, Boolean> _function_3 = (Relation it) -> {
-      Class<? extends Relation> _class = it.getClass();
-      return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class));
-    };
-    this.toTrace(IterableExtensions.<Relation>filter(problem.getRelations(), _function_3), trace);
-    final Consumer<Relation> _function_4 = (Relation it) -> {
-      Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper();
-      this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper);
-    };
-    problem.getRelations().forEach(_function_4);
-    this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);
-    this.scopeMapper.transformScope(problem.getTypes(), config, trace);
-    trace.constantDefinitions = this.collectConstantDefinitions(problem);
-    final Consumer<ConstantDefinition> _function_5 = (ConstantDefinition it) -> {
-      this.constantMapper.transformConstantDefinitionSpecification(it, trace);
-    };
-    Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5);
-    EList<Assertion> _assertions = problem.getAssertions();
-    for (final Assertion assertion : _assertions) {
-      this.transformAssertion(assertion, trace);
-    }
-    return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace);
-  }
-  
-  public void toTrace(final Iterable<Relation> relations, final Logic2VampireLanguageMapperTrace trace) {
-    final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList();
-    for (final Relation rel : relations) {
-      {
-        final String[] nameArray = rel.getName().split(" ");
-        String relNameVar = "";
-        int _length = nameArray.length;
-        boolean _equals = (_length == 3);
-        if (_equals) {
-          relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
-        } else {
-          relNameVar = rel.getName();
-        }
-        final String relName = relNameVar;
-        final RelationDefinition relDef = ((RelationDefinition) rel);
-        int _length_1 = ((Object[])Conversions.unwrapArray(rel.getParameters(), Object.class)).length;
-        ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length_1, 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);
-            vars.add(v);
-          }
-        }
-        VLSFunction _createVLSFunction = this.factory.createVLSFunction();
-        final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
-          it.setConstant(this.support.toIDMultiple("r", relName));
-          for (final VLSVariable v : vars) {
-            EList<VLSTerm> _terms = it.getTerms();
-            VLSVariable _duplicate = this.support.duplicate(v);
-            _terms.add(_duplicate);
-          }
-        };
-        final VLSFunction relFunc = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
-        trace.relDef2Predicate.put(relDef, relFunc);
-        trace.predicate2RelDef.put(relFunc, relDef);
-      }
-    }
-  }
-  
-  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) -> {
-        String _name = assertion.getName();
-        String _plus = ("assertion_" + _name);
-        it.setName(this.support.toID(_plus));
-        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 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) {
-    final String name = CollectionsUtil.<DefinedElement, String>lookup(referred, trace.definedElement2String);
-    VLSConstant _createVLSConstant = this.factory.createVLSConstant();
-    final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
-      it.setName(name);
-    };
-    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
-  }
-  
-  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) -> {
-      Class<? extends Relation> _class = relation.getClass();
-      boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class);
-      if (_equals) {
-        it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant());
-      } else {
-        it.setConstant(CollectionsUtil.<RelationDefinition, VLSFunction>lookup(((RelationDefinition) relation), trace.relDef2Predicate).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 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
deleted file mode 100644
index 22df456b..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ /dev/null
@@ -1,65 +0,0 @@
-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 Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>();
-  
-  public Object topLvlElementIsInInitialModel = null;
-  
-  public Object topLevelType = null;
-  
-  public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();
-  
-  public final Map<VLSFunction, Type> predicate2Type = new HashMap<VLSFunction, Type>();
-  
-  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 Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>();
-  
-  public Map<RelationDefinition, VLSFunction> relDef2Predicate = new HashMap<RelationDefinition, VLSFunction>();
-  
-  public Map<VLSFunction, RelationDefinition> predicate2RelDef = new HashMap<VLSFunction, RelationDefinition>();
-  
-  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
deleted file mode 100644
index e5f42e73..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java
+++ /dev/null
@@ -1,34 +0,0 @@
-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
deleted file mode 100644
index 2100b92f..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
+++ /dev/null
@@ -1,386 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
-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.Logic2VampireLanguageMapper_Support;
-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.VLSTerm;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;
-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.ComplexTypeReference;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
-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.TypeDefinition;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;
-import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-import org.eclipse.emf.common.util.EList;
-import org.eclipse.xtext.xbase.lib.CollectionLiterals;
-import org.eclipse.xtext.xbase.lib.Conversions;
-import org.eclipse.xtext.xbase.lib.Extension;
-import org.eclipse.xtext.xbase.lib.ObjectExtensions;
-import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
-@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 VampireSolverConfiguration config, 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();
-    final ArrayList<Object> toRemove = CollectionLiterals.<Object>newArrayList();
-    for (final Relation l : relationsList) {
-      {
-        TypeReference _get = l.getParameters().get(1);
-        Type _referred = ((ComplexTypeReference) _get).getReferred();
-        Type pointingTo = ((Type) _referred);
-        containmentListCopy.remove(pointingTo);
-        List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList();
-        this.support.listSubtypes(pointingTo, allSubtypes);
-        for (final Type c : allSubtypes) {
-          containmentListCopy.remove(c);
-        }
-      }
-    }
-    Type topTermVar = containmentListCopy.get(0);
-    for (final Relation l_1 : relationsList) {
-      {
-        TypeReference _get = l_1.getParameters().get(0);
-        Type _referred = ((ComplexTypeReference) _get).getReferred();
-        Type pointingFrom = ((Type) _referred);
-        boolean _contains = containmentListCopy.contains(pointingFrom);
-        if (_contains) {
-          topTermVar = pointingFrom;
-        }
-      }
-    }
-    final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString();
-    final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate));
-    trace.topLevelType = topTermVar;
-    boolean topLvlIsInInitModel = false;
-    String topLvlString = "";
-    ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar);
-    listToCheck.addAll(topTermVar.getSubtypes());
-    for (final Type c : listToCheck) {
-      Class<? extends Type> _class = c.getClass();
-      boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class);
-      if (_equals) {
-        int _length = ((Object[])Conversions.unwrapArray(((TypeDefinition) c).getElements(), Object.class)).length;
-        boolean _greaterThan = (_length > 1);
-        if (_greaterThan) {
-          throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model");
-        }
-        EList<DefinedElement> _elements = ((TypeDefinition) c).getElements();
-        for (final DefinedElement d : _elements) {
-          boolean _containsKey = trace.definedElement2String.containsKey(d);
-          if (_containsKey) {
-            topLvlIsInInitModel = true;
-            topLvlString = CollectionsUtil.<DefinedElement, String>lookup(d, trace.definedElement2String);
-          }
-        }
-      }
-    }
-    trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel);
-    final boolean topInIM = topLvlIsInInitModel;
-    final String topStr = topLvlString;
-    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<VLSTffTerm> _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) -> {
-              String _xifexpression = null;
-              if (topInIM) {
-                _xifexpression = topStr;
-              } else {
-                _xifexpression = "o1";
-              }
-              it_4.setName(_xifexpression);
-            };
-            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);
-    VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();
-    final Procedure1<VLSVariable> _function_3 = (VLSVariable it) -> {
-      it.setName("C");
-    };
-    final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3);
-    final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA);
-    final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>();
-    for (final Relation l_2 : relationsList) {
-      {
-        final VLSFunction rel = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate);
-        TypeReference _get = l_2.getParameters().get(1);
-        Type _referred = ((ComplexTypeReference) _get).getReferred();
-        final Type toType = ((Type) _referred);
-        final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);
-        this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList));
-        ArrayList<Type> subTypes = CollectionLiterals.<Type>newArrayList();
-        this.support.listSubtypes(toType, subTypes);
-        for (final Type c_1 : subTypes) {
-          this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList));
-        }
-        VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
-        final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
-          it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString()));
-          it.setFofRole("axiom");
-          VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
-          final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> {
-            EList<VLSTffTerm> _variables = it_1.getVariables();
-            VLSVariable _duplicate = this.support.duplicate(varA);
-            _variables.add(_duplicate);
-            EList<VLSTffTerm> _variables_1 = it_1.getVariables();
-            VLSVariable _duplicate_1 = this.support.duplicate(varB);
-            _variables_1.add(_duplicate_1);
-            VLSImplies _createVLSImplies = this.factory.createVLSImplies();
-            final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> {
-              it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varA, varB)));
-              VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
-              final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {
-                VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier();
-                final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> {
-                  EList<VLSTffTerm> _variables_2 = it_4.getVariables();
-                  VLSVariable _duplicate_2 = this.support.duplicate(varC);
-                  _variables_2.add(_duplicate_2);
-                  EList<VLSTffTerm> _variables_3 = it_4.getVariables();
-                  VLSVariable _duplicate_3 = this.support.duplicate(varB);
-                  _variables_3.add(_duplicate_3);
-                  it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB)));
-                };
-                VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8);
-                it_3.setOperand(_doubleArrow);
-              };
-              VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_7);
-              it_2.setRight(_doubleArrow);
-            };
-            VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6);
-            it_1.setOperand(_doubleArrow);
-          };
-          VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_5);
-          it.setFofFormula(_doubleArrow);
-        };
-        final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);
-        EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
-        _formulas_1.add(relFormula);
-      }
-    }
-    Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet();
-    for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) {
-      {
-        VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
-        final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
-          it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString()));
-          it.setFofRole("axiom");
-          VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-          final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {
-            EList<VLSTffTerm> _variables = it_1.getVariables();
-            VLSVariable _duplicate = this.support.duplicate(varA);
-            _variables.add(_duplicate);
-            VLSImplies _createVLSImplies = this.factory.createVLSImplies();
-            final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> {
-              it_2.setLeft(this.support.duplicate(e.getKey(), varA));
-              VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
-              final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> {
-                EList<VLSTffTerm> _variables_1 = it_3.getVariables();
-                VLSVariable _duplicate_1 = this.support.duplicate(varB);
-                _variables_1.add(_duplicate_1);
-                int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length;
-                boolean _greaterThan_1 = (_length_1 > 1);
-                if (_greaterThan_1) {
-                  it_3.setOperand(this.makeUnique(e.getValue()));
-                } else {
-                  it_3.setOperand(e.getValue().get(0));
-                }
-              };
-              VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7);
-              it_2.setRight(_doubleArrow);
-            };
-            VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6);
-            it_1.setOperand(_doubleArrow);
-          };
-          VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);
-          it.setFofFormula(_doubleArrow);
-        };
-        final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);
-        EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
-        _formulas_1.add(relFormula);
-      }
-    }
-    final ArrayList<VLSVariable> variables = CollectionLiterals.<VLSVariable>newArrayList();
-    final ArrayList<VLSFunction> disjunctionList = CollectionLiterals.<VLSFunction>newArrayList();
-    final ArrayList<VLSTerm> conjunctionList = CollectionLiterals.<VLSTerm>newArrayList();
-    for (int i = 1; (i <= config.contCycleLevel); i++) {
-      {
-        final int ind = i;
-        VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable();
-        final Procedure1<VLSVariable> _function_4 = (VLSVariable it) -> {
-          String _string = Integer.toString(ind);
-          String _plus = ("V" + _string);
-          it.setName(_plus);
-        };
-        VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_3, _function_4);
-        variables.add(_doubleArrow);
-        for (int j = 0; (j < i); j++) {
-          {
-            for (final Relation l_3 : relationsList) {
-              {
-                final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), 
-                  CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));
-                disjunctionList.add(rel);
-              }
-            }
-            conjunctionList.add(this.support.unfoldOr(disjunctionList));
-            disjunctionList.clear();
-          }
-        }
-        VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
-        final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> {
-          it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind)));
-          it.setFofRole("axiom");
-          VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
-          final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> {
-            VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier();
-            final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> {
-              EList<VLSTffTerm> _variables = it_2.getVariables();
-              List<VLSVariable> _duplicate = this.support.duplicate(variables);
-              Iterables.<VLSTffTerm>addAll(_variables, _duplicate);
-              it_2.setOperand(this.support.unfoldAnd(conjunctionList));
-            };
-            VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7);
-            it_1.setOperand(_doubleArrow_1);
-          };
-          VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_6);
-          it.setFofFormula(_doubleArrow_1);
-        };
-        final VLSFofFormula contCycleForm = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5);
-        EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
-        _formulas_1.add(contCycleForm);
-        conjunctionList.clear();
-      }
-    }
-  }
-  
-  protected VLSTerm makeUnique(final List<VLSFunction> list) {
-    final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList();
-    final List<VLSTerm> uniqueRels = CollectionLiterals.<VLSTerm>newArrayList();
-    for (final VLSFunction t1 : list) {
-      {
-        for (final VLSFunction t2 : list) {
-          boolean _equals = Objects.equal(t1, t2);
-          if (_equals) {
-            final VLSFunction fct = this.support.duplicate(t2);
-            possibleNots.add(fct);
-          } else {
-            final VLSFunction op = this.support.duplicate(t2);
-            VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
-            final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> {
-              it.setOperand(op);
-            };
-            final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function);
-            possibleNots.add(negFct);
-          }
-        }
-        uniqueRels.add(this.support.unfoldAnd(possibleNots));
-        possibleNots.clear();
-      }
-    }
-    return this.support.unfoldOr(uniqueRels);
-  }
-  
-  protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) {
-    Object _xblockexpression = null;
-    {
-      boolean keyInMap = false;
-      VLSFunction existingKey = this.factory.createVLSFunction();
-      Set<VLSFunction> _keySet = type2cont.keySet();
-      for (final VLSFunction k : _keySet) {
-        boolean _equals = k.getConstant().equals(toFunc.getConstant());
-        if (_equals) {
-          keyInMap = true;
-          existingKey = k;
-        }
-      }
-      Object _xifexpression = null;
-      if ((!keyInMap)) {
-        _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel));
-      } else {
-        boolean _xifexpression_1 = false;
-        boolean _contains = type2cont.get(existingKey).contains(rel);
-        boolean _not = (!_contains);
-        if (_not) {
-          _xifexpression_1 = type2cont.get(existingKey).add(rel);
-        }
-        _xifexpression = Boolean.valueOf(_xifexpression_1);
-      }
-      _xblockexpression = _xifexpression;
-    }
-    return _xblockexpression;
-  }
-}
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
deleted file mode 100644
index 4c14e93e..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ /dev/null
@@ -1,205 +0,0 @@
-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.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.VLSTffTerm;
-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.HashMap;
-import java.util.List;
-import java.util.Map;
-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.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 Logic2VampireLanguageMapper mapper) {
-    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);
-      }
-    }
-    final String[] nameArray = r.getName().split(" ");
-    String relNameVar = "";
-    int _length_1 = nameArray.length;
-    boolean _equals = (_length_1 == 3);
-    if (_equals) {
-      relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
-    } else {
-      relNameVar = r.getName();
-    }
-    final String relName = relNameVar;
-    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-    final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
-      it.setName(this.support.toIDMultiple("compliance", relName));
-      it.setFofRole("axiom");
-      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-      final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
-        for (final VLSVariable v : relVar2VLS) {
-          EList<VLSTffTerm> _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", relName));
-            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);
-          trace.predicate2Relation.put(rel, r);
-          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 r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {
-    final Map<Variable, VLSVariable> relVar2VLS = new HashMap<Variable, VLSVariable>();
-    final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList();
-    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.put(r.getVariables().get((i).intValue()), v);
-        vars.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);
-      }
-    }
-    final String[] nameArray = r.getName().split(" ");
-    String relNameVar = "";
-    int _length_1 = nameArray.length;
-    boolean _equals = (_length_1 == 3);
-    if (_equals) {
-      relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
-    } else {
-      relNameVar = r.getName();
-    }
-    final String relName = relNameVar;
-    final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS);
-    final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply);
-    VLSAnd _createVLSAnd = this.factory.createVLSAnd();
-    final Procedure1<VLSAnd> _function = (VLSAnd it) -> {
-      it.setLeft(compliance);
-      it.setRight(definition);
-    };
-    final VLSAnd compDefn = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);
-    VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-    final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
-      it.setName(this.support.toID(relName));
-      it.setFofRole("axiom");
-      VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-      final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
-        for (final VLSVariable v : vars) {
-          EList<VLSTffTerm> _variables = it_1.getVariables();
-          VLSVariable _duplicate = this.support.duplicate(v);
-          _variables.add(_duplicate);
-        }
-        VLSImplies _createVLSImplies = this.factory.createVLSImplies();
-        final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
-          VLSFunction _createVLSFunction = this.factory.createVLSFunction();
-          final Procedure1<VLSFunction> _function_4 = (VLSFunction it_3) -> {
-            it_3.setConstant(this.support.toIDMultiple("r", relName));
-            for (final VLSVariable v_1 : vars) {
-              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_4);
-          it_2.setLeft(this.support.duplicate(rel));
-          it_2.setRight(compDefn);
-        };
-        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 relDef = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
-    EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
-    _formulas.add(relDef);
-  }
-  
-  public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) {
-    if (r instanceof RelationDeclaration) {
-      _transformRelation((RelationDeclaration)r, trace, mapper);
-      return;
-    } else if (r instanceof RelationDefinition) {
-      _transformRelation((RelationDefinition)r, trace, mapper);
-      return;
-    } else {
-      throw new IllegalArgumentException("Unhandled parameter types: " +
-        Arrays.<Object>asList(r, trace, mapper).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
deleted file mode 100644
index d6c90484..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ /dev/null
@@ -1,302 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
-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.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.VLSTffTerm;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
-import com.google.common.base.Objects;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.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.util.CollectionsUtil;
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
-import org.eclipse.emf.common.util.EList;
-import org.eclipse.xtext.xbase.lib.CollectionLiterals;
-import org.eclipse.xtext.xbase.lib.Conversions;
-import org.eclipse.xtext.xbase.lib.Extension;
-import org.eclipse.xtext.xbase.lib.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_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 List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
-    int elemsInIM = trace.definedElement2String.size();
-    final int ABSOLUTE_MIN = 0;
-    final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM);
-    final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);
-    final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM);
-    final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();
-    final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN);
-    if ((GLOBAL_MIN != ABSOLUTE_MIN)) {
-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));
-      if (consistant) {
-        for (final VLSConstant i : trace.uniqueInstances) {
-          localInstances.add(this.support.duplicate(i));
-        }
-        this.makeFofFormula(localInstances, trace, true, null);
-      } else {
-        this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null);
-      }
-    }
-    if ((GLOBAL_MAX != ABSOLUTE_MAX)) {
-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);
-      if (consistant) {
-        this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);
-      } else {
-        this.makeFofFormula(localInstances, trace, false, null);
-      }
-    }
-    int i_1 = 1;
-    if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) {
-      i_1 = 0;
-    }
-    int minNum = (-1);
-    Map<Type, Integer> startPoints = new HashMap<Type, Integer>();
-    final Function1<Type, Boolean> _function = (Type it) -> {
-      boolean _equals = it.equals(trace.topLevelType);
-      return Boolean.valueOf((!_equals));
-    };
-    Iterable<Type> _filter = IterableExtensions.<Type>filter(config.typeScopes.minNewElementsByType.keySet(), _function);
-    for (final Type t : _filter) {
-      {
-        int numIniIntModel = 0;
-        Set<DefinedElement> _keySet = trace.definedElement2String.keySet();
-        for (final DefinedElement elem : _keySet) {
-          EList<TypeDefinition> _definedInType = elem.getDefinedInType();
-          for (final TypeDefinition tDefined : _definedInType) {
-            boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined);
-            if (_dfsSubtypeCheck) {
-              int _numIniIntModel = numIniIntModel;
-              numIniIntModel = (_numIniIntModel + 1);
-            }
-          }
-        }
-        Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType);
-        int _minus = ((_lookup).intValue() - numIniIntModel);
-        minNum = _minus;
-        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);
-        }
-      }
-    }
-    final Function1<Type, Boolean> _function_1 = (Type it) -> {
-      boolean _equals = it.equals(trace.topLevelType);
-      return Boolean.valueOf((!_equals));
-    };
-    Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1);
-    for (final Type t_1 : _filter_1) {
-      {
-        int numIniIntModel = 0;
-        Set<DefinedElement> _keySet = trace.definedElement2String.keySet();
-        for (final DefinedElement elem : _keySet) {
-          EList<TypeDefinition> _definedInType = elem.getDefinedInType();
-          boolean _equals = Objects.equal(_definedInType, t_1);
-          if (_equals) {
-            int _numIniIntModel = numIniIntModel;
-            numIniIntModel = (_numIniIntModel + 1);
-          }
-        }
-        Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType);
-        int maxNum = ((_lookup).intValue() - numIniIntModel);
-        boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1);
-        if (_contains) {
-          Integer _lookup_1 = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType);
-          int _minus = ((_lookup_1).intValue() - numIniIntModel);
-          minNum = _minus;
-        } else {
-          minNum = 0;
-        }
-        if ((minNum != 0)) {
-          Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints);
-          this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false);
-        } else {
-          localInstances.clear();
-        }
-        int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + maxNum) - minNum));
-        this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false);
-        this.makeFofFormula(localInstances, trace, false, t_1);
-      }
-    }
-    final boolean DUPLICATES = config.uniquenessDuplicates;
-    final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;
-    int ind = 1;
-    if ((numInst != 0)) {
-      if (DUPLICATES) {
-        for (final VLSConstant e : trace.uniqueInstances) {
-          {
-            final int x = ind;
-            VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-            final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
-              it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));
-              it.setFofRole("axiom");
-              it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e));
-            };
-            final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
-            EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
-            _formulas.add(uniqueness);
-            ind++;
-          }
-        }
-      } else {
-        List<VLSConstant> _subList = trace.uniqueInstances.subList(0, (numInst - 1));
-        for (final VLSConstant e_1 : _subList) {
-          {
-            final int x = ind;
-            VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-            final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
-              it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName()));
-              it.setFofRole("axiom");
-              it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1));
-            };
-            final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
-            EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
-            _formulas.add(uniqueness);
-            ind++;
-          }
-        }
-      }
-    }
-  }
-  
-  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<VLSTffTerm> _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 List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
-    _transformScope(types, 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
deleted file mode 100644
index d757212a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java
+++ /dev/null
@@ -1,515 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;
-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.VLSTffTerm;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
-import com.google.common.base.Objects;
-import com.google.common.collect.Iterables;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression;
-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 java.util.concurrent.TimeUnit;
-import okhttp3.MediaType;
-import okhttp3.OkHttpClient;
-import okhttp3.Request;
-import okhttp3.RequestBody;
-import okhttp3.Response;
-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 List<VLSVariable> duplicate(final List<VLSVariable> vars) {
-    ArrayList<VLSVariable> newList = CollectionLiterals.<VLSVariable>newArrayList();
-    for (final VLSVariable v : vars) {
-      newList.add(this.duplicate(v));
-    }
-    return newList;
-  }
-  
-  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 VLSConstant t2) {
-    final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList();
-    for (final VLSConstant t1 : terms) {
-      boolean _notEquals = (!Objects.equal(t1, t2));
-      if (_notEquals) {
-        VLSInequality _createVLSInequality = this.factory.createVLSInequality();
-        final Procedure1<VLSInequality> _function = (VLSInequality it) -> {
-          VLSConstant _createVLSConstant = this.factory.createVLSConstant();
-          final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> {
-            it_1.setName(t2.getName());
-          };
-          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<VLSTffTerm> _variables = it.getVariables();
-          Collection<VLSVariable> _values = variableMap.values();
-          Iterables.<VLSTffTerm>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<VLSTffTerm> _variables = it.getVariables();
-            Collection<VLSVariable> _values = variableMap.values();
-            Iterables.<VLSTffTerm>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 boolean dfsSubtypeCheck(final Type type, final Type type2) {
-    boolean _xifexpression = false;
-    boolean _isEmpty = type.getSubtypes().isEmpty();
-    if (_isEmpty) {
-      return false;
-    } else {
-      boolean _xifexpression_1 = false;
-      boolean _contains = type.getSubtypes().contains(type2);
-      if (_contains) {
-        return true;
-      } else {
-        EList<Type> _subtypes = type.getSubtypes();
-        for (final Type subtype : _subtypes) {
-          boolean _dfsSubtypeCheck = this.dfsSubtypeCheck(subtype, type2);
-          if (_dfsSubtypeCheck) {
-            return true;
-          }
-        }
-      }
-      _xifexpression = _xifexpression_1;
-    }
-    return _xifexpression;
-  }
-  
-  protected void listSubtypes(final Type t, final List<Type> allSubtypes) {
-    EList<Type> _subtypes = t.getSubtypes();
-    for (final Type subt : _subtypes) {
-      {
-        allSubtypes.add(subt);
-        this.listSubtypes(subt, allSubtypes);
-      }
-    }
-  }
-  
-  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);
-  }
-  
-  public String makeForm(final String formula, final BackendSolver solver, final int time) {
-    String _header = this.getHeader();
-    String _plus = (_header + formula);
-    String _addOptions = this.addOptions();
-    String _plus_1 = (_plus + _addOptions);
-    String _addSolver = this.addSolver(solver, time);
-    String _plus_2 = (_plus_1 + _addSolver);
-    String _addEnd = this.addEnd();
-    return (_plus_2 + _addEnd);
-  }
-  
-  public ArrayList<String> getSolverSpecs(final BackendSolver solver) {
-    if (solver != null) {
-      switch (solver) {
-        case CVC4:
-          return CollectionLiterals.<String>newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT");
-        case DARWINFM:
-          return CollectionLiterals.<String>newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s");
-        case EDARWIN:
-          return CollectionLiterals.<String>newArrayList("E-Darwin---1.5", 
-            "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s");
-        case GEOIII:
-          return CollectionLiterals.<String>newArrayList("Geo-III---2018C", 
-            "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s");
-        case IPROVER:
-          return CollectionLiterals.<String>newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s");
-        case PARADOX:
-          return CollectionLiterals.<String>newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s");
-        case VAMPIRE:
-          return CollectionLiterals.<String>newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s");
-        case Z3:
-          return CollectionLiterals.<String>newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s");
-        default:
-          break;
-      }
-    }
-    return null;
-  }
-  
-  public String getHeader() {
-    return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n";
-  }
-  
-  public String addSpec(final String spec) {
-    return spec.replace("\n", "\\r\\n");
-  }
-  
-  public String addOptions() {
-    return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n";
-  }
-  
-  public String addSolver(final BackendSolver solver, final int time) {
-    final ArrayList<String> solverSpecs = this.getSolverSpecs(solver);
-    final String ID = solverSpecs.get(0);
-    final String cmd = solverSpecs.get(1);
-    return (((((((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID) + 
-      "\"\r\n\r\n") + Integer.valueOf(time)) + 
-      "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___") + ID) + 
-      "\"\r\n\r\n") + ID) + 
-      "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + 
-      "\"\r\n\r\n") + cmd) + "\r\n");
-  }
-  
-  public String addEnd() {
-    return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--";
-  }
-  
-  public ArrayList<String> sendPost(final String formData) throws Exception {
-    final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, 
-      TimeUnit.SECONDS).build();
-    final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA");
-    final RequestBody body = RequestBody.create(mediaType, formData);
-    final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", 
-      "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", 
-      "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", 
-      "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", 
-      "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", 
-      "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", 
-      "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", 
-      "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build();
-    final Response response = client.newCall(request).execute();
-    return CollectionLiterals.<String>newArrayList(response.body().string().split("\n"));
-  }
-}
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
deleted file mode 100644
index 72fea6d3..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ /dev/null
@@ -1,339 +0,0 @@
-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.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.VLSTffTerm;
-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) -> {
-            int _length = type.getName().split(" ").length;
-            boolean _equals = (_length == 3);
-            if (_equals) {
-              it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2]));
-            } else {
-              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);
-          trace.predicate2Type.put(typePred, type);
-        }
-      }
-      final Function1<TypeDefinition, Boolean> _function_1 = (TypeDefinition it) -> {
-        boolean _isIsAbstract = it.isIsAbstract();
-        return Boolean.valueOf((!_isIsAbstract));
-      };
-      Iterable<TypeDefinition> _filter = IterableExtensions.<TypeDefinition>filter(Iterables.<TypeDefinition>filter(types, TypeDefinition.class), _function_1);
-      for (final TypeDefinition type_1 : _filter) {
-        {
-          final int len = type_1.getName().length();
-          boolean _equals = type_1.getName().substring((len - 4), len).equals("enum");
-          final boolean isNotEnum = (!_equals);
-          final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();
-          EList<DefinedElement> _elements = type_1.getElements();
-          for (final DefinedElement e : _elements) {
-            {
-              final String[] nameArray = e.getName().split(" ");
-              String relNameVar = "";
-              int _length = nameArray.length;
-              boolean _equals_1 = (_length == 3);
-              if (_equals_1) {
-                relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
-              } else {
-                relNameVar = e.getName();
-              }
-              final String relName = relNameVar;
-              VLSFunction _createVLSFunction = this.factory.createVLSFunction();
-              final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {
-                it.setConstant(this.support.toIDMultiple("e", relName));
-                EList<VLSTerm> _terms = it.getTerms();
-                VLSVariable _duplicate = this.support.duplicate(variable);
-                _terms.add(_duplicate);
-              };
-              final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2);
-              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_1 = Objects.equal(t1, t2);
-                if (_equals_1) {
-                  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_2 = (VLSUnaryNegation it) -> {
-                    it.setOperand(op);
-                  };
-                  final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);
-                  possibleNots.add(negFct);
-                }
-              }
-              typeDefs.add(this.support.unfoldAnd(possibleNots));
-              possibleNots.clear();
-            }
-          }
-          VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-          final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
-            it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString()));
-            it.setFofRole("axiom");
-            VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-            final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {
-              EList<VLSTffTerm> _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(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));
-                VLSAnd _createVLSAnd = this.factory.createVLSAnd();
-                final Procedure1<VLSAnd> _function_5 = (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_5);
-                it_2.setRight(_doubleArrow);
-              };
-              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 res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
-          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);
-              final int index = (i - globalCounter);
-              VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
-              final Procedure1<VLSFunctionAsTerm> _function_3 = (VLSFunctionAsTerm it) -> {
-                it.setFunctor(("eo" + Integer.valueOf(num)));
-              };
-              final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3);
-              trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());
-              final VLSConstant cst = this.support.toConstant(cstTerm);
-              trace.uniqueInstances.add(cst);
-              VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
-              final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
-                String _xifexpression = null;
-                if (isNotEnum) {
-                  _xifexpression = "definedType";
-                } else {
-                  _xifexpression = "enumScope";
-                }
-                it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString(), 
-                  type_1.getElements().get(index).getName().split(" ")[0]));
-                it.setFofRole("axiom");
-                VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-                final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {
-                  EList<VLSTffTerm> _variables = it_1.getVariables();
-                  VLSVariable _duplicate = this.support.duplicate(variable);
-                  _variables.add(_duplicate);
-                  VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
-                  final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> {
-                    VLSEquality _createVLSEquality = this.factory.createVLSEquality();
-                    final Procedure1<VLSEquality> _function_7 = (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_7);
-                    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_6);
-                  it_1.setOperand(_doubleArrow);
-                };
-                VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);
-                it.setFofFormula(_doubleArrow);
-              };
-              final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);
-              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_2 = (Type it) -> {
-        boolean _isIsAbstract = it.isIsAbstract();
-        return Boolean.valueOf((!_isIsAbstract));
-      };
-      Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_2);
-      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_3 = (VLSUnaryNegation it) -> {
-                it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
-              };
-              VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
-              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();
-        }
-      }
-      final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList();
-      for (final Type t : types) {
-        VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
-        final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
-          it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate)));
-        };
-        VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
-        type2Not.add(_doubleArrow);
-      }
-      VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
-      final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
-        it.setName("notObjectHandler");
-        it.setFofRole("axiom");
-        VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-        final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {
-          EList<VLSTffTerm> _variables = it_1.getVariables();
-          VLSVariable _duplicate = this.support.duplicate(variable);
-          _variables.add(_duplicate);
-          VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
-          final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> {
-            VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation();
-            final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {
-              it_3.setOperand(this.support.topLevelTypeFunc());
-            };
-            VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_7);
-            it_2.setLeft(_doubleArrow_1);
-            it_2.setRight(this.support.unfoldAnd(type2Not));
-          };
-          VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6);
-          it_1.setOperand(_doubleArrow_1);
-        };
-        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);
-        it.setFofFormula(_doubleArrow_1);
-      };
-      final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_4);
-      EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
-      _formulas.add(notObj);
-      VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
-      final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> {
-        it.setName("inheritanceHierarchyHandler");
-        it.setFofRole("axiom");
-        VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
-        final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> {
-          EList<VLSTffTerm> _variables = it_1.getVariables();
-          VLSVariable _duplicate = this.support.duplicate(variable);
-          _variables.add(_duplicate);
-          VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
-          final Procedure1<VLSEquivalent> _function_7 = (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_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_7);
-          it_1.setOperand(_doubleArrow_1);
-        };
-        VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_6);
-        it.setFofFormula(_doubleArrow_1);
-      };
-      final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5);
-      EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
-      _xblockexpression = _formulas_1.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 VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {
-    VLSConstant _createVLSConstant = this.factory.createVLSConstant();
-    final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
-      it.setName(referred.getName());
-    };
-    return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _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
deleted file mode 100644
index 1e08c8ad..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java
+++ /dev/null
@@ -1,5 +0,0 @@
-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/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
deleted file mode 100644
index 9fb23c71..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
+++ /dev/null
@@ -1,42 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;
-import org.eclipse.emf.common.util.EList;
-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 Vampire2LogicMapper {
-  @Extension
-  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;
-  
-  public ModelResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final MonitoredVampireSolution monitoredVampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) {
-    ModelResult _createModelResult = this.resultFactory.createModelResult();
-    final Procedure1<ModelResult> _function = (ModelResult it) -> {
-      it.setProblem(problem);
-      EList<Object> _representation = it.getRepresentation();
-      VampireModel _generatedModel = monitoredVampireSolution.getGeneratedModel();
-      _representation.add(_generatedModel);
-      it.setTrace(trace);
-      it.setStatistics(this.transformStatistics(monitoredVampireSolution, transformationTime));
-    };
-    return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);
-  }
-  
-  public Statistics transformStatistics(final MonitoredVampireSolution solution, final long transformationTime) {
-    Statistics _createStatistics = this.resultFactory.createStatistics();
-    final Procedure1<Statistics> _function = (Statistics it) -> {
-      long _solverTime = solution.getSolverTime();
-      it.setSolverTime(((int) _solverTime));
-      it.setTransformationTime(((int) transformationTime));
-    };
-    return ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function);
-  }
-}
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
deleted file mode 100644
index 39773357..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ /dev/null
@@ -1,82 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
-import com.google.common.base.Objects;
-import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
-import java.io.BufferedReader;
-import java.io.FileReader;
-import java.util.List;
-import org.eclipse.emf.common.util.URI;
-import org.eclipse.xtext.xbase.lib.CollectionLiterals;
-import org.eclipse.xtext.xbase.lib.Conversions;
-import org.eclipse.xtext.xbase.lib.Exceptions;
-import org.eclipse.xtext.xbase.lib.InputOutput;
-@SuppressWarnings("all")
-public class VampireHandler {
-  public MonitoredVampireSolution callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) {
-    try {
-      final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";
-      final String VAMPNAME = "vampire.exe";
-      final String VAMPLOC = (VAMPDIR + VAMPNAME);
-      final String CVC4DIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";
-      final String CVC4NAME = "vampire.exe";
-      final String CVC4LOC = (CVC4DIR + CVC4NAME);
-      final String CMD = "cmd /c ";
-      final String TEMPNAME = "TEMP.tptp";
-      final String SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + 
-        ".tptp");
-      final String PATH = "C:/cygwin64/bin";
-      final URI wsURI = workspace.getWorkspaceURI();
-      final String tempLoc = (wsURI + TEMPNAME);
-      String _plus = (wsURI + SOLNNAME);
-      final String solnLoc = (_plus + " ");
-      String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString();
-      long startTime = (-((long) 1));
-      long solverTime = (-((long) 1));
-      Process p = null;
-      boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP);
-      if (_equals) {
-        String OPTION = " --mode casc_sat ";
-        if ((configuration.runtimeLimit != (-1))) {
-          OPTION = (((OPTION + "-t ") + Integer.valueOf(configuration.runtimeLimit)) + " ");
-        }
-        startTime = System.currentTimeMillis();
-        p = Runtime.getRuntime().exec((((((CMD + VAMPLOC) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));
-        p.waitFor();
-        long _currentTimeMillis = System.currentTimeMillis();
-        long _minus = (_currentTimeMillis - startTime);
-        solverTime = _minus;
-      }
-      boolean _equals_1 = Objects.equal(configuration.solver, BackendSolver.CVC4);
-      if (_equals_1) {
-        String OPTION_1 = " SAT ";
-        if ((configuration.runtimeLimit != (-1))) {
-          OPTION_1 = ((" " + Integer.valueOf(configuration.runtimeLimit)) + OPTION_1);
-        }
-        InputOutput.<String>println((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc));
-        p = Runtime.getRuntime().exec((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));
-        p.waitFor();
-        long _currentTimeMillis_1 = System.currentTimeMillis();
-        long _minus_1 = (_currentTimeMillis_1 - startTime);
-        solverTime = _minus_1;
-      }
-      FileReader _fileReader = new FileReader(solnLoc);
-      final BufferedReader reader = new BufferedReader(_fileReader);
-      final List<String> output = CollectionLiterals.<String>newArrayList();
-      String line = "";
-      while ((!Objects.equal((line = reader.readLine()), null))) {
-        boolean _equals_2 = Objects.equal(line, "Finite Model Found!");
-        if (_equals_2) {
-          return new MonitoredVampireSolution(solverTime, null, true);
-        }
-      }
-      return new MonitoredVampireSolution(solverTime, null, false);
-    } catch (Throwable _e) {
-      throw Exceptions.sneakyThrow(_e);
-    }
-  }
-}
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
deleted file mode 100644
index 507831fa..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java
+++ /dev/null
@@ -1,5 +0,0 @@
-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
deleted file mode 100644
index aff0dc9d..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java
+++ /dev/null
@@ -1,7 +0,0 @@
-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/VampireSolverException.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java
deleted file mode 100644
index b96df82a..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java
+++ /dev/null
@@ -1,19 +0,0 @@
-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);
-  }
-}