9 files changed, 44 insertions, 440 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin
index ddc983a6..337977f1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtextbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java
index d763a193..890341db 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java
@@ -14,7 +14,6 @@ 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;

@@ -33,7 +32,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable;

 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;

@@ -103,9 +101,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
                         case VampireLanguagePackage.VLS_FALSE:

                                 sequence_VLSAtomicConstant(context, (VLSFalse) semanticObject); 

                                 return; 

-                        case VampireLanguagePackage.VLS_FINITE_MODEL:

-                                sequence_VLSFiniteModel(context, (VLSFiniteModel) semanticObject); 

-                                return; 

                         case VampireLanguagePackage.VLS_FOF_FORMULA:

                                 sequence_VLSFofFormula(context, (VLSFofFormula) semanticObject); 

                                 return; 

@@ -160,9 +155,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
                         case VampireLanguagePackage.VLS_TRUE:

                                 sequence_VLSAtomicConstant(context, (VLSTrue) semanticObject); 

                                 return; 

-                        case VampireLanguagePackage.VLS_TRYING:

-                                sequence_VLSTrying(context, (VLSTrying) semanticObject); 

-                                return; 

                         case VampireLanguagePackage.VLS_UNARY_NEGATION:

                                 sequence_VLSUnaryNegation(context, (VLSUnaryNegation) semanticObject); 

                                 return; 

@@ -782,18 +774,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
         

         /**

          * Contexts:

-         *     VLSFiniteModel returns VLSFiniteModel

-         *

-         * Constraint:

-         *     {VLSFiniteModel}

-         */

-        protected void sequence_VLSFiniteModel(ISerializationContext context, VLSFiniteModel semanticObject) {

-                genericSequencer.createSequence(context, semanticObject);

-        }

-        

-        

-        /**

-         * Contexts:

          *     VLSFofFormula returns VLSFofFormula

          *

          * Constraint:

@@ -868,24 +848,6 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic
         

         /**

          * Contexts:

-         *     VLSTrying returns VLSTrying

-         *

-         * Constraint:

-         *     name=LITERAL

-         */

-        protected void sequence_VLSTrying(ISerializationContext context, VLSTrying semanticObject) {

-                if (errorAcceptor != null) {

-                        if (transientValues.isValueTransient(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME) == ValueTransient.YES)

-                                errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME));

-                }

-                SequenceFeeder feeder = createSequencerFeeder(context, semanticObject);

-                feeder.accept(grammarAccess.getVLSTryingAccess().getNameLITERALTerminalRuleCall_2_0(), semanticObject.getName());

-                feeder.finish();

-        }

-        

-        

-        /**

-         * Contexts:

          *     VLSTerm returns VLSAssignment

          *     VLSBinary returns VLSAssignment

          *     VLSBinary.VLSEquivalent_1_0_0_0_0 returns VLSAssignment

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
index 64ba160f..c5bd8be2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/services/VampireLanguageGrammarAccess.java
@@ -234,64 +234,6 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 //'Satisfiable!'

                 public Keyword getSatisfiableKeyword_1() { return cSatisfiableKeyword_1; }

         }

-        public class VLSTryingElements extends AbstractParserRuleElementFinder {

-                private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTrying");

-                private final Group cGroup = (Group)rule.eContents().get(1);

-                private final Keyword cTRYINGKeyword_0 = (Keyword)cGroup.eContents().get(0);

-                private final Keyword cLeftSquareBracketKeyword_1 = (Keyword)cGroup.eContents().get(1);

-                private final Assignment cNameAssignment_2 = (Assignment)cGroup.eContents().get(2);

-                private final RuleCall cNameLITERALTerminalRuleCall_2_0 = (RuleCall)cNameAssignment_2.eContents().get(0);

-                private final Keyword cRightSquareBracketKeyword_3 = (Keyword)cGroup.eContents().get(3);

-                

-                //VLSTrying:

-                //      'TRYING' '[' name=LITERAL ']';

-                @Override public ParserRule getRule() { return rule; }

-                

-                //'TRYING' '[' name=LITERAL ']'

-                public Group getGroup() { return cGroup; }

-                

-                //'TRYING'

-                public Keyword getTRYINGKeyword_0() { return cTRYINGKeyword_0; }

-                

-                //'['

-                public Keyword getLeftSquareBracketKeyword_1() { return cLeftSquareBracketKeyword_1; }

-                

-                //name=LITERAL

-                public Assignment getNameAssignment_2() { return cNameAssignment_2; }

-                

-                //LITERAL

-                public RuleCall getNameLITERALTerminalRuleCall_2_0() { return cNameLITERALTerminalRuleCall_2_0; }

-                

-                //']'

-                public Keyword getRightSquareBracketKeyword_3() { return cRightSquareBracketKeyword_3; }

-        }

-        public class VLSFiniteModelElements extends AbstractParserRuleElementFinder {

-                private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFiniteModel");

-                private final Group cGroup = (Group)rule.eContents().get(1);

-                private final Action cVLSFiniteModelAction_0 = (Action)cGroup.eContents().get(0);

-                private final Keyword cFiniteKeyword_1 = (Keyword)cGroup.eContents().get(1);

-                private final Keyword cModelKeyword_2 = (Keyword)cGroup.eContents().get(2);

-                private final Keyword cFoundKeyword_3 = (Keyword)cGroup.eContents().get(3);

-                

-                //VLSFiniteModel:

-                //      {VLSFiniteModel} 'Finite' 'Model' 'Found!';

-                @Override public ParserRule getRule() { return rule; }

-                

-                //{VLSFiniteModel} 'Finite' 'Model' 'Found!'

-                public Group getGroup() { return cGroup; }

-                

-                //{VLSFiniteModel}

-                public Action getVLSFiniteModelAction_0() { return cVLSFiniteModelAction_0; }

-                

-                //'Finite'

-                public Keyword getFiniteKeyword_1() { return cFiniteKeyword_1; }

-                

-                //'Model'

-                public Keyword getModelKeyword_2() { return cModelKeyword_2; }

-                

-                //'Found!'

-                public Keyword getFoundKeyword_3() { return cFoundKeyword_3; }

-        }

         public class VLSFofFormulaElements extends AbstractParserRuleElementFinder {

                 private final ParserRule rule = (ParserRule) GrammarUtil.findRuleForName(getGrammar(), "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofFormula");

                 private final Group cGroup = (Group)rule.eContents().get(1);

@@ -315,6 +257,13 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 private final Keyword cRightParenthesisKeyword_8 = (Keyword)cGroup.eContents().get(8);

                 private final Keyword cFullStopKeyword_9 = (Keyword)cGroup.eContents().get(9);

                 

+                ////VLSTrying:

+                ////    'TRYING' '[' name = LITERAL ']'

+                ////;

+                ////

+                ////VLSFiniteModel:

+                ////    {VLSFiniteModel} 'Finite' 'Model' 'Found!'

+                ////;

                 //// <FOF formulas>

                 //VLSFofFormula:

                 //      'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','

@@ -1633,8 +1582,6 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
         private final VLSCommentElements pVLSComment;

         private final VLSConfirmationsElements pVLSConfirmations;

         private final VLSSatisfiableElements pVLSSatisfiable;

-        private final VLSTryingElements pVLSTrying;

-        private final VLSFiniteModelElements pVLSFiniteModel;

         private final VLSFofFormulaElements pVLSFofFormula;

         private final VLSTffFormulaElements pVLSTffFormula;

         private final VLSRoleElements pVLSRole;

@@ -1688,8 +1635,6 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 this.pVLSComment = new VLSCommentElements();

                 this.pVLSConfirmations = new VLSConfirmationsElements();

                 this.pVLSSatisfiable = new VLSSatisfiableElements();

-                this.pVLSTrying = new VLSTryingElements();

-                this.pVLSFiniteModel = new VLSFiniteModelElements();

                 this.pVLSFofFormula = new VLSFofFormulaElements();

                 this.pVLSTffFormula = new VLSTffFormulaElements();

                 this.pVLSRole = new VLSRoleElements();

@@ -1922,26 +1867,13 @@ public class VampireLanguageGrammarAccess extends AbstractGrammarElementFinder {
                 return getVLSSatisfiableAccess().getRule();

         }

         

-        //VLSTrying:

-        //      'TRYING' '[' name=LITERAL ']';

-        public VLSTryingElements getVLSTryingAccess() {

-                return pVLSTrying;

-        }

-        

-        public ParserRule getVLSTryingRule() {

-                return getVLSTryingAccess().getRule();

-        }

-        

-        //VLSFiniteModel:

-        //      {VLSFiniteModel} 'Finite' 'Model' 'Found!';

-        public VLSFiniteModelElements getVLSFiniteModelAccess() {

-                return pVLSFiniteModel;

-        }

-        

-        public ParserRule getVLSFiniteModelRule() {

-                return getVLSFiniteModelAccess().getRule();

-        }

-        

+        ////VLSTrying:

+        ////    'TRYING' '[' name = LITERAL ']'

+        ////;

+        ////

+        ////VLSFiniteModel:

+        ////    {VLSFiniteModel} 'Finite' 'Model' 'Found!'

+        ////;

         //// <FOF formulas>

         //VLSFofFormula:

         //      'fof' '(' name=(LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole=VLSRole ',' fofFormula=VLSTerm (','

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 a89885ee..84b65a59 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
@@ -78,24 +78,6 @@ public interface VampireLanguageFactory extends EFactory
   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 -->

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 a9334a48..e7df5378 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
@@ -253,53 +253,6 @@ public interface VampireLanguagePackage extends EPackage
   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 -->

@@ -307,7 +260,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFofFormula()

    * @generated

    */

-  int VLS_FOF_FORMULA = 8;

+  int VLS_FOF_FORMULA = 6;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -362,7 +315,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTffFormula()

    * @generated

    */

-  int VLS_TFF_FORMULA = 9;

+  int VLS_TFF_FORMULA = 7;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -417,7 +370,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAnnotation()

    * @generated

    */

-  int VLS_ANNOTATION = 10;

+  int VLS_ANNOTATION = 8;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -463,7 +416,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTerm()

    * @generated

    */

-  int VLS_TERM = 11;

+  int VLS_TERM = 9;

 

   /**

    * The number of structural features of the '<em>VLS Term</em>' class.

@@ -482,7 +435,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSVariable()

    * @generated

    */

-  int VLS_VARIABLE = 12;

+  int VLS_VARIABLE = 10;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -510,7 +463,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFunctionFof()

    * @generated

    */

-  int VLS_FUNCTION_FOF = 13;

+  int VLS_FUNCTION_FOF = 11;

 

   /**

    * The feature id for the '<em><b>Functor</b></em>' attribute.

@@ -547,7 +500,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSDefinedTerm()

    * @generated

    */

-  int VLS_DEFINED_TERM = 14;

+  int VLS_DEFINED_TERM = 12;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -575,7 +528,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSEquivalent()

    * @generated

    */

-  int VLS_EQUIVALENT = 15;

+  int VLS_EQUIVALENT = 13;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -612,7 +565,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSImplies()

    * @generated

    */

-  int VLS_IMPLIES = 16;

+  int VLS_IMPLIES = 14;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -649,7 +602,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSRevImplies()

    * @generated

    */

-  int VLS_REV_IMPLIES = 17;

+  int VLS_REV_IMPLIES = 15;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -686,7 +639,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSXnor()

    * @generated

    */

-  int VLS_XNOR = 18;

+  int VLS_XNOR = 16;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -723,7 +676,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSNor()

    * @generated

    */

-  int VLS_NOR = 19;

+  int VLS_NOR = 17;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -760,7 +713,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSNand()

    * @generated

    */

-  int VLS_NAND = 20;

+  int VLS_NAND = 18;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -797,7 +750,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAnd()

    * @generated

    */

-  int VLS_AND = 21;

+  int VLS_AND = 19;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -834,7 +787,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSOr()

    * @generated

    */

-  int VLS_OR = 22;

+  int VLS_OR = 20;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -871,7 +824,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSUniversalQuantifier()

    * @generated

    */

-  int VLS_UNIVERSAL_QUANTIFIER = 23;

+  int VLS_UNIVERSAL_QUANTIFIER = 21;

 

   /**

    * The feature id for the '<em><b>Variables</b></em>' containment reference list.

@@ -908,7 +861,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSExistentialQuantifier()

    * @generated

    */

-  int VLS_EXISTENTIAL_QUANTIFIER = 24;

+  int VLS_EXISTENTIAL_QUANTIFIER = 22;

 

   /**

    * The feature id for the '<em><b>Variables</b></em>' containment reference list.

@@ -945,7 +898,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSUnaryNegation()

    * @generated

    */

-  int VLS_UNARY_NEGATION = 25;

+  int VLS_UNARY_NEGATION = 23;

 

   /**

    * The feature id for the '<em><b>Operand</b></em>' containment reference.

@@ -973,7 +926,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSInequality()

    * @generated

    */

-  int VLS_INEQUALITY = 26;

+  int VLS_INEQUALITY = 24;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -1010,7 +963,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSEquality()

    * @generated

    */

-  int VLS_EQUALITY = 27;

+  int VLS_EQUALITY = 25;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -1047,7 +1000,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSAssignment()

    * @generated

    */

-  int VLS_ASSIGNMENT = 28;

+  int VLS_ASSIGNMENT = 26;

 

   /**

    * The feature id for the '<em><b>Left</b></em>' containment reference.

@@ -1084,7 +1037,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSConstant()

    * @generated

    */

-  int VLS_CONSTANT = 29;

+  int VLS_CONSTANT = 27;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -1112,7 +1065,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSTrue()

    * @generated

    */

-  int VLS_TRUE = 30;

+  int VLS_TRUE = 28;

 

   /**

    * The number of structural features of the '<em>VLS True</em>' class.

@@ -1131,7 +1084,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFalse()

    * @generated

    */

-  int VLS_FALSE = 31;

+  int VLS_FALSE = 29;

 

   /**

    * The number of structural features of the '<em>VLS False</em>' class.

@@ -1150,7 +1103,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSFunction()

    * @generated

    */

-  int VLS_FUNCTION = 32;

+  int VLS_FUNCTION = 30;

 

   /**

    * The feature id for the '<em><b>Constant</b></em>' attribute.

@@ -1187,7 +1140,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSLess()

    * @generated

    */

-  int VLS_LESS = 33;

+  int VLS_LESS = 31;

 

   /**

    * The feature id for the '<em><b>Name</b></em>' attribute.

@@ -1224,7 +1177,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSInt()

    * @generated

    */

-  int VLS_INT = 34;

+  int VLS_INT = 32;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1252,7 +1205,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSReal()

    * @generated

    */

-  int VLS_REAL = 35;

+  int VLS_REAL = 33;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1280,7 +1233,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSRational()

    * @generated

    */

-  int VLS_RATIONAL = 36;

+  int VLS_RATIONAL = 34;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1308,7 +1261,7 @@ public interface VampireLanguagePackage extends EPackage
    * @see ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguagePackageImpl#getVLSDoubleQuote()

    * @generated

    */

-  int VLS_DOUBLE_QUOTE = 37;

+  int VLS_DOUBLE_QUOTE = 35;

 

   /**

    * The feature id for the '<em><b>Value</b></em>' attribute.

@@ -1489,37 +1442,6 @@ public interface VampireLanguagePackage extends EPackage
   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 -->

@@ -2492,34 +2414,6 @@ public interface VampireLanguagePackage extends EPackage
     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 -->

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 cd4a7a01..c3c74fe9 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
@@ -71,8 +71,6 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
       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();

@@ -179,28 +177,6 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
    * <!-- 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();

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 ff71ff74..2b131272 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
@@ -15,7 +15,6 @@ 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;

@@ -35,7 +34,6 @@ 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;

@@ -106,20 +104,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    * <!-- 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;

 

   /**

@@ -543,36 +527,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    * <!-- 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;

@@ -1389,11 +1343,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
 

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

@@ -1581,11 +1530,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
 

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

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 90781f47..41e073ca 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
@@ -106,16 +106,6 @@ public class VampireLanguageAdapterFactory extends AdapterFactoryImpl
         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();

@@ -378,36 +368,6 @@ public class VampireLanguageAdapterFactory extends AdapterFactoryImpl
   }

 

   /**

-   * 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;

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 eddb3b4c..24ad4238 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
@@ -116,20 +116,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
         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;

@@ -471,38 +457,6 @@ public class VampireLanguageSwitch<T> extends Switch<T>
   }

 

   /**

-   * 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;