35 files changed, 8675 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAndImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAndImpl.java
new file mode 100644
index 00000000..951de940
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAndImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
+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 And</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAndImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAndImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSAndImpl extends VLSTermImpl implements VLSAnd
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSAndImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_AND;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_AND__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_AND__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_AND__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_AND__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_AND__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_AND__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_AND__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_AND__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_AND__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_AND__RIGHT:
+        return basicSetRight(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_AND__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_AND__RIGHT:
+        return getRight();
+    }
+    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_AND__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_AND__RIGHT:
+        setRight((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_AND__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_AND__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_AND__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_AND__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSAndImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAnnotationImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAnnotationImpl.java
new file mode 100644
index 00000000..092dd4c9
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAnnotationImpl.java
@@ -0,0 +1,311 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnnotation;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.impl.MinimalEObjectImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Annotation</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAnnotationImpl#getName <em>Name</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAnnotationImpl#getFollowup <em>Followup</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAnnotationImpl#getTerms <em>Terms</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSAnnotationImpl extends MinimalEObjectImpl.Container implements VLSAnnotation
+{
+  /**
+   * The default value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected static final String NAME_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected String name = NAME_EDEFAULT;
+  /**
+   * The cached value of the '{@link #getFollowup() <em>Followup</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFollowup()
+   * @generated
+   * @ordered
+   */
+  protected VLSAnnotation followup;
+  /**
+   * The cached value of the '{@link #getTerms() <em>Terms</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getTerms()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSAnnotation> terms;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSAnnotationImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_ANNOTATION;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(String newName)
+  {
+    String oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_ANNOTATION__NAME, oldName, name));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSAnnotation getFollowup()
+  {
+    return followup;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetFollowup(VLSAnnotation newFollowup, NotificationChain msgs)
+  {
+    VLSAnnotation oldFollowup = followup;
+    followup = newFollowup;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP, oldFollowup, newFollowup);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setFollowup(VLSAnnotation newFollowup)
+  {
+    if (newFollowup != followup)
+    {
+      NotificationChain msgs = null;
+      if (followup != null)
+        msgs = ((InternalEObject)followup).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP, null, msgs);
+      if (newFollowup != null)
+        msgs = ((InternalEObject)newFollowup).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP, null, msgs);
+      msgs = basicSetFollowup(newFollowup, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP, newFollowup, newFollowup));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSAnnotation> getTerms()
+  {
+    if (terms == null)
+    {
+      terms = new EObjectContainmentEList<VLSAnnotation>(VLSAnnotation.class, this, VampireLanguagePackage.VLS_ANNOTATION__TERMS);
+    }
+    return terms;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP:
+        return basicSetFollowup(null, msgs);
+      case VampireLanguagePackage.VLS_ANNOTATION__TERMS:
+        return ((InternalEList<?>)getTerms()).basicRemove(otherEnd, 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_ANNOTATION__NAME:
+        return getName();
+      case VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP:
+        return getFollowup();
+      case VampireLanguagePackage.VLS_ANNOTATION__TERMS:
+        return getTerms();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_ANNOTATION__NAME:
+        setName((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP:
+        setFollowup((VLSAnnotation)newValue);
+        return;
+      case VampireLanguagePackage.VLS_ANNOTATION__TERMS:
+        getTerms().clear();
+        getTerms().addAll((Collection<? extends VLSAnnotation>)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_ANNOTATION__NAME:
+        setName(NAME_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP:
+        setFollowup((VLSAnnotation)null);
+        return;
+      case VampireLanguagePackage.VLS_ANNOTATION__TERMS:
+        getTerms().clear();
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_ANNOTATION__NAME:
+        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
+      case VampireLanguagePackage.VLS_ANNOTATION__FOLLOWUP:
+        return followup != null;
+      case VampireLanguagePackage.VLS_ANNOTATION__TERMS:
+        return terms != null && !terms.isEmpty();
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (name: ");
+    result.append(name);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSAnnotationImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAssignmentImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAssignmentImpl.java
new file mode 100644
index 00000000..e6dbb58d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSAssignmentImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAssignment;
+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 Assignment</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAssignmentImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAssignmentImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSAssignmentImpl extends VLSTermImpl implements VLSAssignment
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSAssignmentImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_ASSIGNMENT;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_ASSIGNMENT__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_ASSIGNMENT__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_ASSIGNMENT__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_ASSIGNMENT__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_ASSIGNMENT__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT:
+        return basicSetRight(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_ASSIGNMENT__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT:
+        return getRight();
+    }
+    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_ASSIGNMENT__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT:
+        setRight((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_ASSIGNMENT__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_ASSIGNMENT__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_ASSIGNMENT__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSAssignmentImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSCommentImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSCommentImpl.java
new file mode 100644
index 00000000..9599872d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSCommentImpl.java
@@ -0,0 +1,178 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.impl.MinimalEObjectImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Comment</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSCommentImpl#getComment <em>Comment</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSCommentImpl extends MinimalEObjectImpl.Container implements VLSComment
+{
+  /**
+   * The default value of the '{@link #getComment() <em>Comment</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getComment()
+   * @generated
+   * @ordered
+   */
+  protected static final String COMMENT_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getComment() <em>Comment</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getComment()
+   * @generated
+   * @ordered
+   */
+  protected String comment = COMMENT_EDEFAULT;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSCommentImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_COMMENT;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getComment()
+  {
+    return comment;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setComment(String newComment)
+  {
+    String oldComment = comment;
+    comment = newComment;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_COMMENT__COMMENT, oldComment, comment));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_COMMENT__COMMENT:
+        return getComment();
+    }
+    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_COMMENT__COMMENT:
+        setComment((String)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_COMMENT__COMMENT:
+        setComment(COMMENT_EDEFAULT);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_COMMENT__COMMENT:
+        return COMMENT_EDEFAULT == null ? comment != null : !COMMENT_EDEFAULT.equals(comment);
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (comment: ");
+    result.append(comment);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSCommentImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSConstantImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSConstantImpl.java
new file mode 100644
index 00000000..b9bcf512
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSConstantImpl.java
@@ -0,0 +1,177 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Constant</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSConstantImpl#getName <em>Name</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSConstantImpl extends VLSTermImpl implements VLSConstant
+{
+  /**
+   * The default value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected static final String NAME_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected String name = NAME_EDEFAULT;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSConstantImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_CONSTANT;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(String newName)
+  {
+    String oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_CONSTANT__NAME, oldName, name));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_CONSTANT__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_CONSTANT__NAME:
+        setName((String)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_CONSTANT__NAME:
+        setName(NAME_EDEFAULT);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_CONSTANT__NAME:
+        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (name: ");
+    result.append(name);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSConstantImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDefinedTermImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDefinedTermImpl.java
new file mode 100644
index 00000000..444e2b85
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDefinedTermImpl.java
@@ -0,0 +1,177 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDefinedTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Defined Term</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSDefinedTermImpl#getValue <em>Value</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSDefinedTermImpl extends VLSTermImpl implements VLSDefinedTerm
+{
+  /**
+   * The default value of the '{@link #getValue() <em>Value</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getValue()
+   * @generated
+   * @ordered
+   */
+  protected static final String VALUE_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getValue() <em>Value</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getValue()
+   * @generated
+   * @ordered
+   */
+  protected String value = VALUE_EDEFAULT;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSDefinedTermImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_DEFINED_TERM;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getValue()
+  {
+    return value;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setValue(String newValue)
+  {
+    String oldValue = value;
+    value = newValue;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_DEFINED_TERM__VALUE, oldValue, value));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DEFINED_TERM__VALUE:
+        return getValue();
+    }
+    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_DEFINED_TERM__VALUE:
+        setValue((String)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DEFINED_TERM__VALUE:
+        setValue(VALUE_EDEFAULT);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_DEFINED_TERM__VALUE:
+        return VALUE_EDEFAULT == null ? value != null : !VALUE_EDEFAULT.equals(value);
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (value: ");
+    result.append(value);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSDefinedTermImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDoubleQuoteImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDoubleQuoteImpl.java
new file mode 100644
index 00000000..db99a631
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSDoubleQuoteImpl.java
@@ -0,0 +1,41 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.ecore.EClass;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Double Quote</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSDoubleQuoteImpl extends VLSDefinedTermImpl implements VLSDoubleQuote
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSDoubleQuoteImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_DOUBLE_QUOTE;
+  }
+} //VLSDoubleQuoteImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSEqualityImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSEqualityImpl.java
new file mode 100644
index 00000000..ba729215
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSEqualityImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
+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 Equality</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSEqualityImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSEqualityImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSEqualityImpl extends VLSTermImpl implements VLSEquality
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSEqualityImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_EQUALITY;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUALITY__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUALITY__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUALITY__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUALITY__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUALITY__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUALITY__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUALITY__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUALITY__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_EQUALITY__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_EQUALITY__RIGHT:
+        return basicSetRight(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_EQUALITY__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_EQUALITY__RIGHT:
+        return getRight();
+    }
+    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_EQUALITY__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_EQUALITY__RIGHT:
+        setRight((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_EQUALITY__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_EQUALITY__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_EQUALITY__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_EQUALITY__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSEqualityImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSEquivalentImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSEquivalentImpl.java
new file mode 100644
index 00000000..2ab11117
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSEquivalentImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
+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 Equivalent</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSEquivalentImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSEquivalentImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSEquivalentImpl extends VLSTermImpl implements VLSEquivalent
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSEquivalentImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_EQUIVALENT;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUIVALENT__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUIVALENT__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUIVALENT__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUIVALENT__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUIVALENT__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUIVALENT__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EQUIVALENT__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EQUIVALENT__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_EQUIVALENT__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_EQUIVALENT__RIGHT:
+        return basicSetRight(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_EQUIVALENT__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_EQUIVALENT__RIGHT:
+        return getRight();
+    }
+    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_EQUIVALENT__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_EQUIVALENT__RIGHT:
+        setRight((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_EQUIVALENT__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_EQUIVALENT__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_EQUIVALENT__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_EQUIVALENT__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSEquivalentImpl
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
new file mode 100644
index 00000000..34670d8b
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSExistentialQuantifierImpl.java
@@ -0,0 +1,241 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+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.VLSVariable;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Existential Quantifier</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSExistentialQuantifierImpl#getVariables <em>Variables</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSExistentialQuantifierImpl#getOperand <em>Operand</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSExistentialQuantifierImpl extends VLSTermImpl implements VLSExistentialQuantifier
+{
+  /**
+   * The cached value of the '{@link #getVariables() <em>Variables</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getVariables()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSVariable> variables;
+  /**
+   * The cached value of the '{@link #getOperand() <em>Operand</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getOperand()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm operand;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSExistentialQuantifierImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_EXISTENTIAL_QUANTIFIER;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSVariable> getVariables()
+  {
+    if (variables == null)
+    {
+      variables = new EObjectContainmentEList<VLSVariable>(VLSVariable.class, this, VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__VARIABLES);
+    }
+    return variables;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getOperand()
+  {
+    return operand;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetOperand(VLSTerm newOperand, NotificationChain msgs)
+  {
+    VLSTerm oldOperand = operand;
+    operand = newOperand;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND, oldOperand, newOperand);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setOperand(VLSTerm newOperand)
+  {
+    if (newOperand != operand)
+    {
+      NotificationChain msgs = null;
+      if (operand != null)
+        msgs = ((InternalEObject)operand).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND, null, msgs);
+      if (newOperand != null)
+        msgs = ((InternalEObject)newOperand).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND, null, msgs);
+      msgs = basicSetOperand(newOperand, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND, newOperand, newOperand));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__VARIABLES:
+        return ((InternalEList<?>)getVariables()).basicRemove(otherEnd, msgs);
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND:
+        return basicSetOperand(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_EXISTENTIAL_QUANTIFIER__VARIABLES:
+        return getVariables();
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND:
+        return getOperand();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__VARIABLES:
+        getVariables().clear();
+        getVariables().addAll((Collection<? extends VLSVariable>)newValue);
+        return;
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND:
+        setOperand((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_EXISTENTIAL_QUANTIFIER__VARIABLES:
+        getVariables().clear();
+        return;
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND:
+        setOperand((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__VARIABLES:
+        return variables != null && !variables.isEmpty();
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER__OPERAND:
+        return operand != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSExistentialQuantifierImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFalseImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFalseImpl.java
new file mode 100644
index 00000000..1db5a6b4
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFalseImpl.java
@@ -0,0 +1,41 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFalse;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.ecore.EClass;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS False</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSFalseImpl extends VLSTermImpl implements VLSFalse
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSFalseImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_FALSE;
+  }
+} //VLSFalseImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFofFormulaImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFofFormulaImpl.java
new file mode 100644
index 00000000..beef8908
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFofFormulaImpl.java
@@ -0,0 +1,394 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnnotation;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
+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;
+import org.eclipse.emf.ecore.impl.MinimalEObjectImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Fof Formula</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl#getName <em>Name</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl#getFofRole <em>Fof Role</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl#getFofFormula <em>Fof Formula</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl#getAnnotations <em>Annotations</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSFofFormulaImpl extends MinimalEObjectImpl.Container implements VLSFofFormula
+{
+  /**
+   * The default value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected static final String NAME_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected String name = NAME_EDEFAULT;
+  /**
+   * The default value of the '{@link #getFofRole() <em>Fof Role</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFofRole()
+   * @generated
+   * @ordered
+   */
+  protected static final String FOF_ROLE_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getFofRole() <em>Fof Role</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFofRole()
+   * @generated
+   * @ordered
+   */
+  protected String fofRole = FOF_ROLE_EDEFAULT;
+  /**
+   * The cached value of the '{@link #getFofFormula() <em>Fof Formula</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFofFormula()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm fofFormula;
+  /**
+   * The cached value of the '{@link #getAnnotations() <em>Annotations</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getAnnotations()
+   * @generated
+   * @ordered
+   */
+  protected VLSAnnotation annotations;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSFofFormulaImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_FOF_FORMULA;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(String newName)
+  {
+    String oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FOF_FORMULA__NAME, oldName, name));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getFofRole()
+  {
+    return fofRole;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setFofRole(String newFofRole)
+  {
+    String oldFofRole = fofRole;
+    fofRole = newFofRole;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FOF_FORMULA__FOF_ROLE, oldFofRole, fofRole));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getFofFormula()
+  {
+    return fofFormula;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetFofFormula(VLSTerm newFofFormula, NotificationChain msgs)
+  {
+    VLSTerm oldFofFormula = fofFormula;
+    fofFormula = newFofFormula;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA, oldFofFormula, newFofFormula);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setFofFormula(VLSTerm newFofFormula)
+  {
+    if (newFofFormula != fofFormula)
+    {
+      NotificationChain msgs = null;
+      if (fofFormula != null)
+        msgs = ((InternalEObject)fofFormula).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA, null, msgs);
+      if (newFofFormula != null)
+        msgs = ((InternalEObject)newFofFormula).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA, null, msgs);
+      msgs = basicSetFofFormula(newFofFormula, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA, newFofFormula, newFofFormula));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSAnnotation getAnnotations()
+  {
+    return annotations;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetAnnotations(VLSAnnotation newAnnotations, NotificationChain msgs)
+  {
+    VLSAnnotation oldAnnotations = annotations;
+    annotations = newAnnotations;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS, oldAnnotations, newAnnotations);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setAnnotations(VLSAnnotation newAnnotations)
+  {
+    if (newAnnotations != annotations)
+    {
+      NotificationChain msgs = null;
+      if (annotations != null)
+        msgs = ((InternalEObject)annotations).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS, null, msgs);
+      if (newAnnotations != null)
+        msgs = ((InternalEObject)newAnnotations).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS, null, msgs);
+      msgs = basicSetAnnotations(newAnnotations, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS, newAnnotations, newAnnotations));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA:
+        return basicSetFofFormula(null, msgs);
+      case VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS:
+        return basicSetAnnotations(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_FOF_FORMULA__NAME:
+        return getName();
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_ROLE:
+        return getFofRole();
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA:
+        return getFofFormula();
+      case VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS:
+        return getAnnotations();
+    }
+    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_FOF_FORMULA__NAME:
+        setName((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_ROLE:
+        setFofRole((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA:
+        setFofFormula((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS:
+        setAnnotations((VLSAnnotation)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FOF_FORMULA__NAME:
+        setName(NAME_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_ROLE:
+        setFofRole(FOF_ROLE_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA:
+        setFofFormula((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS:
+        setAnnotations((VLSAnnotation)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FOF_FORMULA__NAME:
+        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_ROLE:
+        return FOF_ROLE_EDEFAULT == null ? fofRole != null : !FOF_ROLE_EDEFAULT.equals(fofRole);
+      case VampireLanguagePackage.VLS_FOF_FORMULA__FOF_FORMULA:
+        return fofFormula != null;
+      case VampireLanguagePackage.VLS_FOF_FORMULA__ANNOTATIONS:
+        return annotations != null;
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (name: ");
+    result.append(name);
+    result.append(", fofRole: ");
+    result.append(fofRole);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSFofFormulaImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFunctionFofImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFunctionFofImpl.java
new file mode 100644
index 00000000..6d1c538b
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFunctionFofImpl.java
@@ -0,0 +1,240 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Function Fof</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFunctionFofImpl#getFunctor <em>Functor</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFunctionFofImpl#getTerms <em>Terms</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSFunctionFofImpl extends VLSTermImpl implements VLSFunctionFof
+{
+  /**
+   * The default value of the '{@link #getFunctor() <em>Functor</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFunctor()
+   * @generated
+   * @ordered
+   */
+  protected static final String FUNCTOR_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getFunctor() <em>Functor</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFunctor()
+   * @generated
+   * @ordered
+   */
+  protected String functor = FUNCTOR_EDEFAULT;
+  /**
+   * The cached value of the '{@link #getTerms() <em>Terms</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getTerms()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSTerm> terms;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSFunctionFofImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_FUNCTION_FOF;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getFunctor()
+  {
+    return functor;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setFunctor(String newFunctor)
+  {
+    String oldFunctor = functor;
+    functor = newFunctor;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FUNCTION_FOF__FUNCTOR, oldFunctor, functor));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSTerm> getTerms()
+  {
+    if (terms == null)
+    {
+      terms = new EObjectContainmentEList<VLSTerm>(VLSTerm.class, this, VampireLanguagePackage.VLS_FUNCTION_FOF__TERMS);
+    }
+    return terms;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FUNCTION_FOF__TERMS:
+        return ((InternalEList<?>)getTerms()).basicRemove(otherEnd, 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_FUNCTION_FOF__FUNCTOR:
+        return getFunctor();
+      case VampireLanguagePackage.VLS_FUNCTION_FOF__TERMS:
+        return getTerms();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FUNCTION_FOF__FUNCTOR:
+        setFunctor((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_FUNCTION_FOF__TERMS:
+        getTerms().clear();
+        getTerms().addAll((Collection<? extends 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_FUNCTION_FOF__FUNCTOR:
+        setFunctor(FUNCTOR_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_FUNCTION_FOF__TERMS:
+        getTerms().clear();
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FUNCTION_FOF__FUNCTOR:
+        return FUNCTOR_EDEFAULT == null ? functor != null : !FUNCTOR_EDEFAULT.equals(functor);
+      case VampireLanguagePackage.VLS_FUNCTION_FOF__TERMS:
+        return terms != null && !terms.isEmpty();
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (functor: ");
+    result.append(functor);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSFunctionFofImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFunctionImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFunctionImpl.java
new file mode 100644
index 00000000..49da58d4
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFunctionImpl.java
@@ -0,0 +1,240 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Function</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFunctionImpl#getConstant <em>Constant</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFunctionImpl#getTerms <em>Terms</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSFunctionImpl extends VLSTermImpl implements VLSFunction
+{
+  /**
+   * The default value of the '{@link #getConstant() <em>Constant</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getConstant()
+   * @generated
+   * @ordered
+   */
+  protected static final String CONSTANT_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getConstant() <em>Constant</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getConstant()
+   * @generated
+   * @ordered
+   */
+  protected String constant = CONSTANT_EDEFAULT;
+  /**
+   * The cached value of the '{@link #getTerms() <em>Terms</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getTerms()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSTerm> terms;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSFunctionImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_FUNCTION;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getConstant()
+  {
+    return constant;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setConstant(String newConstant)
+  {
+    String oldConstant = constant;
+    constant = newConstant;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_FUNCTION__CONSTANT, oldConstant, constant));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSTerm> getTerms()
+  {
+    if (terms == null)
+    {
+      terms = new EObjectContainmentEList<VLSTerm>(VLSTerm.class, this, VampireLanguagePackage.VLS_FUNCTION__TERMS);
+    }
+    return terms;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FUNCTION__TERMS:
+        return ((InternalEList<?>)getTerms()).basicRemove(otherEnd, 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_FUNCTION__CONSTANT:
+        return getConstant();
+      case VampireLanguagePackage.VLS_FUNCTION__TERMS:
+        return getTerms();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FUNCTION__CONSTANT:
+        setConstant((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_FUNCTION__TERMS:
+        getTerms().clear();
+        getTerms().addAll((Collection<? extends 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_FUNCTION__CONSTANT:
+        setConstant(CONSTANT_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_FUNCTION__TERMS:
+        getTerms().clear();
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_FUNCTION__CONSTANT:
+        return CONSTANT_EDEFAULT == null ? constant != null : !CONSTANT_EDEFAULT.equals(constant);
+      case VampireLanguagePackage.VLS_FUNCTION__TERMS:
+        return terms != null && !terms.isEmpty();
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (constant: ");
+    result.append(constant);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSFunctionImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSImpliesImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSImpliesImpl.java
new file mode 100644
index 00000000..3c8d9193
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSImpliesImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
+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 Implies</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSImpliesImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSImpliesImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSImpliesImpl extends VLSTermImpl implements VLSImplies
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSImpliesImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_IMPLIES;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_IMPLIES__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_IMPLIES__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_IMPLIES__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_IMPLIES__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_IMPLIES__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_IMPLIES__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_IMPLIES__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_IMPLIES__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_IMPLIES__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_IMPLIES__RIGHT:
+        return basicSetRight(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_IMPLIES__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_IMPLIES__RIGHT:
+        return getRight();
+    }
+    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_IMPLIES__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_IMPLIES__RIGHT:
+        setRight((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_IMPLIES__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_IMPLIES__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_IMPLIES__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_IMPLIES__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSImpliesImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSIncludeImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSIncludeImpl.java
new file mode 100644
index 00000000..b37d97b4
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSIncludeImpl.java
@@ -0,0 +1,241 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.impl.MinimalEObjectImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Include</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSIncludeImpl#getFileName <em>File Name</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSIncludeImpl#getNames <em>Names</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSIncludeImpl extends MinimalEObjectImpl.Container implements VLSInclude
+{
+  /**
+   * The default value of the '{@link #getFileName() <em>File Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFileName()
+   * @generated
+   * @ordered
+   */
+  protected static final String FILE_NAME_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getFileName() <em>File Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFileName()
+   * @generated
+   * @ordered
+   */
+  protected String fileName = FILE_NAME_EDEFAULT;
+  /**
+   * The cached value of the '{@link #getNames() <em>Names</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getNames()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSName> names;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSIncludeImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_INCLUDE;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getFileName()
+  {
+    return fileName;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setFileName(String newFileName)
+  {
+    String oldFileName = fileName;
+    fileName = newFileName;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_INCLUDE__FILE_NAME, oldFileName, fileName));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSName> getNames()
+  {
+    if (names == null)
+    {
+      names = new EObjectContainmentEList<VLSName>(VLSName.class, this, VampireLanguagePackage.VLS_INCLUDE__NAMES);
+    }
+    return names;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_INCLUDE__NAMES:
+        return ((InternalEList<?>)getNames()).basicRemove(otherEnd, 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_INCLUDE__FILE_NAME:
+        return getFileName();
+      case VampireLanguagePackage.VLS_INCLUDE__NAMES:
+        return getNames();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_INCLUDE__FILE_NAME:
+        setFileName((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_INCLUDE__NAMES:
+        getNames().clear();
+        getNames().addAll((Collection<? extends VLSName>)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_INCLUDE__FILE_NAME:
+        setFileName(FILE_NAME_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_INCLUDE__NAMES:
+        getNames().clear();
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_INCLUDE__FILE_NAME:
+        return FILE_NAME_EDEFAULT == null ? fileName != null : !FILE_NAME_EDEFAULT.equals(fileName);
+      case VampireLanguagePackage.VLS_INCLUDE__NAMES:
+        return names != null && !names.isEmpty();
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (fileName: ");
+    result.append(fileName);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSIncludeImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSInequalityImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSInequalityImpl.java
new file mode 100644
index 00000000..ba409780
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSInequalityImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality;
+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 Inequality</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSInequalityImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSInequalityImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSInequalityImpl extends VLSTermImpl implements VLSInequality
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSInequalityImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_INEQUALITY;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_INEQUALITY__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_INEQUALITY__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_INEQUALITY__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_INEQUALITY__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_INEQUALITY__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_INEQUALITY__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_INEQUALITY__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_INEQUALITY__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_INEQUALITY__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_INEQUALITY__RIGHT:
+        return basicSetRight(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_INEQUALITY__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_INEQUALITY__RIGHT:
+        return getRight();
+    }
+    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_INEQUALITY__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_INEQUALITY__RIGHT:
+        setRight((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_INEQUALITY__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_INEQUALITY__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_INEQUALITY__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_INEQUALITY__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSInequalityImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSIntImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSIntImpl.java
new file mode 100644
index 00000000..a513549a
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSIntImpl.java
@@ -0,0 +1,41 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.ecore.EClass;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Int</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSIntImpl extends VLSDefinedTermImpl implements VLSInt
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSIntImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_INT;
+  }
+} //VLSIntImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSLessImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSLessImpl.java
new file mode 100644
index 00000000..71f2b9c8
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSLessImpl.java
@@ -0,0 +1,240 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSLess;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Less</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSLessImpl#getName <em>Name</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSLessImpl#getTerms <em>Terms</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSLessImpl extends VLSTermImpl implements VLSLess
+{
+  /**
+   * The default value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected static final String NAME_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected String name = NAME_EDEFAULT;
+  /**
+   * The cached value of the '{@link #getTerms() <em>Terms</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getTerms()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSTerm> terms;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSLessImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_LESS;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(String newName)
+  {
+    String oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_LESS__NAME, oldName, name));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSTerm> getTerms()
+  {
+    if (terms == null)
+    {
+      terms = new EObjectContainmentEList<VLSTerm>(VLSTerm.class, this, VampireLanguagePackage.VLS_LESS__TERMS);
+    }
+    return terms;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_LESS__TERMS:
+        return ((InternalEList<?>)getTerms()).basicRemove(otherEnd, 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_LESS__NAME:
+        return getName();
+      case VampireLanguagePackage.VLS_LESS__TERMS:
+        return getTerms();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_LESS__NAME:
+        setName((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_LESS__TERMS:
+        getTerms().clear();
+        getTerms().addAll((Collection<? extends 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_LESS__NAME:
+        setName(NAME_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_LESS__TERMS:
+        getTerms().clear();
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_LESS__NAME:
+        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
+      case VampireLanguagePackage.VLS_LESS__TERMS:
+        return terms != null && !terms.isEmpty();
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (name: ");
+    result.append(name);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSLessImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNameImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNameImpl.java
new file mode 100644
index 00000000..5217696e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNameImpl.java
@@ -0,0 +1,178 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.impl.MinimalEObjectImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Name</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSNameImpl#getName <em>Name</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSNameImpl extends MinimalEObjectImpl.Container implements VLSName
+{
+  /**
+   * The default value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected static final String NAME_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected String name = NAME_EDEFAULT;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSNameImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_NAME;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(String newName)
+  {
+    String oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NAME__NAME, oldName, name));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_NAME__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_NAME__NAME:
+        setName((String)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_NAME__NAME:
+        setName(NAME_EDEFAULT);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_NAME__NAME:
+        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (name: ");
+    result.append(name);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSNameImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNandImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNandImpl.java
new file mode 100644
index 00000000..ca157692
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNandImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNand;
+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 Nand</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSNandImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSNandImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSNandImpl extends VLSTermImpl implements VLSNand
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSNandImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_NAND;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NAND__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NAND__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NAND__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NAND__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NAND__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NAND__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NAND__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NAND__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_NAND__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_NAND__RIGHT:
+        return basicSetRight(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_NAND__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_NAND__RIGHT:
+        return getRight();
+    }
+    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_NAND__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_NAND__RIGHT:
+        setRight((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_NAND__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_NAND__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_NAND__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_NAND__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSNandImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNorImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNorImpl.java
new file mode 100644
index 00000000..b9d8eea4
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSNorImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNor;
+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 Nor</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSNorImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSNorImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSNorImpl extends VLSTermImpl implements VLSNor
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSNorImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_NOR;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NOR__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NOR__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NOR__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NOR__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NOR__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NOR__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_NOR__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_NOR__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_NOR__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_NOR__RIGHT:
+        return basicSetRight(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_NOR__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_NOR__RIGHT:
+        return getRight();
+    }
+    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_NOR__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_NOR__RIGHT:
+        setRight((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_NOR__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_NOR__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_NOR__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_NOR__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSNorImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSOrImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSOrImpl.java
new file mode 100644
index 00000000..dbe09020
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSOrImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr;
+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 Or</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOrImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSOrImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSOrImpl extends VLSTermImpl implements VLSOr
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSOrImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_OR;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_OR__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_OR__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_OR__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_OR__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_OR__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_OR__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_OR__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_OR__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_OR__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_OR__RIGHT:
+        return basicSetRight(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_OR__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_OR__RIGHT:
+        return getRight();
+    }
+    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_OR__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_OR__RIGHT:
+        setRight((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_OR__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_OR__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_OR__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_OR__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSOrImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRationalImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRationalImpl.java
new file mode 100644
index 00000000..43f2b84b
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRationalImpl.java
@@ -0,0 +1,41 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRational;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.ecore.EClass;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Rational</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSRationalImpl extends VLSDefinedTermImpl implements VLSRational
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSRationalImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_RATIONAL;
+  }
+} //VLSRationalImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRealImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRealImpl.java
new file mode 100644
index 00000000..54789949
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRealImpl.java
@@ -0,0 +1,41 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.ecore.EClass;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Real</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSRealImpl extends VLSDefinedTermImpl implements VLSReal
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSRealImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_REAL;
+  }
+} //VLSRealImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRevImpliesImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRevImpliesImpl.java
new file mode 100644
index 00000000..2a0dbf03
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSRevImpliesImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies;
+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 Rev Implies</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSRevImpliesImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSRevImpliesImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSRevImpliesImpl extends VLSTermImpl implements VLSRevImplies
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSRevImpliesImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_REV_IMPLIES;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_REV_IMPLIES__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_REV_IMPLIES__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_REV_IMPLIES__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_REV_IMPLIES__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_REV_IMPLIES__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT:
+        return basicSetRight(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_REV_IMPLIES__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT:
+        return getRight();
+    }
+    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_REV_IMPLIES__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT:
+        setRight((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_REV_IMPLIES__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_REV_IMPLIES__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_REV_IMPLIES__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSRevImpliesImpl
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
new file mode 100644
index 00000000..3766eae5
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java
@@ -0,0 +1,43 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.impl.MinimalEObjectImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Term</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSTermImpl extends MinimalEObjectImpl.Container implements VLSTerm
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSTermImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_TERM;
+  }
+} //VLSTermImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTrueImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTrueImpl.java
new file mode 100644
index 00000000..3153600a
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTrueImpl.java
@@ -0,0 +1,41 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import org.eclipse.emf.ecore.EClass;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS True</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSTrueImpl extends VLSTermImpl implements VLSTrue
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSTrueImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_TRUE;
+  }
+} //VLSTrueImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUnaryNegationImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUnaryNegationImpl.java
new file mode 100644
index 00000000..85dc0b1b
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUnaryNegationImpl.java
@@ -0,0 +1,194 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
+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 Unary Negation</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSUnaryNegationImpl#getOperand <em>Operand</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSUnaryNegationImpl extends VLSTermImpl implements VLSUnaryNegation
+{
+  /**
+   * The cached value of the '{@link #getOperand() <em>Operand</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getOperand()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm operand;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSUnaryNegationImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_UNARY_NEGATION;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getOperand()
+  {
+    return operand;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetOperand(VLSTerm newOperand, NotificationChain msgs)
+  {
+    VLSTerm oldOperand = operand;
+    operand = newOperand;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_UNARY_NEGATION__OPERAND, oldOperand, newOperand);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setOperand(VLSTerm newOperand)
+  {
+    if (newOperand != operand)
+    {
+      NotificationChain msgs = null;
+      if (operand != null)
+        msgs = ((InternalEObject)operand).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_UNARY_NEGATION__OPERAND, null, msgs);
+      if (newOperand != null)
+        msgs = ((InternalEObject)newOperand).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_UNARY_NEGATION__OPERAND, null, msgs);
+      msgs = basicSetOperand(newOperand, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_UNARY_NEGATION__OPERAND, newOperand, newOperand));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_UNARY_NEGATION__OPERAND:
+        return basicSetOperand(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_UNARY_NEGATION__OPERAND:
+        return getOperand();
+    }
+    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_UNARY_NEGATION__OPERAND:
+        setOperand((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_UNARY_NEGATION__OPERAND:
+        setOperand((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_UNARY_NEGATION__OPERAND:
+        return operand != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSUnaryNegationImpl
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
new file mode 100644
index 00000000..5627cc4c
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSUniversalQuantifierImpl.java
@@ -0,0 +1,241 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.Notification;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Universal Quantifier</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSUniversalQuantifierImpl#getVariables <em>Variables</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSUniversalQuantifierImpl#getOperand <em>Operand</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSUniversalQuantifierImpl extends VLSTermImpl implements VLSUniversalQuantifier
+{
+  /**
+   * The cached value of the '{@link #getVariables() <em>Variables</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getVariables()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSVariable> variables;
+  /**
+   * The cached value of the '{@link #getOperand() <em>Operand</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getOperand()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm operand;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSUniversalQuantifierImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_UNIVERSAL_QUANTIFIER;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSVariable> getVariables()
+  {
+    if (variables == null)
+    {
+      variables = new EObjectContainmentEList<VLSVariable>(VLSVariable.class, this, VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__VARIABLES);
+    }
+    return variables;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getOperand()
+  {
+    return operand;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetOperand(VLSTerm newOperand, NotificationChain msgs)
+  {
+    VLSTerm oldOperand = operand;
+    operand = newOperand;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND, oldOperand, newOperand);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setOperand(VLSTerm newOperand)
+  {
+    if (newOperand != operand)
+    {
+      NotificationChain msgs = null;
+      if (operand != null)
+        msgs = ((InternalEObject)operand).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND, null, msgs);
+      if (newOperand != null)
+        msgs = ((InternalEObject)newOperand).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND, null, msgs);
+      msgs = basicSetOperand(newOperand, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND, newOperand, newOperand));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__VARIABLES:
+        return ((InternalEList<?>)getVariables()).basicRemove(otherEnd, msgs);
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND:
+        return basicSetOperand(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_UNIVERSAL_QUANTIFIER__VARIABLES:
+        return getVariables();
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND:
+        return getOperand();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__VARIABLES:
+        getVariables().clear();
+        getVariables().addAll((Collection<? extends VLSVariable>)newValue);
+        return;
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND:
+        setOperand((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_UNIVERSAL_QUANTIFIER__VARIABLES:
+        getVariables().clear();
+        return;
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND:
+        setOperand((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__VARIABLES:
+        return variables != null && !variables.isEmpty();
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER__OPERAND:
+        return operand != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSUniversalQuantifierImpl
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
new file mode 100644
index 00000000..437bb72d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSVariableImpl.java
@@ -0,0 +1,177 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+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.ecore.EClass;
+import org.eclipse.emf.ecore.impl.ENotificationImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>VLS Variable</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSVariableImpl#getName <em>Name</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSVariableImpl extends VLSTermImpl implements VLSVariable
+{
+  /**
+   * The default value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected static final String NAME_EDEFAULT = null;
+  /**
+   * The cached value of the '{@link #getName() <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getName()
+   * @generated
+   * @ordered
+   */
+  protected String name = NAME_EDEFAULT;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSVariableImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_VARIABLE;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public String getName()
+  {
+    return name;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setName(String newName)
+  {
+    String oldName = name;
+    name = newName;
+    if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_VARIABLE__NAME, oldName, name));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public Object eGet(int featureID, boolean resolve, boolean coreType)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_VARIABLE__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__NAME:
+        setName((String)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__NAME:
+        setName(NAME_EDEFAULT);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_VARIABLE__NAME:
+        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
+    }
+    return super.eIsSet(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public String toString()
+  {
+    if (eIsProxy()) return super.toString();
+    StringBuffer result = new StringBuffer(super.toString());
+    result.append(" (name: ");
+    result.append(name);
+    result.append(')');
+    return result.toString();
+  }
+} //VLSVariableImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSXnorImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSXnorImpl.java
new file mode 100644
index 00000000..0f9e5f5a
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSXnorImpl.java
@@ -0,0 +1,265 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSXnor;
+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 Xnor</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSXnorImpl#getLeft <em>Left</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSXnorImpl#getRight <em>Right</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSXnorImpl extends VLSTermImpl implements VLSXnor
+{
+  /**
+   * The cached value of the '{@link #getLeft() <em>Left</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getLeft()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm left;
+  /**
+   * The cached value of the '{@link #getRight() <em>Right</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getRight()
+   * @generated
+   * @ordered
+   */
+  protected VLSTerm right;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSXnorImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_XNOR;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getLeft()
+  {
+    return left;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetLeft(VLSTerm newLeft, NotificationChain msgs)
+  {
+    VLSTerm oldLeft = left;
+    left = newLeft;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_XNOR__LEFT, oldLeft, newLeft);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setLeft(VLSTerm newLeft)
+  {
+    if (newLeft != left)
+    {
+      NotificationChain msgs = null;
+      if (left != null)
+        msgs = ((InternalEObject)left).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_XNOR__LEFT, null, msgs);
+      if (newLeft != null)
+        msgs = ((InternalEObject)newLeft).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_XNOR__LEFT, null, msgs);
+      msgs = basicSetLeft(newLeft, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_XNOR__LEFT, newLeft, newLeft));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm getRight()
+  {
+    return right;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public NotificationChain basicSetRight(VLSTerm newRight, NotificationChain msgs)
+  {
+    VLSTerm oldRight = right;
+    right = newRight;
+    if (eNotificationRequired())
+    {
+      ENotificationImpl notification = new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_XNOR__RIGHT, oldRight, newRight);
+      if (msgs == null) msgs = notification; else msgs.add(notification);
+    }
+    return msgs;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void setRight(VLSTerm newRight)
+  {
+    if (newRight != right)
+    {
+      NotificationChain msgs = null;
+      if (right != null)
+        msgs = ((InternalEObject)right).eInverseRemove(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_XNOR__RIGHT, null, msgs);
+      if (newRight != null)
+        msgs = ((InternalEObject)newRight).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_XNOR__RIGHT, null, msgs);
+      msgs = basicSetRight(newRight, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_XNOR__RIGHT, newRight, newRight));
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_XNOR__LEFT:
+        return basicSetLeft(null, msgs);
+      case VampireLanguagePackage.VLS_XNOR__RIGHT:
+        return basicSetRight(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_XNOR__LEFT:
+        return getLeft();
+      case VampireLanguagePackage.VLS_XNOR__RIGHT:
+        return getRight();
+    }
+    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_XNOR__LEFT:
+        setLeft((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_XNOR__RIGHT:
+        setRight((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_XNOR__LEFT:
+        setLeft((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_XNOR__RIGHT:
+        setRight((VLSTerm)null);
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VLS_XNOR__LEFT:
+        return left != null;
+      case VampireLanguagePackage.VLS_XNOR__RIGHT:
+        return right != null;
+    }
+    return super.eIsSet(featureID);
+  }
+} //VLSXnorImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
new file mode 100644
index 00000000..630fa8ce
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
@@ -0,0 +1,491 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.*;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EPackage;
+import org.eclipse.emf.ecore.impl.EFactoryImpl;
+import org.eclipse.emf.ecore.plugin.EcorePlugin;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model <b>Factory</b>.
+ * <!-- end-user-doc -->
+ * @generated
+ */
+public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireLanguageFactory
+{
+  /**
+   * Creates the default factory implementation.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public static VampireLanguageFactory init()
+  {
+    try
+    {
+      VampireLanguageFactory theVampireLanguageFactory = (VampireLanguageFactory)EPackage.Registry.INSTANCE.getEFactory(VampireLanguagePackage.eNS_URI);
+      if (theVampireLanguageFactory != null)
+      {
+        return theVampireLanguageFactory;
+      }
+    }
+    catch (Exception exception)
+    {
+      EcorePlugin.INSTANCE.log(exception);
+    }
+    return new VampireLanguageFactoryImpl();
+  }
+  /**
+   * Creates an instance of the factory.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VampireLanguageFactoryImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public EObject create(EClass eClass)
+  {
+    switch (eClass.getClassifierID())
+    {
+      case VampireLanguagePackage.VAMPIRE_MODEL: return createVampireModel();
+      case VampireLanguagePackage.VLS_INCLUDE: return createVLSInclude();
+      case VampireLanguagePackage.VLS_NAME: return createVLSName();
+      case VampireLanguagePackage.VLS_COMMENT: return createVLSComment();
+      case VampireLanguagePackage.VLS_FOF_FORMULA: return createVLSFofFormula();
+      case VampireLanguagePackage.VLS_ANNOTATION: return createVLSAnnotation();
+      case VampireLanguagePackage.VLS_TERM: return createVLSTerm();
+      case VampireLanguagePackage.VLS_VARIABLE: return createVLSVariable();
+      case VampireLanguagePackage.VLS_FUNCTION_FOF: return createVLSFunctionFof();
+      case VampireLanguagePackage.VLS_DEFINED_TERM: return createVLSDefinedTerm();
+      case VampireLanguagePackage.VLS_EQUIVALENT: return createVLSEquivalent();
+      case VampireLanguagePackage.VLS_IMPLIES: return createVLSImplies();
+      case VampireLanguagePackage.VLS_REV_IMPLIES: return createVLSRevImplies();
+      case VampireLanguagePackage.VLS_XNOR: return createVLSXnor();
+      case VampireLanguagePackage.VLS_NOR: return createVLSNor();
+      case VampireLanguagePackage.VLS_NAND: return createVLSNand();
+      case VampireLanguagePackage.VLS_AND: return createVLSAnd();
+      case VampireLanguagePackage.VLS_OR: return createVLSOr();
+      case VampireLanguagePackage.VLS_UNIVERSAL_QUANTIFIER: return createVLSUniversalQuantifier();
+      case VampireLanguagePackage.VLS_EXISTENTIAL_QUANTIFIER: return createVLSExistentialQuantifier();
+      case VampireLanguagePackage.VLS_UNARY_NEGATION: return createVLSUnaryNegation();
+      case VampireLanguagePackage.VLS_INEQUALITY: return createVLSInequality();
+      case VampireLanguagePackage.VLS_EQUALITY: return createVLSEquality();
+      case VampireLanguagePackage.VLS_ASSIGNMENT: return createVLSAssignment();
+      case VampireLanguagePackage.VLS_CONSTANT: return createVLSConstant();
+      case VampireLanguagePackage.VLS_TRUE: return createVLSTrue();
+      case VampireLanguagePackage.VLS_FALSE: return createVLSFalse();
+      case VampireLanguagePackage.VLS_FUNCTION: return createVLSFunction();
+      case VampireLanguagePackage.VLS_LESS: return createVLSLess();
+      case VampireLanguagePackage.VLS_INT: return createVLSInt();
+      case VampireLanguagePackage.VLS_REAL: return createVLSReal();
+      case VampireLanguagePackage.VLS_RATIONAL: return createVLSRational();
+      case VampireLanguagePackage.VLS_DOUBLE_QUOTE: return createVLSDoubleQuote();
+      default:
+        throw new IllegalArgumentException("The class '" + eClass.getName() + "' is not a valid classifier");
+    }
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VampireModel createVampireModel()
+  {
+    VampireModelImpl vampireModel = new VampireModelImpl();
+    return vampireModel;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSInclude createVLSInclude()
+  {
+    VLSIncludeImpl vlsInclude = new VLSIncludeImpl();
+    return vlsInclude;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSName createVLSName()
+  {
+    VLSNameImpl vlsName = new VLSNameImpl();
+    return vlsName;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSComment createVLSComment()
+  {
+    VLSCommentImpl vlsComment = new VLSCommentImpl();
+    return vlsComment;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSFofFormula createVLSFofFormula()
+  {
+    VLSFofFormulaImpl vlsFofFormula = new VLSFofFormulaImpl();
+    return vlsFofFormula;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSAnnotation createVLSAnnotation()
+  {
+    VLSAnnotationImpl vlsAnnotation = new VLSAnnotationImpl();
+    return vlsAnnotation;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTerm createVLSTerm()
+  {
+    VLSTermImpl vlsTerm = new VLSTermImpl();
+    return vlsTerm;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSVariable createVLSVariable()
+  {
+    VLSVariableImpl vlsVariable = new VLSVariableImpl();
+    return vlsVariable;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSFunctionFof createVLSFunctionFof()
+  {
+    VLSFunctionFofImpl vlsFunctionFof = new VLSFunctionFofImpl();
+    return vlsFunctionFof;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSDefinedTerm createVLSDefinedTerm()
+  {
+    VLSDefinedTermImpl vlsDefinedTerm = new VLSDefinedTermImpl();
+    return vlsDefinedTerm;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSEquivalent createVLSEquivalent()
+  {
+    VLSEquivalentImpl vlsEquivalent = new VLSEquivalentImpl();
+    return vlsEquivalent;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSImplies createVLSImplies()
+  {
+    VLSImpliesImpl vlsImplies = new VLSImpliesImpl();
+    return vlsImplies;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSRevImplies createVLSRevImplies()
+  {
+    VLSRevImpliesImpl vlsRevImplies = new VLSRevImpliesImpl();
+    return vlsRevImplies;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSXnor createVLSXnor()
+  {
+    VLSXnorImpl vlsXnor = new VLSXnorImpl();
+    return vlsXnor;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSNor createVLSNor()
+  {
+    VLSNorImpl vlsNor = new VLSNorImpl();
+    return vlsNor;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSNand createVLSNand()
+  {
+    VLSNandImpl vlsNand = new VLSNandImpl();
+    return vlsNand;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSAnd createVLSAnd()
+  {
+    VLSAndImpl vlsAnd = new VLSAndImpl();
+    return vlsAnd;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSOr createVLSOr()
+  {
+    VLSOrImpl vlsOr = new VLSOrImpl();
+    return vlsOr;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSUniversalQuantifier createVLSUniversalQuantifier()
+  {
+    VLSUniversalQuantifierImpl vlsUniversalQuantifier = new VLSUniversalQuantifierImpl();
+    return vlsUniversalQuantifier;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSExistentialQuantifier createVLSExistentialQuantifier()
+  {
+    VLSExistentialQuantifierImpl vlsExistentialQuantifier = new VLSExistentialQuantifierImpl();
+    return vlsExistentialQuantifier;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSUnaryNegation createVLSUnaryNegation()
+  {
+    VLSUnaryNegationImpl vlsUnaryNegation = new VLSUnaryNegationImpl();
+    return vlsUnaryNegation;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSInequality createVLSInequality()
+  {
+    VLSInequalityImpl vlsInequality = new VLSInequalityImpl();
+    return vlsInequality;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSEquality createVLSEquality()
+  {
+    VLSEqualityImpl vlsEquality = new VLSEqualityImpl();
+    return vlsEquality;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSAssignment createVLSAssignment()
+  {
+    VLSAssignmentImpl vlsAssignment = new VLSAssignmentImpl();
+    return vlsAssignment;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSConstant createVLSConstant()
+  {
+    VLSConstantImpl vlsConstant = new VLSConstantImpl();
+    return vlsConstant;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTrue createVLSTrue()
+  {
+    VLSTrueImpl vlsTrue = new VLSTrueImpl();
+    return vlsTrue;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSFalse createVLSFalse()
+  {
+    VLSFalseImpl vlsFalse = new VLSFalseImpl();
+    return vlsFalse;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSFunction createVLSFunction()
+  {
+    VLSFunctionImpl vlsFunction = new VLSFunctionImpl();
+    return vlsFunction;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSLess createVLSLess()
+  {
+    VLSLessImpl vlsLess = new VLSLessImpl();
+    return vlsLess;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSInt createVLSInt()
+  {
+    VLSIntImpl vlsInt = new VLSIntImpl();
+    return vlsInt;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSReal createVLSReal()
+  {
+    VLSRealImpl vlsReal = new VLSRealImpl();
+    return vlsReal;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSRational createVLSRational()
+  {
+    VLSRationalImpl vlsRational = new VLSRationalImpl();
+    return vlsRational;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSDoubleQuote createVLSDoubleQuote()
+  {
+    VLSDoubleQuoteImpl vlsDoubleQuote = new VLSDoubleQuoteImpl();
+    return vlsDoubleQuote;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VampireLanguagePackage getVampireLanguagePackage()
+  {
+    return (VampireLanguagePackage)getEPackage();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @deprecated
+   * @generated
+   */
+  @Deprecated
+  public static VampireLanguagePackage getPackage()
+  {
+    return VampireLanguagePackage.eINSTANCE;
+  }
+} //VampireLanguageFactoryImpl
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
new file mode 100644
index 00000000..86921032
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
@@ -0,0 +1,1505 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnnotation;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAssignment;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDefinedTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFalse;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSLess;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNand;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSNor;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRational;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSXnor;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
+import org.eclipse.emf.ecore.EAttribute;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EPackage;
+import org.eclipse.emf.ecore.EReference;
+import org.eclipse.emf.ecore.impl.EPackageImpl;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model <b>Package</b>.
+ * <!-- end-user-doc -->
+ * @generated
+ */
+public class VampireLanguagePackageImpl extends EPackageImpl implements VampireLanguagePackage
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vampireModelEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsIncludeEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsNameEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsCommentEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsFofFormulaEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsAnnotationEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsTermEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsVariableEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsFunctionFofEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsDefinedTermEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsEquivalentEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsImpliesEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsRevImpliesEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsXnorEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsNorEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsNandEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsAndEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsOrEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsUniversalQuantifierEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsExistentialQuantifierEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsUnaryNegationEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsInequalityEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsEqualityEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsAssignmentEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsConstantEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsTrueEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsFalseEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsFunctionEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsLessEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsIntEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsRealEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsRationalEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsDoubleQuoteEClass = null;
+  /**
+   * Creates an instance of the model <b>Package</b>, registered with
+   * {@link org.eclipse.emf.ecore.EPackage.Registry EPackage.Registry} by the package
+   * package URI value.
+   * <p>Note: the correct way to create the package is via the static
+   * factory method {@link #init init()}, which also performs
+   * initialization of the package, or returns the registered package,
+   * if one already exists.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see org.eclipse.emf.ecore.EPackage.Registry
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#eNS_URI
+   * @see #init()
+   * @generated
+   */
+  private VampireLanguagePackageImpl()
+  {
+    super(eNS_URI, VampireLanguageFactory.eINSTANCE);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private static boolean isInited = false;
+  /**
+   * Creates, registers, and initializes the <b>Package</b> for this model, and for any others upon which it depends.
+   * 
+   * <p>This method is used to initialize {@link VampireLanguagePackage#eINSTANCE} when that field is accessed.
+   * Clients should not invoke it directly. Instead, they should simply access that field to obtain the package.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #eNS_URI
+   * @see #createPackageContents()
+   * @see #initializePackageContents()
+   * @generated
+   */
+  public static VampireLanguagePackage init()
+  {
+    if (isInited) return (VampireLanguagePackage)EPackage.Registry.INSTANCE.getEPackage(VampireLanguagePackage.eNS_URI);
+    // Obtain or create and register package
+    VampireLanguagePackageImpl theVampireLanguagePackage = (VampireLanguagePackageImpl)(EPackage.Registry.INSTANCE.get(eNS_URI) instanceof VampireLanguagePackageImpl ? EPackage.Registry.INSTANCE.get(eNS_URI) : new VampireLanguagePackageImpl());
+    isInited = true;
+    // Create package meta-data objects
+    theVampireLanguagePackage.createPackageContents();
+    // Initialize created meta-data
+    theVampireLanguagePackage.initializePackageContents();
+    // Mark meta-data to indicate it can't be changed
+    theVampireLanguagePackage.freeze();
+  
+    // Update the registry and return the package
+    EPackage.Registry.INSTANCE.put(VampireLanguagePackage.eNS_URI, theVampireLanguagePackage);
+    return theVampireLanguagePackage;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVampireModel()
+  {
+    return vampireModelEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVampireModel_Includes()
+  {
+    return (EReference)vampireModelEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVampireModel_Comments()
+  {
+    return (EReference)vampireModelEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVampireModel_Formulas()
+  {
+    return (EReference)vampireModelEClass.getEStructuralFeatures().get(2);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSInclude()
+  {
+    return vlsIncludeEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSInclude_FileName()
+  {
+    return (EAttribute)vlsIncludeEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSInclude_Names()
+  {
+    return (EReference)vlsIncludeEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSName()
+  {
+    return vlsNameEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSName_Name()
+  {
+    return (EAttribute)vlsNameEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSComment()
+  {
+    return vlsCommentEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSComment_Comment()
+  {
+    return (EAttribute)vlsCommentEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSFofFormula()
+  {
+    return vlsFofFormulaEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSFofFormula_Name()
+  {
+    return (EAttribute)vlsFofFormulaEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSFofFormula_FofRole()
+  {
+    return (EAttribute)vlsFofFormulaEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSFofFormula_FofFormula()
+  {
+    return (EReference)vlsFofFormulaEClass.getEStructuralFeatures().get(2);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSFofFormula_Annotations()
+  {
+    return (EReference)vlsFofFormulaEClass.getEStructuralFeatures().get(3);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSAnnotation()
+  {
+    return vlsAnnotationEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSAnnotation_Name()
+  {
+    return (EAttribute)vlsAnnotationEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSAnnotation_Followup()
+  {
+    return (EReference)vlsAnnotationEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSAnnotation_Terms()
+  {
+    return (EReference)vlsAnnotationEClass.getEStructuralFeatures().get(2);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSTerm()
+  {
+    return vlsTermEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSVariable()
+  {
+    return vlsVariableEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSVariable_Name()
+  {
+    return (EAttribute)vlsVariableEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSFunctionFof()
+  {
+    return vlsFunctionFofEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSFunctionFof_Functor()
+  {
+    return (EAttribute)vlsFunctionFofEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSFunctionFof_Terms()
+  {
+    return (EReference)vlsFunctionFofEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSDefinedTerm()
+  {
+    return vlsDefinedTermEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSDefinedTerm_Value()
+  {
+    return (EAttribute)vlsDefinedTermEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSEquivalent()
+  {
+    return vlsEquivalentEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSEquivalent_Left()
+  {
+    return (EReference)vlsEquivalentEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSEquivalent_Right()
+  {
+    return (EReference)vlsEquivalentEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSImplies()
+  {
+    return vlsImpliesEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSImplies_Left()
+  {
+    return (EReference)vlsImpliesEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSImplies_Right()
+  {
+    return (EReference)vlsImpliesEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSRevImplies()
+  {
+    return vlsRevImpliesEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSRevImplies_Left()
+  {
+    return (EReference)vlsRevImpliesEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSRevImplies_Right()
+  {
+    return (EReference)vlsRevImpliesEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSXnor()
+  {
+    return vlsXnorEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSXnor_Left()
+  {
+    return (EReference)vlsXnorEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSXnor_Right()
+  {
+    return (EReference)vlsXnorEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSNor()
+  {
+    return vlsNorEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSNor_Left()
+  {
+    return (EReference)vlsNorEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSNor_Right()
+  {
+    return (EReference)vlsNorEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSNand()
+  {
+    return vlsNandEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSNand_Left()
+  {
+    return (EReference)vlsNandEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSNand_Right()
+  {
+    return (EReference)vlsNandEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSAnd()
+  {
+    return vlsAndEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSAnd_Left()
+  {
+    return (EReference)vlsAndEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSAnd_Right()
+  {
+    return (EReference)vlsAndEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSOr()
+  {
+    return vlsOrEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSOr_Left()
+  {
+    return (EReference)vlsOrEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSOr_Right()
+  {
+    return (EReference)vlsOrEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSUniversalQuantifier()
+  {
+    return vlsUniversalQuantifierEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSUniversalQuantifier_Variables()
+  {
+    return (EReference)vlsUniversalQuantifierEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSUniversalQuantifier_Operand()
+  {
+    return (EReference)vlsUniversalQuantifierEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSExistentialQuantifier()
+  {
+    return vlsExistentialQuantifierEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSExistentialQuantifier_Variables()
+  {
+    return (EReference)vlsExistentialQuantifierEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSExistentialQuantifier_Operand()
+  {
+    return (EReference)vlsExistentialQuantifierEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSUnaryNegation()
+  {
+    return vlsUnaryNegationEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSUnaryNegation_Operand()
+  {
+    return (EReference)vlsUnaryNegationEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSInequality()
+  {
+    return vlsInequalityEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSInequality_Left()
+  {
+    return (EReference)vlsInequalityEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSInequality_Right()
+  {
+    return (EReference)vlsInequalityEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSEquality()
+  {
+    return vlsEqualityEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSEquality_Left()
+  {
+    return (EReference)vlsEqualityEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSEquality_Right()
+  {
+    return (EReference)vlsEqualityEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSAssignment()
+  {
+    return vlsAssignmentEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSAssignment_Left()
+  {
+    return (EReference)vlsAssignmentEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSAssignment_Right()
+  {
+    return (EReference)vlsAssignmentEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSConstant()
+  {
+    return vlsConstantEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSConstant_Name()
+  {
+    return (EAttribute)vlsConstantEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSTrue()
+  {
+    return vlsTrueEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSFalse()
+  {
+    return vlsFalseEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSFunction()
+  {
+    return vlsFunctionEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSFunction_Constant()
+  {
+    return (EAttribute)vlsFunctionEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSFunction_Terms()
+  {
+    return (EReference)vlsFunctionEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSLess()
+  {
+    return vlsLessEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSLess_Name()
+  {
+    return (EAttribute)vlsLessEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSLess_Terms()
+  {
+    return (EReference)vlsLessEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSInt()
+  {
+    return vlsIntEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSReal()
+  {
+    return vlsRealEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSRational()
+  {
+    return vlsRationalEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSDoubleQuote()
+  {
+    return vlsDoubleQuoteEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VampireLanguageFactory getVampireLanguageFactory()
+  {
+    return (VampireLanguageFactory)getEFactoryInstance();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private boolean isCreated = false;
+  /**
+   * Creates the meta-model objects for the package.  This method is
+   * guarded to have no affect on any invocation but its first.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void createPackageContents()
+  {
+    if (isCreated) return;
+    isCreated = true;
+    // Create classes and their features
+    vampireModelEClass = createEClass(VAMPIRE_MODEL);
+    createEReference(vampireModelEClass, VAMPIRE_MODEL__INCLUDES);
+    createEReference(vampireModelEClass, VAMPIRE_MODEL__COMMENTS);
+    createEReference(vampireModelEClass, VAMPIRE_MODEL__FORMULAS);
+    vlsIncludeEClass = createEClass(VLS_INCLUDE);
+    createEAttribute(vlsIncludeEClass, VLS_INCLUDE__FILE_NAME);
+    createEReference(vlsIncludeEClass, VLS_INCLUDE__NAMES);
+    vlsNameEClass = createEClass(VLS_NAME);
+    createEAttribute(vlsNameEClass, VLS_NAME__NAME);
+    vlsCommentEClass = createEClass(VLS_COMMENT);
+    createEAttribute(vlsCommentEClass, VLS_COMMENT__COMMENT);
+    vlsFofFormulaEClass = createEClass(VLS_FOF_FORMULA);
+    createEAttribute(vlsFofFormulaEClass, VLS_FOF_FORMULA__NAME);
+    createEAttribute(vlsFofFormulaEClass, VLS_FOF_FORMULA__FOF_ROLE);
+    createEReference(vlsFofFormulaEClass, VLS_FOF_FORMULA__FOF_FORMULA);
+    createEReference(vlsFofFormulaEClass, VLS_FOF_FORMULA__ANNOTATIONS);
+    vlsAnnotationEClass = createEClass(VLS_ANNOTATION);
+    createEAttribute(vlsAnnotationEClass, VLS_ANNOTATION__NAME);
+    createEReference(vlsAnnotationEClass, VLS_ANNOTATION__FOLLOWUP);
+    createEReference(vlsAnnotationEClass, VLS_ANNOTATION__TERMS);
+    vlsTermEClass = createEClass(VLS_TERM);
+    vlsVariableEClass = createEClass(VLS_VARIABLE);
+    createEAttribute(vlsVariableEClass, VLS_VARIABLE__NAME);
+    vlsFunctionFofEClass = createEClass(VLS_FUNCTION_FOF);
+    createEAttribute(vlsFunctionFofEClass, VLS_FUNCTION_FOF__FUNCTOR);
+    createEReference(vlsFunctionFofEClass, VLS_FUNCTION_FOF__TERMS);
+    vlsDefinedTermEClass = createEClass(VLS_DEFINED_TERM);
+    createEAttribute(vlsDefinedTermEClass, VLS_DEFINED_TERM__VALUE);
+    vlsEquivalentEClass = createEClass(VLS_EQUIVALENT);
+    createEReference(vlsEquivalentEClass, VLS_EQUIVALENT__LEFT);
+    createEReference(vlsEquivalentEClass, VLS_EQUIVALENT__RIGHT);
+    vlsImpliesEClass = createEClass(VLS_IMPLIES);
+    createEReference(vlsImpliesEClass, VLS_IMPLIES__LEFT);
+    createEReference(vlsImpliesEClass, VLS_IMPLIES__RIGHT);
+    vlsRevImpliesEClass = createEClass(VLS_REV_IMPLIES);
+    createEReference(vlsRevImpliesEClass, VLS_REV_IMPLIES__LEFT);
+    createEReference(vlsRevImpliesEClass, VLS_REV_IMPLIES__RIGHT);
+    vlsXnorEClass = createEClass(VLS_XNOR);
+    createEReference(vlsXnorEClass, VLS_XNOR__LEFT);
+    createEReference(vlsXnorEClass, VLS_XNOR__RIGHT);
+    vlsNorEClass = createEClass(VLS_NOR);
+    createEReference(vlsNorEClass, VLS_NOR__LEFT);
+    createEReference(vlsNorEClass, VLS_NOR__RIGHT);
+    vlsNandEClass = createEClass(VLS_NAND);
+    createEReference(vlsNandEClass, VLS_NAND__LEFT);
+    createEReference(vlsNandEClass, VLS_NAND__RIGHT);
+    vlsAndEClass = createEClass(VLS_AND);
+    createEReference(vlsAndEClass, VLS_AND__LEFT);
+    createEReference(vlsAndEClass, VLS_AND__RIGHT);
+    vlsOrEClass = createEClass(VLS_OR);
+    createEReference(vlsOrEClass, VLS_OR__LEFT);
+    createEReference(vlsOrEClass, VLS_OR__RIGHT);
+    vlsUniversalQuantifierEClass = createEClass(VLS_UNIVERSAL_QUANTIFIER);
+    createEReference(vlsUniversalQuantifierEClass, VLS_UNIVERSAL_QUANTIFIER__VARIABLES);
+    createEReference(vlsUniversalQuantifierEClass, VLS_UNIVERSAL_QUANTIFIER__OPERAND);
+    vlsExistentialQuantifierEClass = createEClass(VLS_EXISTENTIAL_QUANTIFIER);
+    createEReference(vlsExistentialQuantifierEClass, VLS_EXISTENTIAL_QUANTIFIER__VARIABLES);
+    createEReference(vlsExistentialQuantifierEClass, VLS_EXISTENTIAL_QUANTIFIER__OPERAND);
+    vlsUnaryNegationEClass = createEClass(VLS_UNARY_NEGATION);
+    createEReference(vlsUnaryNegationEClass, VLS_UNARY_NEGATION__OPERAND);
+    vlsInequalityEClass = createEClass(VLS_INEQUALITY);
+    createEReference(vlsInequalityEClass, VLS_INEQUALITY__LEFT);
+    createEReference(vlsInequalityEClass, VLS_INEQUALITY__RIGHT);
+    vlsEqualityEClass = createEClass(VLS_EQUALITY);
+    createEReference(vlsEqualityEClass, VLS_EQUALITY__LEFT);
+    createEReference(vlsEqualityEClass, VLS_EQUALITY__RIGHT);
+    vlsAssignmentEClass = createEClass(VLS_ASSIGNMENT);
+    createEReference(vlsAssignmentEClass, VLS_ASSIGNMENT__LEFT);
+    createEReference(vlsAssignmentEClass, VLS_ASSIGNMENT__RIGHT);
+    vlsConstantEClass = createEClass(VLS_CONSTANT);
+    createEAttribute(vlsConstantEClass, VLS_CONSTANT__NAME);
+    vlsTrueEClass = createEClass(VLS_TRUE);
+    vlsFalseEClass = createEClass(VLS_FALSE);
+    vlsFunctionEClass = createEClass(VLS_FUNCTION);
+    createEAttribute(vlsFunctionEClass, VLS_FUNCTION__CONSTANT);
+    createEReference(vlsFunctionEClass, VLS_FUNCTION__TERMS);
+    vlsLessEClass = createEClass(VLS_LESS);
+    createEAttribute(vlsLessEClass, VLS_LESS__NAME);
+    createEReference(vlsLessEClass, VLS_LESS__TERMS);
+    vlsIntEClass = createEClass(VLS_INT);
+    vlsRealEClass = createEClass(VLS_REAL);
+    vlsRationalEClass = createEClass(VLS_RATIONAL);
+    vlsDoubleQuoteEClass = createEClass(VLS_DOUBLE_QUOTE);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private boolean isInitialized = false;
+  /**
+   * Complete the initialization of the package and its meta-model.  This
+   * method is guarded to have no affect on any invocation but its first.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public void initializePackageContents()
+  {
+    if (isInitialized) return;
+    isInitialized = true;
+    // Initialize package
+    setName(eNAME);
+    setNsPrefix(eNS_PREFIX);
+    setNsURI(eNS_URI);
+    // Create type parameters
+    // Set bounds for type parameters
+    // Add supertypes to classes
+    vlsVariableEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsFunctionFofEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsDefinedTermEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsEquivalentEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsImpliesEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsRevImpliesEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsXnorEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsNorEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsNandEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsAndEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsOrEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsUniversalQuantifierEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsExistentialQuantifierEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsUnaryNegationEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsInequalityEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsEqualityEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsAssignmentEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsConstantEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsTrueEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsFalseEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsFunctionEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsLessEClass.getESuperTypes().add(this.getVLSTerm());
+    vlsIntEClass.getESuperTypes().add(this.getVLSDefinedTerm());
+    vlsRealEClass.getESuperTypes().add(this.getVLSDefinedTerm());
+    vlsRationalEClass.getESuperTypes().add(this.getVLSDefinedTerm());
+    vlsDoubleQuoteEClass.getESuperTypes().add(this.getVLSDefinedTerm());
+    // Initialize classes and features; add operations and parameters
+    initEClass(vampireModelEClass, VampireModel.class, "VampireModel", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVampireModel_Includes(), this.getVLSInclude(), null, "includes", null, 0, -1, VampireModel.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVampireModel_Comments(), this.getVLSComment(), null, "comments", null, 0, -1, VampireModel.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVampireModel_Formulas(), this.getVLSFofFormula(), null, "formulas", null, 0, -1, VampireModel.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsIncludeEClass, VLSInclude.class, "VLSInclude", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSInclude_FileName(), ecorePackage.getEString(), "fileName", null, 0, 1, VLSInclude.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSInclude_Names(), this.getVLSName(), null, "names", null, 0, -1, VLSInclude.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsNameEClass, VLSName.class, "VLSName", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSName_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSName.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsCommentEClass, VLSComment.class, "VLSComment", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSComment_Comment(), ecorePackage.getEString(), "comment", null, 0, 1, VLSComment.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsFofFormulaEClass, VLSFofFormula.class, "VLSFofFormula", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSFofFormula_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSFofFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEAttribute(getVLSFofFormula_FofRole(), ecorePackage.getEString(), "fofRole", null, 0, 1, VLSFofFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSFofFormula_FofFormula(), this.getVLSTerm(), null, "fofFormula", null, 0, 1, VLSFofFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSFofFormula_Annotations(), this.getVLSAnnotation(), null, "annotations", null, 0, 1, VLSFofFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsAnnotationEClass, VLSAnnotation.class, "VLSAnnotation", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSAnnotation_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSAnnotation.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSAnnotation_Followup(), this.getVLSAnnotation(), null, "followup", null, 0, 1, VLSAnnotation.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSAnnotation_Terms(), this.getVLSAnnotation(), null, "terms", null, 0, -1, VLSAnnotation.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);
+    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);
+    initEClass(vlsFunctionFofEClass, VLSFunctionFof.class, "VLSFunctionFof", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSFunctionFof_Functor(), ecorePackage.getEString(), "functor", null, 0, 1, VLSFunctionFof.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSFunctionFof_Terms(), this.getVLSTerm(), null, "terms", null, 0, -1, VLSFunctionFof.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsDefinedTermEClass, VLSDefinedTerm.class, "VLSDefinedTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSDefinedTerm_Value(), ecorePackage.getEString(), "value", null, 0, 1, VLSDefinedTerm.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsEquivalentEClass, VLSEquivalent.class, "VLSEquivalent", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSEquivalent_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSEquivalent.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSEquivalent_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSEquivalent.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsImpliesEClass, VLSImplies.class, "VLSImplies", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSImplies_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSImplies.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSImplies_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSImplies.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsRevImpliesEClass, VLSRevImplies.class, "VLSRevImplies", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSRevImplies_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSRevImplies.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSRevImplies_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSRevImplies.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsXnorEClass, VLSXnor.class, "VLSXnor", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSXnor_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSXnor.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSXnor_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSXnor.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsNorEClass, VLSNor.class, "VLSNor", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSNor_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSNor.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSNor_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSNor.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsNandEClass, VLSNand.class, "VLSNand", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSNand_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSNand.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSNand_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSNand.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsAndEClass, VLSAnd.class, "VLSAnd", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSAnd_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSAnd.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSAnd_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSAnd.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsOrEClass, VLSOr.class, "VLSOr", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSOr_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSOr.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    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.getVLSVariable(), 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.getVLSVariable(), 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);
+    initEReference(getVLSUnaryNegation_Operand(), this.getVLSTerm(), null, "operand", null, 0, 1, VLSUnaryNegation.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsInequalityEClass, VLSInequality.class, "VLSInequality", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSInequality_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSInequality.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSInequality_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSInequality.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsEqualityEClass, VLSEquality.class, "VLSEquality", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSEquality_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSEquality.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSEquality_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSEquality.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsAssignmentEClass, VLSAssignment.class, "VLSAssignment", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEReference(getVLSAssignment_Left(), this.getVLSTerm(), null, "left", null, 0, 1, VLSAssignment.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSAssignment_Right(), this.getVLSTerm(), null, "right", null, 0, 1, VLSAssignment.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsConstantEClass, VLSConstant.class, "VLSConstant", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSConstant_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSConstant.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsTrueEClass, VLSTrue.class, "VLSTrue", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEClass(vlsFalseEClass, VLSFalse.class, "VLSFalse", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEClass(vlsFunctionEClass, VLSFunction.class, "VLSFunction", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSFunction_Constant(), ecorePackage.getEString(), "constant", null, 0, 1, VLSFunction.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSFunction_Terms(), this.getVLSTerm(), null, "terms", null, 0, -1, VLSFunction.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsLessEClass, VLSLess.class, "VLSLess", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSLess_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSLess.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSLess_Terms(), this.getVLSTerm(), null, "terms", null, 0, -1, VLSLess.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsIntEClass, VLSInt.class, "VLSInt", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEClass(vlsRealEClass, VLSReal.class, "VLSReal", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEClass(vlsRationalEClass, VLSRational.class, "VLSRational", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEClass(vlsDoubleQuoteEClass, VLSDoubleQuote.class, "VLSDoubleQuote", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    // Create resource
+    createResource(eNS_URI);
+  }
+} //VampireLanguagePackageImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireModelImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireModelImpl.java
new file mode 100644
index 00000000..ea3dabc7
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireModelImpl.java
@@ -0,0 +1,246 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
+import java.util.Collection;
+import org.eclipse.emf.common.notify.NotificationChain;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.InternalEObject;
+import org.eclipse.emf.ecore.impl.MinimalEObjectImpl;
+import org.eclipse.emf.ecore.util.EObjectContainmentEList;
+import org.eclipse.emf.ecore.util.InternalEList;
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>Vampire Model</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl#getIncludes <em>Includes</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl#getComments <em>Comments</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl#getFormulas <em>Formulas</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VampireModelImpl extends MinimalEObjectImpl.Container implements VampireModel
+{
+  /**
+   * The cached value of the '{@link #getIncludes() <em>Includes</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getIncludes()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSInclude> includes;
+  /**
+   * The cached value of the '{@link #getComments() <em>Comments</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getComments()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSComment> comments;
+  /**
+   * The cached value of the '{@link #getFormulas() <em>Formulas</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getFormulas()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSFofFormula> formulas;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VampireModelImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VAMPIRE_MODEL;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSInclude> getIncludes()
+  {
+    if (includes == null)
+    {
+      includes = new EObjectContainmentEList<VLSInclude>(VLSInclude.class, this, VampireLanguagePackage.VAMPIRE_MODEL__INCLUDES);
+    }
+    return includes;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSComment> getComments()
+  {
+    if (comments == null)
+    {
+      comments = new EObjectContainmentEList<VLSComment>(VLSComment.class, this, VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS);
+    }
+    return comments;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EList<VLSFofFormula> getFormulas()
+  {
+    if (formulas == null)
+    {
+      formulas = new EObjectContainmentEList<VLSFofFormula>(VLSFofFormula.class, this, VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS);
+    }
+    return formulas;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VAMPIRE_MODEL__INCLUDES:
+        return ((InternalEList<?>)getIncludes()).basicRemove(otherEnd, msgs);
+      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
+        return ((InternalEList<?>)getComments()).basicRemove(otherEnd, msgs);
+      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
+        return ((InternalEList<?>)getFormulas()).basicRemove(otherEnd, 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.VAMPIRE_MODEL__INCLUDES:
+        return getIncludes();
+      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
+        return getComments();
+      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
+        return getFormulas();
+    }
+    return super.eGet(featureID, resolve, coreType);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @SuppressWarnings("unchecked")
+  @Override
+  public void eSet(int featureID, Object newValue)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VAMPIRE_MODEL__INCLUDES:
+        getIncludes().clear();
+        getIncludes().addAll((Collection<? extends VLSInclude>)newValue);
+        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
+        getComments().clear();
+        getComments().addAll((Collection<? extends VLSComment>)newValue);
+        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
+        getFormulas().clear();
+        getFormulas().addAll((Collection<? extends VLSFofFormula>)newValue);
+        return;
+    }
+    super.eSet(featureID, newValue);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public void eUnset(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VAMPIRE_MODEL__INCLUDES:
+        getIncludes().clear();
+        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
+        getComments().clear();
+        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
+        getFormulas().clear();
+        return;
+    }
+    super.eUnset(featureID);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  public boolean eIsSet(int featureID)
+  {
+    switch (featureID)
+    {
+      case VampireLanguagePackage.VAMPIRE_MODEL__INCLUDES:
+        return includes != null && !includes.isEmpty();
+      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
+        return comments != null && !comments.isEmpty();
+      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
+        return formulas != null && !formulas.isEmpty();
+    }
+    return super.eIsSet(featureID);
+  }
+} //VampireModelImpl