17 files changed, 718 insertions, 661 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSDeclaration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSDeclaration.java
index d3e5a2d5..4ff74235 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSDeclaration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSDeclaration.java
@@ -9,6 +9,12 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 * A representation of the model object '<em><b>VLS Declaration</b></em>'.
 * <!-- end-user-doc -->
 *
+ * <p>
+ * The following features are supported:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDeclaration#getType <em>Type</em>}</li>
+ * </ul>
 *
 * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSDeclaration()
 * @model
@@ -16,4 +22,30 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 */
 public interface VLSDeclaration extends VLSTffTerm
 {
+  /**
+   * Returns the value of the '<em><b>Type</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Type</em>' containment reference isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Type</em>' containment reference.
+   * @see #setType(VLSTypeDef)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSDeclaration_Type()
+   * @model containment="true"
+   * @generated
+   */
+  VLSTypeDef getType();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDeclaration#getType <em>Type</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Type</em>' containment reference.
+   * @see #getType()
+   * @generated
+   */
+  void setType(VLSTypeDef value);
 } // VLSDeclaration
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSExistentialQuantifier.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSExistentialQuantifier.java
index a70dff64..c70d312b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSExistentialQuantifier.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSExistentialQuantifier.java
@@ -26,7 +26,7 @@ public interface VLSExistentialQuantifier extends VLSTerm
 {
  /**
   * Returns the value of the '<em><b>Variables</b></em>' containment reference list.
-   * The list contents are of type {@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration}.
+   * The list contents are of type {@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm}.
   * <!-- begin-user-doc -->
   * <p>
   * If the meaning of the '<em>Variables</em>' containment reference list isn't clear,
@@ -38,7 +38,7 @@ public interface VLSExistentialQuantifier extends VLSTerm
   * @model containment="true"
   * @generated
   */
-  EList<VLSVariableDeclaration> getVariables();
+  EList<VLSTffTerm> getVariables();
  /**
   * Returns the value of the '<em><b>Operand</b></em>' containment reference.
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSOtherDeclaration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSOtherDeclaration.java
index 0ffd104d..4e4e3d8b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSOtherDeclaration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSOtherDeclaration.java
@@ -9,6 +9,12 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 * A representation of the model object '<em><b>VLS Other Declaration</b></em>'.
 * <!-- end-user-doc -->
 *
+ * <p>
+ * The following features are supported:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration#getName <em>Name</em>}</li>
+ * </ul>
 *
 * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSOtherDeclaration()
 * @model
@@ -16,4 +22,30 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 */
 public interface VLSOtherDeclaration extends VLSDeclaration
 {
+  /**
+   * Returns the value of the '<em><b>Name</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Name</em>' containment reference isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Name</em>' containment reference.
+   * @see #setName(VLSTerm)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSOtherDeclaration_Name()
+   * @model containment="true"
+   * @generated
+   */
+  VLSTerm getName();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration#getName <em>Name</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Name</em>' containment reference.
+   * @see #getName()
+   * @generated
+   */
+  void setName(VLSTerm value);
 } // VLSOtherDeclaration
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTerm.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTerm.java
index 7a077714..d1f20508 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTerm.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTerm.java
@@ -9,43 +9,11 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 * A representation of the model object '<em><b>VLS Term</b></em>'.
 * <!-- end-user-doc -->
 *
- * <p>
- * The following features are supported:
- * </p>
- * <ul>
- *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm#getType <em>Type</em>}</li>
- * </ul>
 *
 * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTerm()
 * @model
 * @generated
 */
-public interface VLSTerm extends VLSTffTerm, VLSOtherDeclaration
+public interface VLSTerm extends VLSTffTerm
 {
-  /**
-   * Returns the value of the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <p>
-   * If the meaning of the '<em>Type</em>' containment reference isn't clear,
-   * there really should be more of a description here...
-   * </p>
-   * <!-- end-user-doc -->
-   * @return the value of the '<em>Type</em>' containment reference.
-   * @see #setType(VLSTypeDef)
-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTerm_Type()
-   * @model containment="true"
-   * @generated
-   */
-  VLSTypeDef getType();
-  /**
-   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm#getType <em>Type</em>}' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @param value the new value of the '<em>Type</em>' containment reference.
-   * @see #getType()
-   * @generated
-   */
-  void setType(VLSTypeDef value);
 } // VLSTerm
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSUniversalQuantifier.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSUniversalQuantifier.java
index 00dd1733..9e7da58a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSUniversalQuantifier.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSUniversalQuantifier.java
@@ -26,7 +26,7 @@ public interface VLSUniversalQuantifier extends VLSTerm
 {
  /**
   * Returns the value of the '<em><b>Variables</b></em>' containment reference list.
-   * The list contents are of type {@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration}.
+   * The list contents are of type {@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm}.
   * <!-- begin-user-doc -->
   * <p>
   * If the meaning of the '<em>Variables</em>' containment reference list isn't clear,
@@ -38,7 +38,7 @@ public interface VLSUniversalQuantifier extends VLSTerm
   * @model containment="true"
   * @generated
   */
-  EList<VLSVariableDeclaration> getVariables();
+  EList<VLSTffTerm> getVariables();
  /**
   * Returns the value of the '<em><b>Operand</b></em>' containment reference.
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariable.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariable.java
index 5a9dc028..9750e4c5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariable.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariable.java
@@ -20,7 +20,7 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 * @model
 * @generated
 */
-public interface VLSVariable extends VLSVariableDeclaration, VLSTerm
+public interface VLSVariable extends VLSTerm
 {
  /**
   * Returns the value of the '<em><b>Name</b></em>' attribute.
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariableDeclaration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariableDeclaration.java
index 9e5a6ba2..a45aec5c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariableDeclaration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSVariableDeclaration.java
@@ -9,6 +9,12 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 * A representation of the model object '<em><b>VLS Variable Declaration</b></em>'.
 * <!-- end-user-doc -->
 *
+ * <p>
+ * The following features are supported:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration#getName <em>Name</em>}</li>
+ * </ul>
 *
 * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSVariableDeclaration()
 * @model
@@ -16,4 +22,30 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage;
 */
 public interface VLSVariableDeclaration extends VLSDeclaration
 {
+  /**
+   * Returns the value of the '<em><b>Name</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Name</em>' containment reference isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Name</em>' containment reference.
+   * @see #setName(VLSVariable)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSVariableDeclaration_Name()
+   * @model containment="true"
+   * @generated
+   */
+  VLSVariable getName();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration#getName <em>Name</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Name</em>' containment reference.
+   * @see #getName()
+   * @generated
+   */
+  void setName(VLSVariable value);
 } // VLSVariableDeclaration
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
index 3ef777f8..7c917251 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
@@ -345,13 +345,22 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_DECLARATION = 7;
  /**
+   * The feature id for the '<em><b>Type</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_DECLARATION__TYPE = VLS_TFF_TERM_FEATURE_COUNT + 0;
+  /**
   * The number of structural features of the '<em>VLS Declaration</em>' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
   * @ordered
   */
-  int VLS_DECLARATION_FEATURE_COUNT = VLS_TFF_TERM_FEATURE_COUNT + 0;
+  int VLS_DECLARATION_FEATURE_COUNT = VLS_TFF_TERM_FEATURE_COUNT + 1;
  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOtherDeclarationImpl <em>VLS Other Declaration</em>}' class.
@@ -364,13 +373,31 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_OTHER_DECLARATION = 8;
  /**
+   * The feature id for the '<em><b>Type</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_OTHER_DECLARATION__TYPE = VLS_DECLARATION__TYPE;
+  /**
+   * The feature id for the '<em><b>Name</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_OTHER_DECLARATION__NAME = VLS_DECLARATION_FEATURE_COUNT + 0;
+  /**
   * The number of structural features of the '<em>VLS Other Declaration</em>' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
   * @ordered
   */
-  int VLS_OTHER_DECLARATION_FEATURE_COUNT = VLS_DECLARATION_FEATURE_COUNT + 0;
+  int VLS_OTHER_DECLARATION_FEATURE_COUNT = VLS_DECLARATION_FEATURE_COUNT + 1;
  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableDeclarationImpl <em>VLS Variable Declaration</em>}' class.
@@ -383,13 +410,31 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_VARIABLE_DECLARATION = 9;
  /**
+   * The feature id for the '<em><b>Type</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_VARIABLE_DECLARATION__TYPE = VLS_DECLARATION__TYPE;
+  /**
+   * The feature id for the '<em><b>Name</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_VARIABLE_DECLARATION__NAME = VLS_DECLARATION_FEATURE_COUNT + 0;
+  /**
   * The number of structural features of the '<em>VLS Variable Declaration</em>' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
   * @ordered
   */
-  int VLS_VARIABLE_DECLARATION_FEATURE_COUNT = VLS_DECLARATION_FEATURE_COUNT + 0;
+  int VLS_VARIABLE_DECLARATION_FEATURE_COUNT = VLS_DECLARATION_FEATURE_COUNT + 1;
  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTypeDefImpl <em>VLS Type Def</em>}' class.
@@ -457,22 +502,13 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_TERM = 11;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_TERM__TYPE = VLS_TFF_TERM_FEATURE_COUNT + 0;
-  /**
   * The number of structural features of the '<em>VLS Term</em>' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
   * @ordered
   */
-  int VLS_TERM_FEATURE_COUNT = VLS_TFF_TERM_FEATURE_COUNT + 1;
+  int VLS_TERM_FEATURE_COUNT = VLS_TFF_TERM_FEATURE_COUNT + 0;
  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableImpl <em>VLS Variable</em>}' class.
@@ -485,22 +521,13 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_VARIABLE = 12;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_VARIABLE__TYPE = VLS_VARIABLE_DECLARATION_FEATURE_COUNT + 0;
-  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
   * @ordered
   */
-  int VLS_VARIABLE__NAME = VLS_VARIABLE_DECLARATION_FEATURE_COUNT + 1;
+  int VLS_VARIABLE__NAME = VLS_TERM_FEATURE_COUNT + 0;
  /**
   * The number of structural features of the '<em>VLS Variable</em>' class.
@@ -509,7 +536,7 @@ public interface VampireLanguagePackage extends EPackage
   * @generated
   * @ordered
   */
-  int VLS_VARIABLE_FEATURE_COUNT = VLS_VARIABLE_DECLARATION_FEATURE_COUNT + 2;
+  int VLS_VARIABLE_FEATURE_COUNT = VLS_TERM_FEATURE_COUNT + 1;
  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFunctionAsTermImpl <em>VLS Function As Term</em>}' class.
@@ -522,15 +549,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_FUNCTION_AS_TERM = 13;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_FUNCTION_AS_TERM__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Functor</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -568,15 +586,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_DEFINED_TERM = 14;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_DEFINED_TERM__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -690,15 +699,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_EQUIVALENT = 19;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_EQUIVALENT__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -736,15 +736,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_IMPLIES = 20;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_IMPLIES__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -782,15 +773,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_REV_IMPLIES = 21;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_REV_IMPLIES__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -828,15 +810,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_XNOR = 22;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_XNOR__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -874,15 +847,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_NOR = 23;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_NOR__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -920,15 +884,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_NAND = 24;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_NAND__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -966,15 +921,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_AND = 25;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_AND__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1012,15 +958,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_OR = 26;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_OR__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1058,15 +995,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_UNIVERSAL_QUANTIFIER = 27;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_UNIVERSAL_QUANTIFIER__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Variables</b></em>' containment reference list.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1104,15 +1032,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_EXISTENTIAL_QUANTIFIER = 28;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_EXISTENTIAL_QUANTIFIER__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Variables</b></em>' containment reference list.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1150,15 +1069,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_UNARY_NEGATION = 29;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_UNARY_NEGATION__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Operand</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1187,15 +1097,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_INEQUALITY = 30;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_INEQUALITY__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1233,15 +1134,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_EQUALITY = 31;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_EQUALITY__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1279,15 +1171,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_ASSIGNMENT = 32;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_ASSIGNMENT__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1325,15 +1208,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_CONSTANT = 33;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_CONSTANT__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1362,15 +1236,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_TRUE = 34;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_TRUE__TYPE = VLS_TERM__TYPE;
-  /**
   * The number of structural features of the '<em>VLS True</em>' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1390,15 +1255,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_FALSE = 35;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_FALSE__TYPE = VLS_TERM__TYPE;
-  /**
   * The number of structural features of the '<em>VLS False</em>' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1418,15 +1274,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_FUNCTION = 36;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_FUNCTION__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Constant</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1464,15 +1311,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_LESS = 37;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_LESS__TYPE = VLS_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1510,15 +1348,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_INT = 38;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_INT__TYPE = VLS_DEFINED_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1547,15 +1376,6 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_DOUBLE_QUOTE = 39;
  /**
-   * The feature id for the '<em><b>Type</b></em>' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   * @ordered
-   */
-  int VLS_DOUBLE_QUOTE__TYPE = VLS_DEFINED_TERM__TYPE;
-  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1831,6 +1651,17 @@ public interface VampireLanguagePackage extends EPackage
  EClass getVLSDeclaration();
  /**
+   * Returns the meta object for the containment reference '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDeclaration#getType <em>Type</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the containment reference '<em>Type</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDeclaration#getType()
+   * @see #getVLSDeclaration()
+   * @generated
+   */
+  EReference getVLSDeclaration_Type();
+  /**
   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration <em>VLS Other Declaration</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1841,6 +1672,17 @@ public interface VampireLanguagePackage extends EPackage
  EClass getVLSOtherDeclaration();
  /**
+   * Returns the meta object for the containment reference '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration#getName <em>Name</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the containment reference '<em>Name</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration#getName()
+   * @see #getVLSOtherDeclaration()
+   * @generated
+   */
+  EReference getVLSOtherDeclaration_Name();
+  /**
   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration <em>VLS Variable Declaration</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1851,6 +1693,17 @@ public interface VampireLanguagePackage extends EPackage
  EClass getVLSVariableDeclaration();
  /**
+   * Returns the meta object for the containment reference '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration#getName <em>Name</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the containment reference '<em>Name</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration#getName()
+   * @see #getVLSVariableDeclaration()
+   * @generated
+   */
+  EReference getVLSVariableDeclaration_Name();
+  /**
   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTypeDef <em>VLS Type Def</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1915,17 +1768,6 @@ public interface VampireLanguagePackage extends EPackage
  EClass getVLSTerm();
  /**
-   * Returns the meta object for the containment reference '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm#getType <em>Type</em>}'.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @return the meta object for the containment reference '<em>Type</em>'.
-   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm#getType()
-   * @see #getVLSTerm()
-   * @generated
-   */
-  EReference getVLSTerm_Type();
-  /**
   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable <em>VLS Variable</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -2844,6 +2686,14 @@ public interface VampireLanguagePackage extends EPackage
    EClass VLS_DECLARATION = eINSTANCE.getVLSDeclaration();
    /**
+     * The meta object literal for the '<em><b>Type</b></em>' containment reference feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EReference VLS_DECLARATION__TYPE = eINSTANCE.getVLSDeclaration_Type();
+    /**
     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOtherDeclarationImpl <em>VLS Other Declaration</em>}' class.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
@@ -2854,6 +2704,14 @@ public interface VampireLanguagePackage extends EPackage
    EClass VLS_OTHER_DECLARATION = eINSTANCE.getVLSOtherDeclaration();
    /**
+     * The meta object literal for the '<em><b>Name</b></em>' containment reference feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EReference VLS_OTHER_DECLARATION__NAME = eINSTANCE.getVLSOtherDeclaration_Name();
+    /**
     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableDeclarationImpl <em>VLS Variable Declaration</em>}' class.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
@@ -2864,6 +2722,14 @@ public interface VampireLanguagePackage extends EPackage
    EClass VLS_VARIABLE_DECLARATION = eINSTANCE.getVLSVariableDeclaration();
    /**
+     * The meta object literal for the '<em><b>Name</b></em>' containment reference feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EReference VLS_VARIABLE_DECLARATION__NAME = eINSTANCE.getVLSVariableDeclaration_Name();
+    /**
     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTypeDefImpl <em>VLS Type Def</em>}' class.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
@@ -2916,14 +2782,6 @@ public interface VampireLanguagePackage extends EPackage
    EClass VLS_TERM = eINSTANCE.getVLSTerm();
    /**
-     * The meta object literal for the '<em><b>Type</b></em>' containment reference feature.
-     * <!-- begin-user-doc -->
-     * <!-- end-user-doc -->
-     * @generated
-     */
-    EReference VLS_TERM__TYPE = eINSTANCE.getVLSTerm_Type();
-    /**
     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableImpl <em>VLS Variable</em>}' class.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDeclarationImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDeclarationImpl.java
index bb913d80..894c76de 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDeclarationImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDeclarationImpl.java
@@ -4,20 +4,43 @@
 package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDeclaration;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTypeDef;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
 import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
 /**
 * <!-- begin-user-doc -->
 * An implementation of the model object '<em><b>VLS Declaration</b></em>'.
 * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSDeclarationImpl#getType <em>Type</em>}</li>
+ * </ul>
 *
 * @generated
 */
 public class VLSDeclarationImpl extends VLSTffTermImpl implements VLSDeclaration
 {
  /**
+   * The cached value of the '{@link #getType() <em>Type</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getType()
+   * @generated
+   * @ordered
+   */
+  protected VLSTypeDef type;
+  /**
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
@@ -38,4 +61,134 @@ public class VLSDeclarationImpl extends VLSTffTermImpl implements VLSDeclaration
    return VampireLanguagePackage.Literals.VLS_DECLARATION;
  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTypeDef getType()
+  {
+    return type;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetType(VLSTypeDef newType, NotificationChain msgs)
+  {
+    VLSTypeDef oldType = type;
+    type = newType;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_DECLARATION__TYPE, oldType, newType);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setType(VLSTypeDef newType)
+  {
+    if (newType != type)
+    {
+      NotificationChain msgs = null;
+      if (type != null)
+        msgs = ((InternalEObject)type).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_DECLARATION__TYPE, null, msgs);
+      if (newType != null)
+        msgs = ((InternalEObject)newType).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_DECLARATION__TYPE, null, msgs);
+      msgs = basicSetType(newType, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_DECLARATION__TYPE, newType, newType));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DECLARATION__TYPE:
+        return basicSetType(null, msgs);
+    }
+    return super.eInverseRemove(otherEnd, featureID, msgs);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DECLARATION__TYPE:
+        return getType();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DECLARATION__TYPE:
+        setType((VLSTypeDef)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DECLARATION__TYPE:
+        setType((VLSTypeDef)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DECLARATION__TYPE:
+        return type != null;
+    }
+    return super.eIsSet(featureID);
+  }
 } //VLSDeclarationImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSExistentialQuantifierImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSExistentialQuantifierImpl.java
index 115c7a23..6d71ec60 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSExistentialQuantifierImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSExistentialQuantifierImpl.java
@@ -5,7 +5,7 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
 import java.util.Collection;
@@ -47,7 +47,7 @@ public class VLSExistentialQuantifierImpl extends VLSTermImpl implements VLSExis
   * @generated
   * @ordered
   */
-  protected EList<VLSVariableDeclaration> variables;
+  protected EList<VLSTffTerm> variables;
  /**
   * The cached value of the '{@link #getOperand() <em>Operand</em>}' containment reference.
@@ -85,11 +85,11 @@ public class VLSExistentialQuantifierImpl extends VLSTermImpl implements VLSExis
   * <!-- end-user-doc -->
   * @generated
   */
-  public EList<VLSVariableDeclaration> getVariables()
+  public EList<VLSTffTerm> getVariables()
  {
    if (variables == null)
    {
-      variables = new EObjectContainmentEList<VLSVariableDeclaration>(VLSVariableDeclaration.class, this, VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__VARIABLES);
+      variables = new EObjectContainmentEList<VLSTffTerm>(VLSTffTerm.class, this, VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__VARIABLES);
    }
    return variables;
  }
@@ -191,7 +191,7 @@ public class VLSExistentialQuantifierImpl extends VLSTermImpl implements VLSExis
    {
      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__VARIABLES:
        getVariables().clear();
-        getVariables().addAll((Collection<? extends VLSVariableDeclaration>)newValue);
+        getVariables().addAll((Collection<? extends VLSTffTerm>)newValue);
        return;
      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND:
        setOperand((VLSTerm)newValue);
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSOtherDeclarationImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSOtherDeclarationImpl.java
index c5abc76a..eb7afd3d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSOtherDeclarationImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSOtherDeclarationImpl.java
@@ -4,20 +4,43 @@
 package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
 import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
 /**
 * <!-- begin-user-doc -->
 * An implementation of the model object '<em><b>VLS Other Declaration</b></em>'.
 * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOtherDeclarationImpl#getName <em>Name</em>}</li>
+ * </ul>
 *
 * @generated
 */
 public class VLSOtherDeclarationImpl extends VLSDeclarationImpl implements VLSOtherDeclaration
 {
  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm name;
+  /**
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
@@ -38,4 +61,134 @@ public class VLSOtherDeclarationImpl extends VLSDeclarationImpl implements VLSOt
    return VampireLanguagePackage.Literals.VLS_OTHER_DECLARATION;
  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetName(VLSTerm newName, NotificationChain msgs)
+  {
+    VLSTerm oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME, oldName, newName);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(VLSTerm newName)
+  {
+    if (newName != name)
+    {
+      NotificationChain msgs = null;
+      if (name != null)
+        msgs = ((InternalEObject)name).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME, null, msgs);
+      if (newName != null)
+        msgs = ((InternalEObject)newName).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME, null, msgs);
+      msgs = basicSetName(newName, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME, newName, newName));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME:
+        return basicSetName(null, msgs);
+    }
+    return super.eInverseRemove(otherEnd, featureID, msgs);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME:
+        return getName();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME:
+        setName((VLSTerm)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME:
+        setName((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_OTHER_DECLARATION__NAME:
+        return name != null;
+    }
+    return super.eIsSet(featureID);
+  }
 } //VLSOtherDeclarationImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java
index 0ea49b4c..c56d7ecd 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java
@@ -4,43 +4,20 @@
 package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTypeDef;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
-import org.eclipse.emf.common.notify.Notification;
-import org.eclipse.emf.common.notify.NotificationChain;
 import org.eclipse.emf.ecore.EClass;
-import org.eclipse.emf.ecore.InternalEObject;
-import org.eclipse.emf.ecore.impl.ENotificationImpl;
 /**
 * <!-- begin-user-doc -->
 * An implementation of the model object '<em><b>VLS Term</b></em>'.
 * <!-- end-user-doc -->
- * <p>
- * The following features are implemented:
- * </p>
- * <ul>
- *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTermImpl#getType <em>Type</em>}</li>
- * </ul>
 *
 * @generated
 */
 public class VLSTermImpl extends VLSTffTermImpl implements VLSTerm
 {
  /**
-   * The cached value of the '{@link #getType() <em>Type</em>}' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @see #getType()
-   * @generated
-   * @ordered
-   */
-  protected VLSTypeDef type;
-  /**
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
@@ -61,134 +38,4 @@ public class VLSTermImpl extends VLSTffTermImpl implements VLSTerm
    return VampireLanguagePackage.Literals.VLS_TERM;
  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  public VLSTypeDef getType()
-  {
-    return type;
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  public NotificationChain basicSetType(VLSTypeDef newType, NotificationChain msgs)
-  {
-    VLSTypeDef oldType = type;
-    type = newType;
-    if (eNotificationRequired())
-    {
-      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_TERM__TYPE, oldType, newType);
-      if (msgs == null) msgs = notification; else msgs.add(notification);
-    }
-    return msgs;
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  public void setType(VLSTypeDef newType)
-  {
-    if (newType != type)
-    {
-      NotificationChain msgs = null;
-      if (type != null)
-        msgs = ((InternalEObject)type).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_TERM__TYPE, null, msgs);
-      if (newType != null)
-        msgs = ((InternalEObject)newType).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_TERM__TYPE, null, msgs);
-      msgs = basicSetType(newType, msgs);
-      if (msgs != null) msgs.dispatch();
-    }
-    else if (eNotificationRequired())
-      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_TERM__TYPE, newType, newType));
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
-  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
-  {
-    switch (featureID)
-    {
-      case VampireLanguagePackage.VLS_TERM__TYPE:
-        return basicSetType(null, msgs);
-    }
-    return super.eInverseRemove(otherEnd, featureID, msgs);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
-  public Object eGet(int featureID, boolean resolve, boolean coreType)
-  {
-    switch (featureID)
-    {
-      case VampireLanguagePackage.VLS_TERM__TYPE:
-        return getType();
-    }
-    return super.eGet(featureID, resolve, coreType);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
-  public void eSet(int featureID, Object newValue)
-  {
-    switch (featureID)
-    {
-      case VampireLanguagePackage.VLS_TERM__TYPE:
-        setType((VLSTypeDef)newValue);
-        return;
-    }
-    super.eSet(featureID, newValue);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
-  public void eUnset(int featureID)
-  {
-    switch (featureID)
-    {
-      case VampireLanguagePackage.VLS_TERM__TYPE:
-        setType((VLSTypeDef)null);
-        return;
-    }
-    super.eUnset(featureID);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
-  public boolean eIsSet(int featureID)
-  {
-    switch (featureID)
-    {
-      case VampireLanguagePackage.VLS_TERM__TYPE:
-        return type != null;
-    }
-    return super.eIsSet(featureID);
-  }
 } //VLSTermImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUniversalQuantifierImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUniversalQuantifierImpl.java
index b9bfbe07..e3482fb8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUniversalQuantifierImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUniversalQuantifierImpl.java
@@ -4,8 +4,8 @@
 package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
 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.VLSVariableDeclaration;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
 import java.util.Collection;
@@ -47,7 +47,7 @@ public class VLSUniversalQuantifierImpl extends VLSTermImpl implements VLSUniver
   * @generated
   * @ordered
   */
-  protected EList<VLSVariableDeclaration> variables;
+  protected EList<VLSTffTerm> variables;
  /**
   * The cached value of the '{@link #getOperand() <em>Operand</em>}' containment reference.
@@ -85,11 +85,11 @@ public class VLSUniversalQuantifierImpl extends VLSTermImpl implements VLSUniver
   * <!-- end-user-doc -->
   * @generated
   */
-  public EList<VLSVariableDeclaration> getVariables()
+  public EList<VLSTffTerm> getVariables()
  {
    if (variables == null)
    {
-      variables = new EObjectContainmentEList<VLSVariableDeclaration>(VLSVariableDeclaration.class, this, VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__VARIABLES);
+      variables = new EObjectContainmentEList<VLSTffTerm>(VLSTffTerm.class, this, VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__VARIABLES);
    }
    return variables;
  }
@@ -191,7 +191,7 @@ public class VLSUniversalQuantifierImpl extends VLSTermImpl implements VLSUniver
    {
      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__VARIABLES:
        getVariables().clear();
-        getVariables().addAll((Collection<? extends VLSVariableDeclaration>)newValue);
+        getVariables().addAll((Collection<? extends VLSTffTerm>)newValue);
        return;
      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND:
        setOperand((VLSTerm)newValue);
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableDeclarationImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableDeclarationImpl.java
index 0e6c0ef9..5ebb84c7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableDeclarationImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableDeclarationImpl.java
@@ -3,21 +3,44 @@
 */
 package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
 import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
 /**
 * <!-- begin-user-doc -->
 * An implementation of the model object '<em><b>VLS Variable Declaration</b></em>'.
 * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableDeclarationImpl#getName <em>Name</em>}</li>
+ * </ul>
 *
 * @generated
 */
 public class VLSVariableDeclarationImpl extends VLSDeclarationImpl implements VLSVariableDeclaration
 {
  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected VLSVariable name;
+  /**
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
@@ -38,4 +61,134 @@ public class VLSVariableDeclarationImpl extends VLSDeclarationImpl implements VL
    return VampireLanguagePackage.Literals.VLS_VARIABLE_DECLARATION;
  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSVariable getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetName(VLSVariable newName, NotificationChain msgs)
+  {
+    VLSVariable oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME, oldName, newName);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(VLSVariable newName)
+  {
+    if (newName != name)
+    {
+      NotificationChain msgs = null;
+      if (name != null)
+        msgs = ((InternalEObject)name).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME, null, msgs);
+      if (newName != null)
+        msgs = ((InternalEObject)newName).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME, null, msgs);
+      msgs = basicSetName(newName, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME, newName, newName));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME:
+        return basicSetName(null, msgs);
+    }
+    return super.eInverseRemove(otherEnd, featureID, msgs);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME:
+        return getName();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME:
+        setName((VLSVariable)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME:
+        setName((VLSVariable)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_VARIABLE_DECLARATION__NAME:
+        return name != null;
+    }
+    return super.eIsSet(featureID);
+  }
 } //VLSVariableDeclarationImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableImpl.java
index 1d38ddfb..9ebed3eb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableImpl.java
@@ -3,17 +3,12 @@
 */
 package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTypeDef;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
 import org.eclipse.emf.common.notify.Notification;
-import org.eclipse.emf.common.notify.NotificationChain;
 import org.eclipse.emf.ecore.EClass;
-import org.eclipse.emf.ecore.InternalEObject;
 import org.eclipse.emf.ecore.impl.ENotificationImpl;
@@ -25,25 +20,14 @@ import org.eclipse.emf.ecore.impl.ENotificationImpl;
 * The following features are implemented:
 * </p>
 * <ul>
- *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableImpl#getType <em>Type</em>}</li>
 *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableImpl#getName <em>Name</em>}</li>
 * </ul>
 *
 * @generated
 */
-public class VLSVariableImpl extends VLSVariableDeclarationImpl implements VLSVariable
+public class VLSVariableImpl extends VLSTermImpl implements VLSVariable
 {
  /**
-   * The cached value of the '{@link #getType() <em>Type</em>}' containment reference.
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @see #getType()
-   * @generated
-   * @ordered
-   */
-  protected VLSTypeDef type;
-  /**
   * The default value of the '{@link #getName() <em>Name</em>}' attribute.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -89,54 +73,6 @@ public class VLSVariableImpl extends VLSVariableDeclarationImpl implements VLSVa
   * <!-- end-user-doc -->
   * @generated
   */
-  public VLSTypeDef getType()
-  {
-    return type;
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  public NotificationChain basicSetType(VLSTypeDef newType, NotificationChain msgs)
-  {
-    VLSTypeDef oldType = type;
-    type = newType;
-    if (eNotificationRequired())
-    {
-      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_VARIABLE__TYPE, oldType, newType);
-      if (msgs == null) msgs = notification; else msgs.add(notification);
-    }
-    return msgs;
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  public void setType(VLSTypeDef newType)
-  {
-    if (newType != type)
-    {
-      NotificationChain msgs = null;
-      if (type != null)
-        msgs = ((InternalEObject)type).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_VARIABLE__TYPE, null, msgs);
-      if (newType != null)
-        msgs = ((InternalEObject)newType).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_VARIABLE__TYPE, null, msgs);
-      msgs = basicSetType(newType, msgs);
-      if (msgs != null) msgs.dispatch();
-    }
-    else if (eNotificationRequired())
-      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_VARIABLE__TYPE, newType, newType));
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
  public String getName()
  {
    return name;
@@ -161,28 +97,10 @@ public class VLSVariableImpl extends VLSVariableDeclarationImpl implements VLSVa
   * @generated
   */
  @Override
-  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
-  {
-    switch (featureID)
-    {
-      case VampireLanguagePackage.VLS_VARIABLE__TYPE:
-        return basicSetType(null, msgs);
-    }
-    return super.eInverseRemove(otherEnd, featureID, msgs);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
  public Object eGet(int featureID, boolean resolve, boolean coreType)
  {
    switch (featureID)
    {
-      case VampireLanguagePackage.VLS_VARIABLE__TYPE:
-        return getType();
      case VampireLanguagePackage.VLS_VARIABLE__NAME:
        return getName();
    }
@@ -199,9 +117,6 @@ public class VLSVariableImpl extends VLSVariableDeclarationImpl implements VLSVa
  {
    switch (featureID)
    {
-      case VampireLanguagePackage.VLS_VARIABLE__TYPE:
-        setType((VLSTypeDef)newValue);
-        return;
      case VampireLanguagePackage.VLS_VARIABLE__NAME:
        setName((String)newValue);
        return;
@@ -219,9 +134,6 @@ public class VLSVariableImpl extends VLSVariableDeclarationImpl implements VLSVa
  {
    switch (featureID)
    {
-      case VampireLanguagePackage.VLS_VARIABLE__TYPE:
-        setType((VLSTypeDef)null);
-        return;
      case VampireLanguagePackage.VLS_VARIABLE__NAME:
        setName(NAME_EDEFAULT);
        return;
@@ -239,8 +151,6 @@ public class VLSVariableImpl extends VLSVariableDeclarationImpl implements VLSVa
  {
    switch (featureID)
    {
-      case VampireLanguagePackage.VLS_VARIABLE__TYPE:
-        return type != null;
      case VampireLanguagePackage.VLS_VARIABLE__NAME:
        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
    }
@@ -253,58 +163,6 @@ public class VLSVariableImpl extends VLSVariableDeclarationImpl implements VLSVa
   * @generated
   */
  @Override
-  public int eBaseStructuralFeatureID(int derivedFeatureID, Class<?> baseClass)
-  {
-    if (baseClass == VLSOtherDeclaration.class)
-    {
-      switch (derivedFeatureID)
-      {
-        default: return -1;
-      }
-    }
-    if (baseClass == VLSTerm.class)
-    {
-      switch (derivedFeatureID)
-      {
-        case VampireLanguagePackage.VLS_VARIABLE__TYPE: return VampireLanguagePackage.VLS_TERM__TYPE;
-        default: return -1;
-      }
-    }
-    return super.eBaseStructuralFeatureID(derivedFeatureID, baseClass);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
-  public int eDerivedStructuralFeatureID(int baseFeatureID, Class<?> baseClass)
-  {
-    if (baseClass == VLSOtherDeclaration.class)
-    {
-      switch (baseFeatureID)
-      {
-        default: return -1;
-      }
-    }
-    if (baseClass == VLSTerm.class)
-    {
-      switch (baseFeatureID)
-      {
-        case VampireLanguagePackage.VLS_TERM__TYPE: return VampireLanguagePackage.VLS_VARIABLE__TYPE;
-        default: return -1;
-      }
-    }
-    return super.eDerivedStructuralFeatureID(baseFeatureID, baseClass);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
-  @Override
  public String toString()
  {
    if (eIsProxy()) return super.toString();
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
index 6b2b7085..676b2786 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
@@ -649,6 +649,16 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public EReference getVLSDeclaration_Type()
+  {
+    return (EReference)vlsDeclarationEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public EClass getVLSOtherDeclaration()
  {
    return vlsOtherDeclarationEClass;
@@ -659,6 +669,16 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public EReference getVLSOtherDeclaration_Name()
+  {
+    return (EReference)vlsOtherDeclarationEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public EClass getVLSVariableDeclaration()
  {
    return vlsVariableDeclarationEClass;
@@ -669,6 +689,16 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public EReference getVLSVariableDeclaration_Name()
+  {
+    return (EReference)vlsVariableDeclarationEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public EClass getVLSTypeDef()
  {
    return vlsTypeDefEClass;
@@ -729,16 +759,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
-  public EReference getVLSTerm_Type()
-  {
-    return (EReference)vlsTermEClass.getEStructuralFeatures().get(0);
-  }
-  /**
-   * <!-- begin-user-doc -->
-   * <!-- end-user-doc -->
-   * @generated
-   */
  public EClass getVLSVariable()
  {
    return vlsVariableEClass;
@@ -1445,10 +1465,13 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    vlsTffTermEClass = createEClass(VLS_TFF_TERM);
    vlsDeclarationEClass = createEClass(VLS_DECLARATION);
+    createEReference(vlsDeclarationEClass, VLS_DECLARATION__TYPE);
    vlsOtherDeclarationEClass = createEClass(VLS_OTHER_DECLARATION);
+    createEReference(vlsOtherDeclarationEClass, VLS_OTHER_DECLARATION__NAME);
    vlsVariableDeclarationEClass = createEClass(VLS_VARIABLE_DECLARATION);
+    createEReference(vlsVariableDeclarationEClass, VLS_VARIABLE_DECLARATION__NAME);
    vlsTypeDefEClass = createEClass(VLS_TYPE_DEF);
    createEReference(vlsTypeDefEClass, VLS_TYPE_DEF__TYPE_SIG);
@@ -1457,7 +1480,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    createEReference(vlsTypeDefEClass, VLS_TYPE_DEF__NEXT_TYPE);
    vlsTermEClass = createEClass(VLS_TERM);
-    createEReference(vlsTermEClass, VLS_TERM__TYPE);
    vlsVariableEClass = createEClass(VLS_VARIABLE);
    createEAttribute(vlsVariableEClass, VLS_VARIABLE__NAME);
@@ -1586,8 +1608,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    vlsOtherDeclarationEClass.getESuperTypes().add(this.getVLSDeclaration());
    vlsVariableDeclarationEClass.getESuperTypes().add(this.getVLSDeclaration());
    vlsTermEClass.getESuperTypes().add(this.getVLSTffTerm());
-    vlsTermEClass.getESuperTypes().add(this.getVLSOtherDeclaration());
-    vlsVariableEClass.getESuperTypes().add(this.getVLSVariableDeclaration());
    vlsVariableEClass.getESuperTypes().add(this.getVLSTerm());
    vlsFunctionAsTermEClass.getESuperTypes().add(this.getVLSTerm());
    vlsDefinedTermEClass.getESuperTypes().add(this.getVLSTerm());
@@ -1649,10 +1669,13 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    initEClass(vlsTffTermEClass, VLSTffTerm.class, "VLSTffTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
    initEClass(vlsDeclarationEClass, VLSDeclaration.class, "VLSDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSDeclaration_Type(), this.getVLSTypeDef(), null, "type", null, 0, 1, VLSDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsOtherDeclarationEClass, VLSOtherDeclaration.class, "VLSOtherDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSOtherDeclaration_Name(), this.getVLSTerm(), null, "name", null, 0, 1, VLSOtherDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsVariableDeclarationEClass, VLSVariableDeclaration.class, "VLSVariableDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSVariableDeclaration_Name(), this.getVLSVariable(), null, "name", null, 0, 1, VLSVariableDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsTypeDefEClass, VLSTypeDef.class, "VLSTypeDef", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
    initEReference(getVLSTypeDef_TypeSig(), this.getVLSTypeDef(), null, "typeSig", null, 0, 1, VLSTypeDef.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
@@ -1661,7 +1684,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    initEReference(getVLSTypeDef_NextType(), this.getVLSTerm(), null, "nextType", null, 0, 1, VLSTypeDef.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsTermEClass, VLSTerm.class, "VLSTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
-    initEReference(getVLSTerm_Type(), this.getVLSTypeDef(), null, "type", null, 0, 1, VLSTerm.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsVariableEClass, VLSVariable.class, "VLSVariable", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
    initEAttribute(getVLSVariable_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSVariable.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
@@ -1715,11 +1737,11 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    initEReference(getVLSOr_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSOr.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsUniversalQuantifierEClass, VLSUniversalQuantifier.class, "VLSUniversalQuantifier", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
-    initEReference(getVLSUniversalQuantifier_Variables(), this.getVLSVariableDeclaration(), null, "variables", null, 0, -1, VLSUniversalQuantifier.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSUniversalQuantifier_Variables(), this.getVLSTffTerm(), null, "variables", null, 0, -1, VLSUniversalQuantifier.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEReference(getVLSUniversalQuantifier_Operand(), this.getVLSTerm(), null, "operand", null, 0, 1, VLSUniversalQuantifier.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsExistentialQuantifierEClass, VLSExistentialQuantifier.class, "VLSExistentialQuantifier", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
-    initEReference(getVLSExistentialQuantifier_Variables(), this.getVLSVariableDeclaration(), null, "variables", null, 0, -1, VLSExistentialQuantifier.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSExistentialQuantifier_Variables(), this.getVLSTffTerm(), null, "variables", null, 0, -1, VLSExistentialQuantifier.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEReference(getVLSExistentialQuantifier_Operand(), this.getVLSTerm(), null, "operand", null, 0, 1, VLSExistentialQuantifier.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
    initEClass(vlsUnaryNegationEClass, VLSUnaryNegation.class, "VLSUnaryNegation", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
index e4aae7f8..193ac81b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
@@ -159,8 +159,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
      {
        VLSTerm vlsTerm = (VLSTerm)theEObject;
        T result = caseVLSTerm(vlsTerm);
-        if (result == null) result = caseVLSOtherDeclaration(vlsTerm);
-        if (result == null) result = caseVLSDeclaration(vlsTerm);
        if (result == null) result = caseVLSTffTerm(vlsTerm);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -169,10 +167,7 @@ public class VampireLanguageSwitch<T> extends Switch<T>
      {
        VLSVariable vlsVariable = (VLSVariable)theEObject;
        T result = caseVLSVariable(vlsVariable);
-        if (result == null) result = caseVLSVariableDeclaration(vlsVariable);
        if (result == null) result = caseVLSTerm(vlsVariable);
-        if (result == null) result = caseVLSOtherDeclaration(vlsVariable);
-        if (result == null) result = caseVLSDeclaration(vlsVariable);
        if (result == null) result = caseVLSTffTerm(vlsVariable);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -182,8 +177,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSFunctionAsTerm vlsFunctionAsTerm = (VLSFunctionAsTerm)theEObject;
        T result = caseVLSFunctionAsTerm(vlsFunctionAsTerm);
        if (result == null) result = caseVLSTerm(vlsFunctionAsTerm);
-        if (result == null) result = caseVLSOtherDeclaration(vlsFunctionAsTerm);
-        if (result == null) result = caseVLSDeclaration(vlsFunctionAsTerm);
        if (result == null) result = caseVLSTffTerm(vlsFunctionAsTerm);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -193,8 +186,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSDefinedTerm vlsDefinedTerm = (VLSDefinedTerm)theEObject;
        T result = caseVLSDefinedTerm(vlsDefinedTerm);
        if (result == null) result = caseVLSTerm(vlsDefinedTerm);
-        if (result == null) result = caseVLSOtherDeclaration(vlsDefinedTerm);
-        if (result == null) result = caseVLSDeclaration(vlsDefinedTerm);
        if (result == null) result = caseVLSTffTerm(vlsDefinedTerm);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -236,8 +227,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSEquivalent vlsEquivalent = (VLSEquivalent)theEObject;
        T result = caseVLSEquivalent(vlsEquivalent);
        if (result == null) result = caseVLSTerm(vlsEquivalent);
-        if (result == null) result = caseVLSOtherDeclaration(vlsEquivalent);
-        if (result == null) result = caseVLSDeclaration(vlsEquivalent);
        if (result == null) result = caseVLSTffTerm(vlsEquivalent);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -247,8 +236,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSImplies vlsImplies = (VLSImplies)theEObject;
        T result = caseVLSImplies(vlsImplies);
        if (result == null) result = caseVLSTerm(vlsImplies);
-        if (result == null) result = caseVLSOtherDeclaration(vlsImplies);
-        if (result == null) result = caseVLSDeclaration(vlsImplies);
        if (result == null) result = caseVLSTffTerm(vlsImplies);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -258,8 +245,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSRevImplies vlsRevImplies = (VLSRevImplies)theEObject;
        T result = caseVLSRevImplies(vlsRevImplies);
        if (result == null) result = caseVLSTerm(vlsRevImplies);
-        if (result == null) result = caseVLSOtherDeclaration(vlsRevImplies);
-        if (result == null) result = caseVLSDeclaration(vlsRevImplies);
        if (result == null) result = caseVLSTffTerm(vlsRevImplies);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -269,8 +254,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSXnor vlsXnor = (VLSXnor)theEObject;
        T result = caseVLSXnor(vlsXnor);
        if (result == null) result = caseVLSTerm(vlsXnor);
-        if (result == null) result = caseVLSOtherDeclaration(vlsXnor);
-        if (result == null) result = caseVLSDeclaration(vlsXnor);
        if (result == null) result = caseVLSTffTerm(vlsXnor);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -280,8 +263,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSNor vlsNor = (VLSNor)theEObject;
        T result = caseVLSNor(vlsNor);
        if (result == null) result = caseVLSTerm(vlsNor);
-        if (result == null) result = caseVLSOtherDeclaration(vlsNor);
-        if (result == null) result = caseVLSDeclaration(vlsNor);
        if (result == null) result = caseVLSTffTerm(vlsNor);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -291,8 +272,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSNand vlsNand = (VLSNand)theEObject;
        T result = caseVLSNand(vlsNand);
        if (result == null) result = caseVLSTerm(vlsNand);
-        if (result == null) result = caseVLSOtherDeclaration(vlsNand);
-        if (result == null) result = caseVLSDeclaration(vlsNand);
        if (result == null) result = caseVLSTffTerm(vlsNand);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -302,8 +281,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSAnd vlsAnd = (VLSAnd)theEObject;
        T result = caseVLSAnd(vlsAnd);
        if (result == null) result = caseVLSTerm(vlsAnd);
-        if (result == null) result = caseVLSOtherDeclaration(vlsAnd);
-        if (result == null) result = caseVLSDeclaration(vlsAnd);
        if (result == null) result = caseVLSTffTerm(vlsAnd);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -313,8 +290,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSOr vlsOr = (VLSOr)theEObject;
        T result = caseVLSOr(vlsOr);
        if (result == null) result = caseVLSTerm(vlsOr);
-        if (result == null) result = caseVLSOtherDeclaration(vlsOr);
-        if (result == null) result = caseVLSDeclaration(vlsOr);
        if (result == null) result = caseVLSTffTerm(vlsOr);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -324,8 +299,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSUniversalQuantifier vlsUniversalQuantifier = (VLSUniversalQuantifier)theEObject;
        T result = caseVLSUniversalQuantifier(vlsUniversalQuantifier);
        if (result == null) result = caseVLSTerm(vlsUniversalQuantifier);
-        if (result == null) result = caseVLSOtherDeclaration(vlsUniversalQuantifier);
-        if (result == null) result = caseVLSDeclaration(vlsUniversalQuantifier);
        if (result == null) result = caseVLSTffTerm(vlsUniversalQuantifier);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -335,8 +308,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSExistentialQuantifier vlsExistentialQuantifier = (VLSExistentialQuantifier)theEObject;
        T result = caseVLSExistentialQuantifier(vlsExistentialQuantifier);
        if (result == null) result = caseVLSTerm(vlsExistentialQuantifier);
-        if (result == null) result = caseVLSOtherDeclaration(vlsExistentialQuantifier);
-        if (result == null) result = caseVLSDeclaration(vlsExistentialQuantifier);
        if (result == null) result = caseVLSTffTerm(vlsExistentialQuantifier);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -346,8 +317,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSUnaryNegation vlsUnaryNegation = (VLSUnaryNegation)theEObject;
        T result = caseVLSUnaryNegation(vlsUnaryNegation);
        if (result == null) result = caseVLSTerm(vlsUnaryNegation);
-        if (result == null) result = caseVLSOtherDeclaration(vlsUnaryNegation);
-        if (result == null) result = caseVLSDeclaration(vlsUnaryNegation);
        if (result == null) result = caseVLSTffTerm(vlsUnaryNegation);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -357,8 +326,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSInequality vlsInequality = (VLSInequality)theEObject;
        T result = caseVLSInequality(vlsInequality);
        if (result == null) result = caseVLSTerm(vlsInequality);
-        if (result == null) result = caseVLSOtherDeclaration(vlsInequality);
-        if (result == null) result = caseVLSDeclaration(vlsInequality);
        if (result == null) result = caseVLSTffTerm(vlsInequality);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -368,8 +335,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSEquality vlsEquality = (VLSEquality)theEObject;
        T result = caseVLSEquality(vlsEquality);
        if (result == null) result = caseVLSTerm(vlsEquality);
-        if (result == null) result = caseVLSOtherDeclaration(vlsEquality);
-        if (result == null) result = caseVLSDeclaration(vlsEquality);
        if (result == null) result = caseVLSTffTerm(vlsEquality);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -379,8 +344,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSAssignment vlsAssignment = (VLSAssignment)theEObject;
        T result = caseVLSAssignment(vlsAssignment);
        if (result == null) result = caseVLSTerm(vlsAssignment);
-        if (result == null) result = caseVLSOtherDeclaration(vlsAssignment);
-        if (result == null) result = caseVLSDeclaration(vlsAssignment);
        if (result == null) result = caseVLSTffTerm(vlsAssignment);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -390,8 +353,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSConstant vlsConstant = (VLSConstant)theEObject;
        T result = caseVLSConstant(vlsConstant);
        if (result == null) result = caseVLSTerm(vlsConstant);
-        if (result == null) result = caseVLSOtherDeclaration(vlsConstant);
-        if (result == null) result = caseVLSDeclaration(vlsConstant);
        if (result == null) result = caseVLSTffTerm(vlsConstant);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -401,8 +362,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSTrue vlsTrue = (VLSTrue)theEObject;
        T result = caseVLSTrue(vlsTrue);
        if (result == null) result = caseVLSTerm(vlsTrue);
-        if (result == null) result = caseVLSOtherDeclaration(vlsTrue);
-        if (result == null) result = caseVLSDeclaration(vlsTrue);
        if (result == null) result = caseVLSTffTerm(vlsTrue);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -412,8 +371,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSFalse vlsFalse = (VLSFalse)theEObject;
        T result = caseVLSFalse(vlsFalse);
        if (result == null) result = caseVLSTerm(vlsFalse);
-        if (result == null) result = caseVLSOtherDeclaration(vlsFalse);
-        if (result == null) result = caseVLSDeclaration(vlsFalse);
        if (result == null) result = caseVLSTffTerm(vlsFalse);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -423,8 +380,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSFunction vlsFunction = (VLSFunction)theEObject;
        T result = caseVLSFunction(vlsFunction);
        if (result == null) result = caseVLSTerm(vlsFunction);
-        if (result == null) result = caseVLSOtherDeclaration(vlsFunction);
-        if (result == null) result = caseVLSDeclaration(vlsFunction);
        if (result == null) result = caseVLSTffTerm(vlsFunction);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -434,8 +389,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        VLSLess vlsLess = (VLSLess)theEObject;
        T result = caseVLSLess(vlsLess);
        if (result == null) result = caseVLSTerm(vlsLess);
-        if (result == null) result = caseVLSOtherDeclaration(vlsLess);
-        if (result == null) result = caseVLSDeclaration(vlsLess);
        if (result == null) result = caseVLSTffTerm(vlsLess);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -446,8 +399,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        T result = caseVLSInt(vlsInt);
        if (result == null) result = caseVLSDefinedTerm(vlsInt);
        if (result == null) result = caseVLSTerm(vlsInt);
-        if (result == null) result = caseVLSOtherDeclaration(vlsInt);
-        if (result == null) result = caseVLSDeclaration(vlsInt);
        if (result == null) result = caseVLSTffTerm(vlsInt);
        if (result == null) result = defaultCase(theEObject);
        return result;
@@ -458,8 +409,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        T result = caseVLSDoubleQuote(vlsDoubleQuote);
        if (result == null) result = caseVLSDefinedTerm(vlsDoubleQuote);
        if (result == null) result = caseVLSTerm(vlsDoubleQuote);
-        if (result == null) result = caseVLSOtherDeclaration(vlsDoubleQuote);
-        if (result == null) result = caseVLSDeclaration(vlsDoubleQuote);
        if (result == null) result = caseVLSTffTerm(vlsDoubleQuote);
        if (result == null) result = defaultCase(theEObject);
        return result;