18 files changed, 1994 insertions, 32 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSConfirmations.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSConfirmations.java
new file mode 100644
index 00000000..25e607f9
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSConfirmations.java
@@ -0,0 +1,20 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage;
+import org.eclipse.emf.ecore.EObject;
+/**
+ * <!-- begin-user-doc -->
+ * A representation of the model object '<em><b>VLS Confirmations</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ *
+ * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSConfirmations()
+ * @model
+ * @generated
+ */
+public interface VLSConfirmations extends EObject
+{
+} // VLSConfirmations
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSFiniteModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSFiniteModel.java
new file mode 100644
index 00000000..bfd23d8d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSFiniteModel.java
@@ -0,0 +1,20 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage;
+import org.eclipse.emf.ecore.EObject;
+/**
+ * <!-- begin-user-doc -->
+ * A representation of the model object '<em><b>VLS Finite Model</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ *
+ * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSFiniteModel()
+ * @model
+ * @generated
+ */
+public interface VLSFiniteModel extends EObject
+{
+} // VLSFiniteModel
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSSatisfiable.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSSatisfiable.java
new file mode 100644
index 00000000..75006570
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSSatisfiable.java
@@ -0,0 +1,19 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage;
+/**
+ * <!-- begin-user-doc -->
+ * A representation of the model object '<em><b>VLS Satisfiable</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ *
+ * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSSatisfiable()
+ * @model
+ * @generated
+ */
+public interface VLSSatisfiable extends VLSConfirmations
+{
+} // VLSSatisfiable
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTffFormula.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTffFormula.java
new file mode 100644
index 00000000..8b455f0a
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTffFormula.java
@@ -0,0 +1,133 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage;
+import org.eclipse.emf.ecore.EObject;
+/**
+ * <!-- begin-user-doc -->
+ * A representation of the model object '<em><b>VLS Tff Formula</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * <p>
+ * The following features are supported:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getName <em>Name</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofRole <em>Fof Role</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofFormula <em>Fof Formula</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getAnnotations <em>Annotations</em>}</li>
+ * </ul>
+ *
+ * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTffFormula()
+ * @model
+ * @generated
+ */
+public interface VLSTffFormula extends EObject
+{
+  /**
+   * Returns the value of the '<em><b>Name</b></em>' attribute.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Name</em>' attribute isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Name</em>' attribute.
+   * @see #setName(String)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTffFormula_Name()
+   * @model
+   * @generated
+   */
+  String getName();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getName <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Name</em>' attribute.
+   * @see #getName()
+   * @generated
+   */
+  void setName(String value);
+  /**
+   * Returns the value of the '<em><b>Fof Role</b></em>' attribute.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Fof Role</em>' attribute isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Fof Role</em>' attribute.
+   * @see #setFofRole(String)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTffFormula_FofRole()
+   * @model
+   * @generated
+   */
+  String getFofRole();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofRole <em>Fof Role</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Fof Role</em>' attribute.
+   * @see #getFofRole()
+   * @generated
+   */
+  void setFofRole(String value);
+  /**
+   * Returns the value of the '<em><b>Fof Formula</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Fof Formula</em>' containment reference isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Fof Formula</em>' containment reference.
+   * @see #setFofFormula(VLSTerm)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTffFormula_FofFormula()
+   * @model containment="true"
+   * @generated
+   */
+  VLSTerm getFofFormula();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofFormula <em>Fof Formula</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Fof Formula</em>' containment reference.
+   * @see #getFofFormula()
+   * @generated
+   */
+  void setFofFormula(VLSTerm value);
+  /**
+   * Returns the value of the '<em><b>Annotations</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Annotations</em>' containment reference isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Annotations</em>' containment reference.
+   * @see #setAnnotations(VLSAnnotation)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTffFormula_Annotations()
+   * @model containment="true"
+   * @generated
+   */
+  VLSAnnotation getAnnotations();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getAnnotations <em>Annotations</em>}' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Annotations</em>' containment reference.
+   * @see #getAnnotations()
+   * @generated
+   */
+  void setAnnotations(VLSAnnotation value);
+} // VLSTffFormula
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTrying.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTrying.java
new file mode 100644
index 00000000..c2080a9c
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VLSTrying.java
@@ -0,0 +1,52 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage;
+import org.eclipse.emf.ecore.EObject;
+/**
+ * <!-- begin-user-doc -->
+ * A representation of the model object '<em><b>VLS Trying</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * <p>
+ * The following features are supported:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying#getName <em>Name</em>}</li>
+ * </ul>
+ *
+ * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTrying()
+ * @model
+ * @generated
+ */
+public interface VLSTrying extends EObject
+{
+  /**
+   * Returns the value of the '<em><b>Name</b></em>' attribute.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Name</em>' attribute isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Name</em>' attribute.
+   * @see #setName(String)
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVLSTrying_Name()
+   * @model
+   * @generated
+   */
+  String getName();
+  /**
+   * Sets the value of the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying#getName <em>Name</em>}' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @param value the new value of the '<em>Name</em>' attribute.
+   * @see #getName()
+   * @generated
+   */
+  void setName(String value);
+} // VLSTrying
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java
index 3896cc7f..a89885ee 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguageFactory.java
@@ -60,6 +60,42 @@ public interface VampireLanguageFactory extends EFactory
  VLSComment createVLSComment();
  /**
+   * Returns a new object of class '<em>VLS Confirmations</em>'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return a new object of class '<em>VLS Confirmations</em>'.
+   * @generated
+   */
+  VLSConfirmations createVLSConfirmations();
+  /**
+   * Returns a new object of class '<em>VLS Satisfiable</em>'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return a new object of class '<em>VLS Satisfiable</em>'.
+   * @generated
+   */
+  VLSSatisfiable createVLSSatisfiable();
+  /**
+   * Returns a new object of class '<em>VLS Trying</em>'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return a new object of class '<em>VLS Trying</em>'.
+   * @generated
+   */
+  VLSTrying createVLSTrying();
+  /**
+   * Returns a new object of class '<em>VLS Finite Model</em>'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return a new object of class '<em>VLS Finite Model</em>'.
+   * @generated
+   */
+  VLSFiniteModel createVLSFiniteModel();
+  /**
   * Returns a new object of class '<em>VLS Fof Formula</em>'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -69,6 +105,15 @@ public interface VampireLanguageFactory extends EFactory
  VLSFofFormula createVLSFofFormula();
  /**
+   * Returns a new object of class '<em>VLS Tff Formula</em>'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return a new object of class '<em>VLS Tff Formula</em>'.
+   * @generated
+   */
+  VLSTffFormula createVLSTffFormula();
+  /**
   * Returns a new object of class '<em>VLS Annotation</em>'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
index f1519839..a9334a48 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireLanguagePackage.java
@@ -86,13 +86,31 @@ public interface VampireLanguagePackage extends EPackage
  int VAMPIRE_MODEL__COMMENTS = 1;
  /**
+   * The feature id for the '<em><b>Confirmations</b></em>' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VAMPIRE_MODEL__CONFIRMATIONS = 2;
+  /**
   * The feature id for the '<em><b>Formulas</b></em>' containment reference list.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
   * @ordered
   */
-  int VAMPIRE_MODEL__FORMULAS = 2;
+  int VAMPIRE_MODEL__FORMULAS = 3;
+  /**
+   * The feature id for the '<em><b>Tfformulas</b></em>' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VAMPIRE_MODEL__TFFORMULAS = 4;
  /**
   * The number of structural features of the '<em>Vampire Model</em>' class.
@@ -101,7 +119,7 @@ public interface VampireLanguagePackage extends EPackage
   * @generated
   * @ordered
   */
-  int VAMPIRE_MODEL_FEATURE_COUNT = 3;
+  int VAMPIRE_MODEL_FEATURE_COUNT = 5;
  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSIncludeImpl <em>VLS Include</em>}' class.
@@ -197,6 +215,91 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_COMMENT_FEATURE_COUNT = 1;
  /**
+   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSConfirmationsImpl <em>VLS Confirmations</em>}' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSConfirmationsImpl
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSConfirmations()
+   * @generated
+   */
+  int VLS_CONFIRMATIONS = 4;
+  /**
+   * The number of structural features of the '<em>VLS Confirmations</em>' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_CONFIRMATIONS_FEATURE_COUNT = 0;
+  /**
+   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSSatisfiableImpl <em>VLS Satisfiable</em>}' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSSatisfiableImpl
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSSatisfiable()
+   * @generated
+   */
+  int VLS_SATISFIABLE = 5;
+  /**
+   * The number of structural features of the '<em>VLS Satisfiable</em>' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_SATISFIABLE_FEATURE_COUNT = VLS_CONFIRMATIONS_FEATURE_COUNT + 0;
+  /**
+   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl <em>VLS Trying</em>}' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTrying()
+   * @generated
+   */
+  int VLS_TRYING = 6;
+  /**
+   * The feature id for the '<em><b>Name</b></em>' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_TRYING__NAME = 0;
+  /**
+   * The number of structural features of the '<em>VLS Trying</em>' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_TRYING_FEATURE_COUNT = 1;
+  /**
+   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl <em>VLS Finite Model</em>}' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFiniteModel()
+   * @generated
+   */
+  int VLS_FINITE_MODEL = 7;
+  /**
+   * The number of structural features of the '<em>VLS Finite Model</em>' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_FINITE_MODEL_FEATURE_COUNT = 0;
+  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl <em>VLS Fof Formula</em>}' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -204,7 +307,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFofFormula()
   * @generated
   */
-  int VLS_FOF_FORMULA = 4;
+  int VLS_FOF_FORMULA = 8;
  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
@@ -252,6 +355,61 @@ public interface VampireLanguagePackage extends EPackage
  int VLS_FOF_FORMULA_FEATURE_COUNT = 4;
  /**
+   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl <em>VLS Tff Formula</em>}' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTffFormula()
+   * @generated
+   */
+  int VLS_TFF_FORMULA = 9;
+  /**
+   * The feature id for the '<em><b>Name</b></em>' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_TFF_FORMULA__NAME = 0;
+  /**
+   * The feature id for the '<em><b>Fof Role</b></em>' attribute.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_TFF_FORMULA__FOF_ROLE = 1;
+  /**
+   * The feature id for the '<em><b>Fof Formula</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_TFF_FORMULA__FOF_FORMULA = 2;
+  /**
+   * The feature id for the '<em><b>Annotations</b></em>' containment reference.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_TFF_FORMULA__ANNOTATIONS = 3;
+  /**
+   * The number of structural features of the '<em>VLS Tff Formula</em>' class.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   * @ordered
+   */
+  int VLS_TFF_FORMULA_FEATURE_COUNT = 4;
+  /**
   * The meta object id for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAnnotationImpl <em>VLS Annotation</em>}' class.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -259,7 +417,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAnnotation()
   * @generated
   */
-  int VLS_ANNOTATION = 5;
+  int VLS_ANNOTATION = 10;
  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
@@ -305,7 +463,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTerm()
   * @generated
   */
-  int VLS_TERM = 6;
+  int VLS_TERM = 11;
  /**
   * The number of structural features of the '<em>VLS Term</em>' class.
@@ -324,7 +482,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSVariable()
   * @generated
   */
-  int VLS_VARIABLE = 7;
+  int VLS_VARIABLE = 12;
  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
@@ -352,7 +510,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFunctionFof()
   * @generated
   */
-  int VLS_FUNCTION_FOF = 8;
+  int VLS_FUNCTION_FOF = 13;
  /**
   * The feature id for the '<em><b>Functor</b></em>' attribute.
@@ -389,7 +547,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSDefinedTerm()
   * @generated
   */
-  int VLS_DEFINED_TERM = 9;
+  int VLS_DEFINED_TERM = 14;
  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
@@ -417,7 +575,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSEquivalent()
   * @generated
   */
-  int VLS_EQUIVALENT = 10;
+  int VLS_EQUIVALENT = 15;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -454,7 +612,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSImplies()
   * @generated
   */
-  int VLS_IMPLIES = 11;
+  int VLS_IMPLIES = 16;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -491,7 +649,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSRevImplies()
   * @generated
   */
-  int VLS_REV_IMPLIES = 12;
+  int VLS_REV_IMPLIES = 17;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -528,7 +686,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSXnor()
   * @generated
   */
-  int VLS_XNOR = 13;
+  int VLS_XNOR = 18;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -565,7 +723,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSNor()
   * @generated
   */
-  int VLS_NOR = 14;
+  int VLS_NOR = 19;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -602,7 +760,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSNand()
   * @generated
   */
-  int VLS_NAND = 15;
+  int VLS_NAND = 20;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -639,7 +797,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAnd()
   * @generated
   */
-  int VLS_AND = 16;
+  int VLS_AND = 21;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -676,7 +834,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSOr()
   * @generated
   */
-  int VLS_OR = 17;
+  int VLS_OR = 22;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -713,7 +871,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSUniversalQuantifier()
   * @generated
   */
-  int VLS_UNIVERSAL_QUANTIFIER = 18;
+  int VLS_UNIVERSAL_QUANTIFIER = 23;
  /**
   * The feature id for the '<em><b>Variables</b></em>' containment reference list.
@@ -750,7 +908,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSExistentialQuantifier()
   * @generated
   */
-  int VLS_EXISTENTIAL_QUANTIFIER = 19;
+  int VLS_EXISTENTIAL_QUANTIFIER = 24;
  /**
   * The feature id for the '<em><b>Variables</b></em>' containment reference list.
@@ -787,7 +945,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSUnaryNegation()
   * @generated
   */
-  int VLS_UNARY_NEGATION = 20;
+  int VLS_UNARY_NEGATION = 25;
  /**
   * The feature id for the '<em><b>Operand</b></em>' containment reference.
@@ -815,7 +973,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSInequality()
   * @generated
   */
-  int VLS_INEQUALITY = 21;
+  int VLS_INEQUALITY = 26;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -852,7 +1010,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSEquality()
   * @generated
   */
-  int VLS_EQUALITY = 22;
+  int VLS_EQUALITY = 27;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -889,7 +1047,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAssignment()
   * @generated
   */
-  int VLS_ASSIGNMENT = 23;
+  int VLS_ASSIGNMENT = 28;
  /**
   * The feature id for the '<em><b>Left</b></em>' containment reference.
@@ -926,7 +1084,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSConstant()
   * @generated
   */
-  int VLS_CONSTANT = 24;
+  int VLS_CONSTANT = 29;
  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
@@ -954,7 +1112,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTrue()
   * @generated
   */
-  int VLS_TRUE = 25;
+  int VLS_TRUE = 30;
  /**
   * The number of structural features of the '<em>VLS True</em>' class.
@@ -973,7 +1131,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFalse()
   * @generated
   */
-  int VLS_FALSE = 26;
+  int VLS_FALSE = 31;
  /**
   * The number of structural features of the '<em>VLS False</em>' class.
@@ -992,7 +1150,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFunction()
   * @generated
   */
-  int VLS_FUNCTION = 27;
+  int VLS_FUNCTION = 32;
  /**
   * The feature id for the '<em><b>Constant</b></em>' attribute.
@@ -1029,7 +1187,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSLess()
   * @generated
   */
-  int VLS_LESS = 28;
+  int VLS_LESS = 33;
  /**
   * The feature id for the '<em><b>Name</b></em>' attribute.
@@ -1066,7 +1224,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSInt()
   * @generated
   */
-  int VLS_INT = 29;
+  int VLS_INT = 34;
  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
@@ -1094,7 +1252,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSReal()
   * @generated
   */
-  int VLS_REAL = 30;
+  int VLS_REAL = 35;
  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
@@ -1122,7 +1280,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSRational()
   * @generated
   */
-  int VLS_RATIONAL = 31;
+  int VLS_RATIONAL = 36;
  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
@@ -1150,7 +1308,7 @@ public interface VampireLanguagePackage extends EPackage
   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSDoubleQuote()
   * @generated
   */
-  int VLS_DOUBLE_QUOTE = 32;
+  int VLS_DOUBLE_QUOTE = 37;
  /**
   * The feature id for the '<em><b>Value</b></em>' attribute.
@@ -1204,6 +1362,17 @@ public interface VampireLanguagePackage extends EPackage
  EReference getVampireModel_Comments();
  /**
+   * Returns the meta object for the containment reference list '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getConfirmations <em>Confirmations</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the containment reference list '<em>Confirmations</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getConfirmations()
+   * @see #getVampireModel()
+   * @generated
+   */
+  EReference getVampireModel_Confirmations();
+  /**
   * Returns the meta object for the containment reference list '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getFormulas <em>Formulas</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1215,6 +1384,17 @@ public interface VampireLanguagePackage extends EPackage
  EReference getVampireModel_Formulas();
  /**
+   * Returns the meta object for the containment reference list '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getTfformulas <em>Tfformulas</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the containment reference list '<em>Tfformulas</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getTfformulas()
+   * @see #getVampireModel()
+   * @generated
+   */
+  EReference getVampireModel_Tfformulas();
+  /**
   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude <em>VLS Include</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1289,6 +1469,57 @@ public interface VampireLanguagePackage extends EPackage
  EAttribute getVLSComment_Comment();
  /**
+   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations <em>VLS Confirmations</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for class '<em>VLS Confirmations</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations
+   * @generated
+   */
+  EClass getVLSConfirmations();
+  /**
+   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable <em>VLS Satisfiable</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for class '<em>VLS Satisfiable</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable
+   * @generated
+   */
+  EClass getVLSSatisfiable();
+  /**
+   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying <em>VLS Trying</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for class '<em>VLS Trying</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying
+   * @generated
+   */
+  EClass getVLSTrying();
+  /**
+   * Returns the meta object for the attribute '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying#getName <em>Name</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the attribute '<em>Name</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying#getName()
+   * @see #getVLSTrying()
+   * @generated
+   */
+  EAttribute getVLSTrying_Name();
+  /**
+   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel <em>VLS Finite Model</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for class '<em>VLS Finite Model</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel
+   * @generated
+   */
+  EClass getVLSFiniteModel();
+  /**
   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula <em>VLS Fof Formula</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -1343,6 +1574,60 @@ public interface VampireLanguagePackage extends EPackage
  EReference getVLSFofFormula_Annotations();
  /**
+   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula <em>VLS Tff Formula</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for class '<em>VLS Tff Formula</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula
+   * @generated
+   */
+  EClass getVLSTffFormula();
+  /**
+   * Returns the meta object for the attribute '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getName <em>Name</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the attribute '<em>Name</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getName()
+   * @see #getVLSTffFormula()
+   * @generated
+   */
+  EAttribute getVLSTffFormula_Name();
+  /**
+   * Returns the meta object for the attribute '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofRole <em>Fof Role</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the attribute '<em>Fof Role</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofRole()
+   * @see #getVLSTffFormula()
+   * @generated
+   */
+  EAttribute getVLSTffFormula_FofRole();
+  /**
+   * Returns the meta object for the containment reference '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofFormula <em>Fof Formula</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the containment reference '<em>Fof Formula</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getFofFormula()
+   * @see #getVLSTffFormula()
+   * @generated
+   */
+  EReference getVLSTffFormula_FofFormula();
+  /**
+   * Returns the meta object for the containment reference '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getAnnotations <em>Annotations</em>}'.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @return the meta object for the containment reference '<em>Annotations</em>'.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula#getAnnotations()
+   * @see #getVLSTffFormula()
+   * @generated
+   */
+  EReference getVLSTffFormula_Annotations();
+  /**
   * Returns the meta object for class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnnotation <em>VLS Annotation</em>}'.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -2101,6 +2386,14 @@ public interface VampireLanguagePackage extends EPackage
    EReference VAMPIRE_MODEL__COMMENTS = eINSTANCE.getVampireModel_Comments();
    /**
+     * The meta object literal for the '<em><b>Confirmations</b></em>' containment reference list feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EReference VAMPIRE_MODEL__CONFIRMATIONS = eINSTANCE.getVampireModel_Confirmations();
+    /**
     * The meta object literal for the '<em><b>Formulas</b></em>' containment reference list feature.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
@@ -2109,6 +2402,14 @@ public interface VampireLanguagePackage extends EPackage
    EReference VAMPIRE_MODEL__FORMULAS = eINSTANCE.getVampireModel_Formulas();
    /**
+     * The meta object literal for the '<em><b>Tfformulas</b></em>' containment reference list feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EReference VAMPIRE_MODEL__TFFORMULAS = eINSTANCE.getVampireModel_Tfformulas();
+    /**
     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSIncludeImpl <em>VLS Include</em>}' class.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
@@ -2171,6 +2472,54 @@ public interface VampireLanguagePackage extends EPackage
    EAttribute VLS_COMMENT__COMMENT = eINSTANCE.getVLSComment_Comment();
    /**
+     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSConfirmationsImpl <em>VLS Confirmations</em>}' class.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSConfirmationsImpl
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSConfirmations()
+     * @generated
+     */
+    EClass VLS_CONFIRMATIONS = eINSTANCE.getVLSConfirmations();
+    /**
+     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSSatisfiableImpl <em>VLS Satisfiable</em>}' class.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSSatisfiableImpl
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSSatisfiable()
+     * @generated
+     */
+    EClass VLS_SATISFIABLE = eINSTANCE.getVLSSatisfiable();
+    /**
+     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl <em>VLS Trying</em>}' class.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTrying()
+     * @generated
+     */
+    EClass VLS_TRYING = eINSTANCE.getVLSTrying();
+    /**
+     * The meta object literal for the '<em><b>Name</b></em>' attribute feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EAttribute VLS_TRYING__NAME = eINSTANCE.getVLSTrying_Name();
+    /**
+     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl <em>VLS Finite Model</em>}' class.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFiniteModelImpl
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFiniteModel()
+     * @generated
+     */
+    EClass VLS_FINITE_MODEL = eINSTANCE.getVLSFiniteModel();
+    /**
     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSFofFormulaImpl <em>VLS Fof Formula</em>}' class.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
@@ -2213,6 +2562,48 @@ public interface VampireLanguagePackage extends EPackage
    EReference VLS_FOF_FORMULA__ANNOTATIONS = eINSTANCE.getVLSFofFormula_Annotations();
    /**
+     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl <em>VLS Tff Formula</em>}' class.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl
+     * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTffFormula()
+     * @generated
+     */
+    EClass VLS_TFF_FORMULA = eINSTANCE.getVLSTffFormula();
+    /**
+     * The meta object literal for the '<em><b>Name</b></em>' attribute feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EAttribute VLS_TFF_FORMULA__NAME = eINSTANCE.getVLSTffFormula_Name();
+    /**
+     * The meta object literal for the '<em><b>Fof Role</b></em>' attribute feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EAttribute VLS_TFF_FORMULA__FOF_ROLE = eINSTANCE.getVLSTffFormula_FofRole();
+    /**
+     * The meta object literal for the '<em><b>Fof Formula</b></em>' containment reference feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EReference VLS_TFF_FORMULA__FOF_FORMULA = eINSTANCE.getVLSTffFormula_FofFormula();
+    /**
+     * The meta object literal for the '<em><b>Annotations</b></em>' containment reference feature.
+     * <!-- begin-user-doc -->
+     * <!-- end-user-doc -->
+     * @generated
+     */
+    EReference VLS_TFF_FORMULA__ANNOTATIONS = eINSTANCE.getVLSTffFormula_Annotations();
+    /**
     * The meta object literal for the '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSAnnotationImpl <em>VLS Annotation</em>}' class.
     * <!-- begin-user-doc -->
     * <!-- end-user-doc -->
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireModel.java
index fae3ccf5..be258228 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireModel.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/VampireModel.java
@@ -18,7 +18,9 @@ import org.eclipse.emf.ecore.EObject;
 * <ul>
 *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getIncludes <em>Includes</em>}</li>
 *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getComments <em>Comments</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getConfirmations <em>Confirmations</em>}</li>
 *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getFormulas <em>Formulas</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel#getTfformulas <em>Tfformulas</em>}</li>
 * </ul>
 *
 * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVampireModel()
@@ -60,6 +62,22 @@ public interface VampireModel extends EObject
  EList<VLSComment> getComments();
  /**
+   * Returns the value of the '<em><b>Confirmations</b></em>' containment reference list.
+   * The list contents are of type {@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations}.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Confirmations</em>' containment reference list isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Confirmations</em>' containment reference list.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVampireModel_Confirmations()
+   * @model containment="true"
+   * @generated
+   */
+  EList<VLSConfirmations> getConfirmations();
+  /**
   * Returns the value of the '<em><b>Formulas</b></em>' containment reference list.
   * The list contents are of type {@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula}.
   * <!-- begin-user-doc -->
@@ -75,4 +93,20 @@ public interface VampireModel extends EObject
   */
  EList<VLSFofFormula> getFormulas();
+  /**
+   * Returns the value of the '<em><b>Tfformulas</b></em>' containment reference list.
+   * The list contents are of type {@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula}.
+   * <!-- begin-user-doc -->
+   * <p>
+   * If the meaning of the '<em>Tfformulas</em>' containment reference list isn't clear,
+   * there really should be more of a description here...
+   * </p>
+   * <!-- end-user-doc -->
+   * @return the value of the '<em>Tfformulas</em>' containment reference list.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage#getVampireModel_Tfformulas()
+   * @model containment="true"
+   * @generated
+   */
+  EList<VLSTffFormula> getTfformulas();
 } // VampireModel
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSConfirmationsImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSConfirmationsImpl.java
new file mode 100644
index 00000000..fb4bbf82
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSConfirmationsImpl.java
@@ -0,0 +1,43 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations;
+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 Confirmations</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSConfirmationsImpl extends MinimalEObjectImpl.Container implements VLSConfirmations
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSConfirmationsImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_CONFIRMATIONS;
+  }
+} //VLSConfirmationsImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFiniteModelImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFiniteModelImpl.java
new file mode 100644
index 00000000..dfbbf6ed
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSFiniteModelImpl.java
@@ -0,0 +1,43 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel;
+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 Finite Model</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSFiniteModelImpl extends MinimalEObjectImpl.Container implements VLSFiniteModel
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSFiniteModelImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_FINITE_MODEL;
+  }
+} //VLSFiniteModelImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSSatisfiableImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSSatisfiableImpl.java
new file mode 100644
index 00000000..0c591e2f
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSSatisfiableImpl.java
@@ -0,0 +1,41 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable;
+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 Satisfiable</b></em>'.
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class VLSSatisfiableImpl extends VLSConfirmationsImpl implements VLSSatisfiable
+{
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  protected VLSSatisfiableImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_SATISFIABLE;
+  }
+} //VLSSatisfiableImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTffFormulaImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTffFormulaImpl.java
new file mode 100644
index 00000000..b20fa91c
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTffFormulaImpl.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.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula;
+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 Tff Formula</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl#getName <em>Name</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl#getFofRole <em>Fof Role</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl#getFofFormula <em>Fof Formula</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTffFormulaImpl#getAnnotations <em>Annotations</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSTffFormulaImpl extends MinimalEObjectImpl.Container implements VLSTffFormula
+{
+  /**
+   * 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 VLSTffFormulaImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_TFF_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_TFF_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_TFF_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_TFF_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_TFF_FORMULA__FOF_FORMULA, null, msgs);
+      if (newFofFormula != null)
+        msgs = ((InternalEObject)newFofFormula).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_TFF_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_TFF_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_TFF_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_TFF_FORMULA__ANNOTATIONS, null, msgs);
+      if (newAnnotations != null)
+        msgs = ((InternalEObject)newAnnotations).eInverseAdd(this, EOPPOSITE_FEATURE_BASE - VampireLanguagePackage.VLS_TFF_FORMULA__ANNOTATIONS, null, msgs);
+      msgs = basicSetAnnotations(newAnnotations, msgs);
+      if (msgs != null) msgs.dispatch();
+    }
+    else if (eNotificationRequired())
+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_TFF_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_TFF_FORMULA__FOF_FORMULA:
+        return basicSetFofFormula(null, msgs);
+      case VampireLanguagePackage.VLS_TFF_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_TFF_FORMULA__NAME:
+        return getName();
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_ROLE:
+        return getFofRole();
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_FORMULA:
+        return getFofFormula();
+      case VampireLanguagePackage.VLS_TFF_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_TFF_FORMULA__NAME:
+        setName((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_ROLE:
+        setFofRole((String)newValue);
+        return;
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_FORMULA:
+        setFofFormula((VLSTerm)newValue);
+        return;
+      case VampireLanguagePackage.VLS_TFF_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_TFF_FORMULA__NAME:
+        setName(NAME_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_ROLE:
+        setFofRole(FOF_ROLE_EDEFAULT);
+        return;
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_FORMULA:
+        setFofFormula((VLSTerm)null);
+        return;
+      case VampireLanguagePackage.VLS_TFF_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_TFF_FORMULA__NAME:
+        return NAME_EDEFAULT == null ? name != null : !NAME_EDEFAULT.equals(name);
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_ROLE:
+        return FOF_ROLE_EDEFAULT == null ? fofRole != null : !FOF_ROLE_EDEFAULT.equals(fofRole);
+      case VampireLanguagePackage.VLS_TFF_FORMULA__FOF_FORMULA:
+        return fofFormula != null;
+      case VampireLanguagePackage.VLS_TFF_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();
+  }
+} //VLSTffFormulaImpl
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTryingImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTryingImpl.java
new file mode 100644
index 00000000..40e62d9e
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTryingImpl.java
@@ -0,0 +1,178 @@
+/**
+ * generated by Xtext 2.12.0
+ */
+package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying;
+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 Trying</b></em>'.
+ * <!-- end-user-doc -->
+ * <p>
+ * The following features are implemented:
+ * </p>
+ * <ul>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTryingImpl#getName <em>Name</em>}</li>
+ * </ul>
+ *
+ * @generated
+ */
+public class VLSTryingImpl extends MinimalEObjectImpl.Container implements VLSTrying
+{
+  /**
+   * 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 VLSTryingImpl()
+  {
+    super();
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  @Override
+  protected EClass eStaticClass()
+  {
+    return VampireLanguagePackage.Literals.VLS_TRYING;
+  }
+  /**
+   * <!-- 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_TRYING__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_TRYING__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_TRYING__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_TRYING__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_TRYING__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();
+  }
+} //VLSTryingImpl
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
index 630fa8ce..cd4a7a01 100644
--- 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
@@ -69,7 +69,12 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
      case VampireLanguagePackage.VLS_INCLUDE: return createVLSInclude();
      case VampireLanguagePackage.VLS_NAME: return createVLSName();
      case VampireLanguagePackage.VLS_COMMENT: return createVLSComment();
+      case VampireLanguagePackage.VLS_CONFIRMATIONS: return createVLSConfirmations();
+      case VampireLanguagePackage.VLS_SATISFIABLE: return createVLSSatisfiable();
+      case VampireLanguagePackage.VLS_TRYING: return createVLSTrying();
+      case VampireLanguagePackage.VLS_FINITE_MODEL: return createVLSFiniteModel();
      case VampireLanguagePackage.VLS_FOF_FORMULA: return createVLSFofFormula();
+      case VampireLanguagePackage.VLS_TFF_FORMULA: return createVLSTffFormula();
      case VampireLanguagePackage.VLS_ANNOTATION: return createVLSAnnotation();
      case VampireLanguagePackage.VLS_TERM: return createVLSTerm();
      case VampireLanguagePackage.VLS_VARIABLE: return createVLSVariable();
@@ -152,6 +157,50 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public VLSConfirmations createVLSConfirmations()
+  {
+    VLSConfirmationsImpl vlsConfirmations = new VLSConfirmationsImpl();
+    return vlsConfirmations;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSSatisfiable createVLSSatisfiable()
+  {
+    VLSSatisfiableImpl vlsSatisfiable = new VLSSatisfiableImpl();
+    return vlsSatisfiable;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSTrying createVLSTrying()
+  {
+    VLSTryingImpl vlsTrying = new VLSTryingImpl();
+    return vlsTrying;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public VLSFiniteModel createVLSFiniteModel()
+  {
+    VLSFiniteModelImpl vlsFiniteModel = new VLSFiniteModelImpl();
+    return vlsFiniteModel;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public VLSFofFormula createVLSFofFormula()
  {
    VLSFofFormulaImpl vlsFofFormula = new VLSFofFormulaImpl();
@@ -163,6 +212,17 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public VLSTffFormula createVLSTffFormula()
+  {
+    VLSTffFormulaImpl vlsTffFormula = new VLSTffFormulaImpl();
+    return vlsTffFormula;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public VLSAnnotation createVLSAnnotation()
  {
    VLSAnnotationImpl vlsAnnotation = new VLSAnnotationImpl();
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
index 86921032..ff71ff74 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
@@ -7,6 +7,7 @@ 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.VLSConfirmations;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDefinedTerm;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
@@ -14,6 +15,7 @@ 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.VLSFiniteModel;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof;
@@ -29,8 +31,11 @@ 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.VLSSatisfiable;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
@@ -87,6 +92,34 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  private EClass vlsConfirmationsEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsSatisfiableEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsTryingEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  private EClass vlsFiniteModelEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  private EClass vlsFofFormulaEClass = null;
  /**
@@ -94,6 +127,13 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  private EClass vlsTffFormulaEClass = null;
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  private EClass vlsAnnotationEClass = null;
  /**
@@ -383,7 +423,7 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
-  public EReference getVampireModel_Formulas()
+  public EReference getVampireModel_Confirmations()
  {
    return (EReference)vampireModelEClass.getEStructuralFeatures().get(2);
  }
@@ -393,6 +433,26 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public EReference getVampireModel_Formulas()
+  {
+    return (EReference)vampireModelEClass.getEStructuralFeatures().get(3);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVampireModel_Tfformulas()
+  {
+    return (EReference)vampireModelEClass.getEStructuralFeatures().get(4);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public EClass getVLSInclude()
  {
    return vlsIncludeEClass;
@@ -463,6 +523,56 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public EClass getVLSConfirmations()
+  {
+    return vlsConfirmationsEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSSatisfiable()
+  {
+    return vlsSatisfiableEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSTrying()
+  {
+    return vlsTryingEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSTrying_Name()
+  {
+    return (EAttribute)vlsTryingEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EClass getVLSFiniteModel()
+  {
+    return vlsFiniteModelEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public EClass getVLSFofFormula()
  {
    return vlsFofFormulaEClass;
@@ -513,6 +623,56 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
   * <!-- end-user-doc -->
   * @generated
   */
+  public EClass getVLSTffFormula()
+  {
+    return vlsTffFormulaEClass;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSTffFormula_Name()
+  {
+    return (EAttribute)vlsTffFormulaEClass.getEStructuralFeatures().get(0);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EAttribute getVLSTffFormula_FofRole()
+  {
+    return (EAttribute)vlsTffFormulaEClass.getEStructuralFeatures().get(1);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSTffFormula_FofFormula()
+  {
+    return (EReference)vlsTffFormulaEClass.getEStructuralFeatures().get(2);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
+  public EReference getVLSTffFormula_Annotations()
+  {
+    return (EReference)vlsTffFormulaEClass.getEStructuralFeatures().get(3);
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public EClass getVLSAnnotation()
  {
    return vlsAnnotationEClass;
@@ -1211,7 +1371,9 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    vampireModelEClass = createEClass(VAMPIRE_MODEL);
    createEReference(vampireModelEClass, VAMPIRE_MODEL__INCLUDES);
    createEReference(vampireModelEClass, VAMPIRE_MODEL__COMMENTS);
+    createEReference(vampireModelEClass, VAMPIRE_MODEL__CONFIRMATIONS);
    createEReference(vampireModelEClass, VAMPIRE_MODEL__FORMULAS);
+    createEReference(vampireModelEClass, VAMPIRE_MODEL__TFFORMULAS);
    vlsIncludeEClass = createEClass(VLS_INCLUDE);
    createEAttribute(vlsIncludeEClass, VLS_INCLUDE__FILE_NAME);
@@ -1223,12 +1385,27 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    vlsCommentEClass = createEClass(VLS_COMMENT);
    createEAttribute(vlsCommentEClass, VLS_COMMENT__COMMENT);
+    vlsConfirmationsEClass = createEClass(VLS_CONFIRMATIONS);
+    vlsSatisfiableEClass = createEClass(VLS_SATISFIABLE);
+    vlsTryingEClass = createEClass(VLS_TRYING);
+    createEAttribute(vlsTryingEClass, VLS_TRYING__NAME);
+    vlsFiniteModelEClass = createEClass(VLS_FINITE_MODEL);
    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);
+    vlsTffFormulaEClass = createEClass(VLS_TFF_FORMULA);
+    createEAttribute(vlsTffFormulaEClass, VLS_TFF_FORMULA__NAME);
+    createEAttribute(vlsTffFormulaEClass, VLS_TFF_FORMULA__FOF_ROLE);
+    createEReference(vlsTffFormulaEClass, VLS_TFF_FORMULA__FOF_FORMULA);
+    createEReference(vlsTffFormulaEClass, VLS_TFF_FORMULA__ANNOTATIONS);
    vlsAnnotationEClass = createEClass(VLS_ANNOTATION);
    createEAttribute(vlsAnnotationEClass, VLS_ANNOTATION__NAME);
    createEReference(vlsAnnotationEClass, VLS_ANNOTATION__FOLLOWUP);
@@ -1354,6 +1531,7 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    // Set bounds for type parameters
    // Add supertypes to classes
+    vlsSatisfiableEClass.getESuperTypes().add(this.getVLSConfirmations());
    vlsVariableEClass.getESuperTypes().add(this.getVLSTerm());
    vlsFunctionFofEClass.getESuperTypes().add(this.getVLSTerm());
    vlsDefinedTermEClass.getESuperTypes().add(this.getVLSTerm());
@@ -1385,7 +1563,9 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    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_Confirmations(), this.getVLSConfirmations(), null, "confirmations", 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);
+    initEReference(getVampireModel_Tfformulas(), this.getVLSTffFormula(), null, "tfformulas", 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);
@@ -1397,12 +1577,27 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    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(vlsConfirmationsEClass, VLSConfirmations.class, "VLSConfirmations", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEClass(vlsSatisfiableEClass, VLSSatisfiable.class, "VLSSatisfiable", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEClass(vlsTryingEClass, VLSTrying.class, "VLSTrying", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSTrying_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSTrying.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEClass(vlsFiniteModelEClass, VLSFiniteModel.class, "VLSFiniteModel", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
    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(vlsTffFormulaEClass, VLSTffFormula.class, "VLSTffFormula", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);
+    initEAttribute(getVLSTffFormula_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSTffFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEAttribute(getVLSTffFormula_FofRole(), ecorePackage.getEString(), "fofRole", null, 0, 1, VLSTffFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSTffFormula_FofFormula(), this.getVLSTerm(), null, "fofFormula", null, 0, 1, VLSTffFormula.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);
+    initEReference(getVLSTffFormula_Annotations(), this.getVLSAnnotation(), null, "annotations", null, 0, 1, VLSTffFormula.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);
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
index ea3dabc7..05b3086c 100644
--- 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
@@ -4,8 +4,10 @@
 package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude;
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
@@ -33,7 +35,9 @@ import org.eclipse.emf.ecore.util.InternalEList;
 * <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#getConfirmations <em>Confirmations</em>}</li>
 *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl#getFormulas <em>Formulas</em>}</li>
+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl#getTfformulas <em>Tfformulas</em>}</li>
 * </ul>
 *
 * @generated
@@ -61,6 +65,16 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
  protected EList<VLSComment> comments;
  /**
+   * The cached value of the '{@link #getConfirmations() <em>Confirmations</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getConfirmations()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSConfirmations> confirmations;
+  /**
   * The cached value of the '{@link #getFormulas() <em>Formulas</em>}' containment reference list.
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
@@ -71,6 +85,16 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
  protected EList<VLSFofFormula> formulas;
  /**
+   * The cached value of the '{@link #getTfformulas() <em>Tfformulas</em>}' containment reference list.
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @see #getTfformulas()
+   * @generated
+   * @ordered
+   */
+  protected EList<VLSTffFormula> tfformulas;
+  /**
   * <!-- begin-user-doc -->
   * <!-- end-user-doc -->
   * @generated
@@ -124,6 +148,20 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
   * <!-- end-user-doc -->
   * @generated
   */
+  public EList<VLSConfirmations> getConfirmations()
+  {
+    if (confirmations == null)
+    {
+      confirmations = new EObjectContainmentEList<VLSConfirmations>(VLSConfirmations.class, this, VampireLanguagePackage.VAMPIRE_MODEL__CONFIRMATIONS);
+    }
+    return confirmations;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  public EList<VLSFofFormula> getFormulas()
  {
    if (formulas == null)
@@ -138,6 +176,20 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
   * <!-- end-user-doc -->
   * @generated
   */
+  public EList<VLSTffFormula> getTfformulas()
+  {
+    if (tfformulas == null)
+    {
+      tfformulas = new EObjectContainmentEList<VLSTffFormula>(VLSTffFormula.class, this, VampireLanguagePackage.VAMPIRE_MODEL__TFFORMULAS);
+    }
+    return tfformulas;
+  }
+  /**
+   * <!-- begin-user-doc -->
+   * <!-- end-user-doc -->
+   * @generated
+   */
  @Override
  public NotificationChain eInverseRemove(InternalEObject otherEnd, int featureID, NotificationChain msgs)
  {
@@ -147,8 +199,12 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
        return ((InternalEList<?>)getIncludes()).basicRemove(otherEnd, msgs);
      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
        return ((InternalEList<?>)getComments()).basicRemove(otherEnd, msgs);
+      case VampireLanguagePackage.VAMPIRE_MODEL__CONFIRMATIONS:
+        return ((InternalEList<?>)getConfirmations()).basicRemove(otherEnd, msgs);
      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
        return ((InternalEList<?>)getFormulas()).basicRemove(otherEnd, msgs);
+      case VampireLanguagePackage.VAMPIRE_MODEL__TFFORMULAS:
+        return ((InternalEList<?>)getTfformulas()).basicRemove(otherEnd, msgs);
    }
    return super.eInverseRemove(otherEnd, featureID, msgs);
  }
@@ -167,8 +223,12 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
        return getIncludes();
      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
        return getComments();
+      case VampireLanguagePackage.VAMPIRE_MODEL__CONFIRMATIONS:
+        return getConfirmations();
      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
        return getFormulas();
+      case VampireLanguagePackage.VAMPIRE_MODEL__TFFORMULAS:
+        return getTfformulas();
    }
    return super.eGet(featureID, resolve, coreType);
  }
@@ -192,10 +252,18 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
        getComments().clear();
        getComments().addAll((Collection<? extends VLSComment>)newValue);
        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__CONFIRMATIONS:
+        getConfirmations().clear();
+        getConfirmations().addAll((Collection<? extends VLSConfirmations>)newValue);
+        return;
      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
        getFormulas().clear();
        getFormulas().addAll((Collection<? extends VLSFofFormula>)newValue);
        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__TFFORMULAS:
+        getTfformulas().clear();
+        getTfformulas().addAll((Collection<? extends VLSTffFormula>)newValue);
+        return;
    }
    super.eSet(featureID, newValue);
  }
@@ -216,9 +284,15 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
        getComments().clear();
        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__CONFIRMATIONS:
+        getConfirmations().clear();
+        return;
      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
        getFormulas().clear();
        return;
+      case VampireLanguagePackage.VAMPIRE_MODEL__TFFORMULAS:
+        getTfformulas().clear();
+        return;
    }
    super.eUnset(featureID);
  }
@@ -237,8 +311,12 @@ public class VampireModelImpl extends MinimalEObjectImpl.Container implements Va
        return includes != null && !includes.isEmpty();
      case VampireLanguagePackage.VAMPIRE_MODEL__COMMENTS:
        return comments != null && !comments.isEmpty();
+      case VampireLanguagePackage.VAMPIRE_MODEL__CONFIRMATIONS:
+        return confirmations != null && !confirmations.isEmpty();
      case VampireLanguagePackage.VAMPIRE_MODEL__FORMULAS:
        return formulas != null && !formulas.isEmpty();
+      case VampireLanguagePackage.VAMPIRE_MODEL__TFFORMULAS:
+        return tfformulas != null && !tfformulas.isEmpty();
    }
    return super.eIsSet(featureID);
  }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java
index 8e096360..90781f47 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageAdapterFactory.java
@@ -96,11 +96,36 @@ public class VampireLanguageAdapterFactory extends AdapterFactoryImpl
        return createVLSCommentAdapter();
      }
      @Override
+      public Adapter caseVLSConfirmations(VLSConfirmations object)
+      {
+        return createVLSConfirmationsAdapter();
+      }
+      @Override
+      public Adapter caseVLSSatisfiable(VLSSatisfiable object)
+      {
+        return createVLSSatisfiableAdapter();
+      }
+      @Override
+      public Adapter caseVLSTrying(VLSTrying object)
+      {
+        return createVLSTryingAdapter();
+      }
+      @Override
+      public Adapter caseVLSFiniteModel(VLSFiniteModel object)
+      {
+        return createVLSFiniteModelAdapter();
+      }
+      @Override
      public Adapter caseVLSFofFormula(VLSFofFormula object)
      {
        return createVLSFofFormulaAdapter();
      }
      @Override
+      public Adapter caseVLSTffFormula(VLSTffFormula object)
+      {
+        return createVLSTffFormulaAdapter();
+      }
+      @Override
      public Adapter caseVLSAnnotation(VLSAnnotation object)
      {
        return createVLSAnnotationAdapter();
@@ -323,6 +348,66 @@ public class VampireLanguageAdapterFactory extends AdapterFactoryImpl
  }
  /**
+   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations <em>VLS Confirmations</em>}'.
+   * <!-- begin-user-doc -->
+   * This default implementation returns null so that we can easily ignore cases;
+   * it's useful to ignore a case when inheritance will catch all the cases anyway.
+   * <!-- end-user-doc -->
+   * @return the new adapter.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConfirmations
+   * @generated
+   */
+  public Adapter createVLSConfirmationsAdapter()
+  {
+    return null;
+  }
+  /**
+   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable <em>VLS Satisfiable</em>}'.
+   * <!-- begin-user-doc -->
+   * This default implementation returns null so that we can easily ignore cases;
+   * it's useful to ignore a case when inheritance will catch all the cases anyway.
+   * <!-- end-user-doc -->
+   * @return the new adapter.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable
+   * @generated
+   */
+  public Adapter createVLSSatisfiableAdapter()
+  {
+    return null;
+  }
+  /**
+   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying <em>VLS Trying</em>}'.
+   * <!-- begin-user-doc -->
+   * This default implementation returns null so that we can easily ignore cases;
+   * it's useful to ignore a case when inheritance will catch all the cases anyway.
+   * <!-- end-user-doc -->
+   * @return the new adapter.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying
+   * @generated
+   */
+  public Adapter createVLSTryingAdapter()
+  {
+    return null;
+  }
+  /**
+   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel <em>VLS Finite Model</em>}'.
+   * <!-- begin-user-doc -->
+   * This default implementation returns null so that we can easily ignore cases;
+   * it's useful to ignore a case when inheritance will catch all the cases anyway.
+   * <!-- end-user-doc -->
+   * @return the new adapter.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel
+   * @generated
+   */
+  public Adapter createVLSFiniteModelAdapter()
+  {
+    return null;
+  }
+  /**
   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula <em>VLS Fof Formula</em>}'.
   * <!-- begin-user-doc -->
   * This default implementation returns null so that we can easily ignore cases;
@@ -338,6 +423,21 @@ public class VampireLanguageAdapterFactory extends AdapterFactoryImpl
  }
  /**
+   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula <em>VLS Tff Formula</em>}'.
+   * <!-- begin-user-doc -->
+   * This default implementation returns null so that we can easily ignore cases;
+   * it's useful to ignore a case when inheritance will catch all the cases anyway.
+   * <!-- end-user-doc -->
+   * @return the new adapter.
+   * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula
+   * @generated
+   */
+  public Adapter createVLSTffFormulaAdapter()
+  {
+    return null;
+  }
+  /**
   * Creates a new adapter for an object of class '{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnnotation <em>VLS Annotation</em>}'.
   * <!-- begin-user-doc -->
   * This default implementation returns null so that we can easily ignore cases;
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
index 8d70157d..eddb3b4c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/util/VampireLanguageSwitch.java
@@ -101,6 +101,35 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        if (result == null) result = defaultCase(theEObject);
        return result;
      }
+      case VampireLanguagePackage.VLS_CONFIRMATIONS:
+      {
+        VLSConfirmations vlsConfirmations = (VLSConfirmations)theEObject;
+        T result = caseVLSConfirmations(vlsConfirmations);
+        if (result == null) result = defaultCase(theEObject);
+        return result;
+      }
+      case VampireLanguagePackage.VLS_SATISFIABLE:
+      {
+        VLSSatisfiable vlsSatisfiable = (VLSSatisfiable)theEObject;
+        T result = caseVLSSatisfiable(vlsSatisfiable);
+        if (result == null) result = caseVLSConfirmations(vlsSatisfiable);
+        if (result == null) result = defaultCase(theEObject);
+        return result;
+      }
+      case VampireLanguagePackage.VLS_TRYING:
+      {
+        VLSTrying vlsTrying = (VLSTrying)theEObject;
+        T result = caseVLSTrying(vlsTrying);
+        if (result == null) result = defaultCase(theEObject);
+        return result;
+      }
+      case VampireLanguagePackage.VLS_FINITE_MODEL:
+      {
+        VLSFiniteModel vlsFiniteModel = (VLSFiniteModel)theEObject;
+        T result = caseVLSFiniteModel(vlsFiniteModel);
+        if (result == null) result = defaultCase(theEObject);
+        return result;
+      }
      case VampireLanguagePackage.VLS_FOF_FORMULA:
      {
        VLSFofFormula vlsFofFormula = (VLSFofFormula)theEObject;
@@ -108,6 +137,13 @@ public class VampireLanguageSwitch<T> extends Switch<T>
        if (result == null) result = defaultCase(theEObject);
        return result;
      }
+      case VampireLanguagePackage.VLS_TFF_FORMULA:
+      {
+        VLSTffFormula vlsTffFormula = (VLSTffFormula)theEObject;
+        T result = caseVLSTffFormula(vlsTffFormula);
+        if (result == null) result = defaultCase(theEObject);
+        return result;
+      }
      case VampireLanguagePackage.VLS_ANNOTATION:
      {
        VLSAnnotation vlsAnnotation = (VLSAnnotation)theEObject;
@@ -403,6 +439,70 @@ public class VampireLanguageSwitch<T> extends Switch<T>
  }
  /**
+   * Returns the result of interpreting the object as an instance of '<em>VLS Confirmations</em>'.
+   * <!-- begin-user-doc -->
+   * This implementation returns null;
+   * returning a non-null result will terminate the switch.
+   * <!-- end-user-doc -->
+   * @param object the target of the switch.
+   * @return the result of interpreting the object as an instance of '<em>VLS Confirmations</em>'.
+   * @see #doSwitch(org.eclipse.emf.ecore.EObject) doSwitch(EObject)
+   * @generated
+   */
+  public T caseVLSConfirmations(VLSConfirmations object)
+  {
+    return null;
+  }
+  /**
+   * Returns the result of interpreting the object as an instance of '<em>VLS Satisfiable</em>'.
+   * <!-- begin-user-doc -->
+   * This implementation returns null;
+   * returning a non-null result will terminate the switch.
+   * <!-- end-user-doc -->
+   * @param object the target of the switch.
+   * @return the result of interpreting the object as an instance of '<em>VLS Satisfiable</em>'.
+   * @see #doSwitch(org.eclipse.emf.ecore.EObject) doSwitch(EObject)
+   * @generated
+   */
+  public T caseVLSSatisfiable(VLSSatisfiable object)
+  {
+    return null;
+  }
+  /**
+   * Returns the result of interpreting the object as an instance of '<em>VLS Trying</em>'.
+   * <!-- begin-user-doc -->
+   * This implementation returns null;
+   * returning a non-null result will terminate the switch.
+   * <!-- end-user-doc -->
+   * @param object the target of the switch.
+   * @return the result of interpreting the object as an instance of '<em>VLS Trying</em>'.
+   * @see #doSwitch(org.eclipse.emf.ecore.EObject) doSwitch(EObject)
+   * @generated
+   */
+  public T caseVLSTrying(VLSTrying object)
+  {
+    return null;
+  }
+  /**
+   * Returns the result of interpreting the object as an instance of '<em>VLS Finite Model</em>'.
+   * <!-- begin-user-doc -->
+   * This implementation returns null;
+   * returning a non-null result will terminate the switch.
+   * <!-- end-user-doc -->
+   * @param object the target of the switch.
+   * @return the result of interpreting the object as an instance of '<em>VLS Finite Model</em>'.
+   * @see #doSwitch(org.eclipse.emf.ecore.EObject) doSwitch(EObject)
+   * @generated
+   */
+  public T caseVLSFiniteModel(VLSFiniteModel object)
+  {
+    return null;
+  }
+  /**
   * Returns the result of interpreting the object as an instance of '<em>VLS Fof Formula</em>'.
   * <!-- begin-user-doc -->
   * This implementation returns null;
@@ -419,6 +519,22 @@ public class VampireLanguageSwitch<T> extends Switch<T>
  }
  /**
+   * Returns the result of interpreting the object as an instance of '<em>VLS Tff Formula</em>'.
+   * <!-- begin-user-doc -->
+   * This implementation returns null;
+   * returning a non-null result will terminate the switch.
+   * <!-- end-user-doc -->
+   * @param object the target of the switch.
+   * @return the result of interpreting the object as an instance of '<em>VLS Tff Formula</em>'.
+   * @see #doSwitch(org.eclipse.emf.ecore.EObject) doSwitch(EObject)
+   * @generated
+   */
+  public T caseVLSTffFormula(VLSTffFormula object)
+  {
+    return null;
+  }
+  /**
   * Returns the result of interpreting the object as an instance of '<em>VLS Annotation</em>'.
   * <!-- begin-user-doc -->
   * This implementation returns null;