1 files changed, 2669 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g
new file mode 100644
index 00000000..2819b307
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/parser/antlr/internal/InternalVampireLanguage.g
@@ -0,0 +1,2669 @@
+/*
+ * generated by Xtext 2.12.0
+ */
+grammar InternalVampireLanguage;
+options {
+        superClass=AbstractInternalAntlrParser;
+}
+@lexer::header {
+package ca.mcgill.ecse.dslreasoner.parser.antlr.internal;
+// Hack: Use our own Lexer superclass by means of import. 
+// Currently there is no other way to specify the superclass for the lexer.
+import org.eclipse.xtext.parser.antlr.Lexer;
+}
+@parser::header {
+package ca.mcgill.ecse.dslreasoner.parser.antlr.internal;
+import org.eclipse.xtext.*;
+import org.eclipse.xtext.parser.*;
+import org.eclipse.xtext.parser.impl.*;
+import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.xtext.parser.antlr.AbstractInternalAntlrParser;
+import org.eclipse.xtext.parser.antlr.XtextTokenStream;
+import org.eclipse.xtext.parser.antlr.XtextTokenStream.HiddenTokens;
+import org.eclipse.xtext.parser.antlr.AntlrDatatypeRuleToken;
+import ca.mcgill.ecse.dslreasoner.services.VampireLanguageGrammarAccess;
+}
+@parser::members {
+        private VampireLanguageGrammarAccess grammarAccess;
+    public InternalVampireLanguageParser(TokenStream input, VampireLanguageGrammarAccess grammarAccess) {
+        this(input);
+        this.grammarAccess = grammarAccess;
+        registerRules(grammarAccess.getGrammar());
+    }
+    @Override
+    protected String getFirstRuleName() {
+        return "VampireModel";
+        }
+        @Override
+        protected VampireLanguageGrammarAccess getGrammarAccess() {
+                return grammarAccess;
+        }
+}
+@rulecatch {
+    catch (RecognitionException re) {
+        recover(input,re);
+        appendSkippedTokens();
+    }
+}
+// Entry rule entryRuleVampireModel
+entryRuleVampireModel returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVampireModelRule()); }
+        iv_ruleVampireModel=ruleVampireModel
+        { $current=$iv_ruleVampireModel.current; }
+        EOF;
+// Rule VampireModel
+ruleVampireModel returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVampireModelAccess().getIncludesVLSIncludeParserRuleCall_0_0());
+                                }
+                                lv_includes_0_0=ruleVLSInclude
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVampireModelRule());
+                                        }
+                                        add(
+                                                $current,
+                                                "includes",
+                                                lv_includes_0_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSInclude");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+                    |
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVampireModelAccess().getCommentsVLSCommentParserRuleCall_1_0());
+                                }
+                                lv_comments_1_0=ruleVLSComment
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVampireModelRule());
+                                        }
+                                        add(
+                                                $current,
+                                                "comments",
+                                                lv_comments_1_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSComment");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+                    |
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVampireModelAccess().getFormulasVLSFofFormulaParserRuleCall_2_0());
+                                }
+                                lv_formulas_2_0=ruleVLSFofFormula
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVampireModelRule());
+                                        }
+                                        add(
+                                                $current,
+                                                "formulas",
+                                                lv_formulas_2_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofFormula");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+        )*
+;
+// Entry rule entryRuleVLSInclude
+entryRuleVLSInclude returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSIncludeRule()); }
+        iv_ruleVLSInclude=ruleVLSInclude
+        { $current=$iv_ruleVLSInclude.current; }
+        EOF;
+// Rule VLSInclude
+ruleVLSInclude returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                otherlv_0='include('
+                {
+                        newLeafNode(otherlv_0, grammarAccess.getVLSIncludeAccess().getIncludeKeyword_0());
+                }
+                (
+                        (
+                                lv_fileName_1_0=RULE_SINGLE_QUOTE
+                                {
+                                        newLeafNode(lv_fileName_1_0, grammarAccess.getVLSIncludeAccess().getFileNameSINGLE_QUOTETerminalRuleCall_1_0());
+                                }
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElement(grammarAccess.getVLSIncludeRule());
+                                        }
+                                        setWithLastConsumed(
+                                                $current,
+                                                "fileName",
+                                                lv_fileName_1_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE");
+                                }
+                        )
+                )
+                (
+                        otherlv_2=',['
+                        {
+                                newLeafNode(otherlv_2, grammarAccess.getVLSIncludeAccess().getCommaLeftSquareBracketKeyword_2_0());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSIncludeAccess().getNamesVLSNameParserRuleCall_2_1_0());
+                                        }
+                                        lv_names_3_0=ruleVLSName
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSIncludeRule());
+                                                }
+                                                add(
+                                                        $current,
+                                                        "names",
+                                                        lv_names_3_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSName");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                        (
+                                otherlv_4=','
+                                {
+                                        newLeafNode(otherlv_4, grammarAccess.getVLSIncludeAccess().getCommaKeyword_2_2_0());
+                                }
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSIncludeAccess().getNamesVLSNameParserRuleCall_2_2_1_0());
+                                                }
+                                                lv_names_5_0=ruleVLSName
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSIncludeRule());
+                                                        }
+                                                        add(
+                                                                $current,
+                                                                "names",
+                                                                lv_names_5_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSName");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )*
+                        otherlv_6=']'
+                        {
+                                newLeafNode(otherlv_6, grammarAccess.getVLSIncludeAccess().getRightSquareBracketKeyword_2_3());
+                        }
+                )?
+        )
+;
+// Entry rule entryRuleVLSName
+entryRuleVLSName returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSNameRule()); }
+        iv_ruleVLSName=ruleVLSName
+        { $current=$iv_ruleVLSName.current; }
+        EOF;
+// Rule VLSName
+ruleVLSName returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        (
+                                lv_name_0_1=RULE_LOWER_WORD_ID
+                                {
+                                        newLeafNode(lv_name_0_1, grammarAccess.getVLSNameAccess().getNameLOWER_WORD_IDTerminalRuleCall_0_0());
+                                }
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElement(grammarAccess.getVLSNameRule());
+                                        }
+                                        setWithLastConsumed(
+                                                $current,
+                                                "name",
+                                                lv_name_0_1,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID");
+                                }
+                                    |
+                                lv_name_0_2=RULE_SINGLE_QUOTE
+                                {
+                                        newLeafNode(lv_name_0_2, grammarAccess.getVLSNameAccess().getNameSINGLE_QUOTETerminalRuleCall_0_1());
+                                }
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElement(grammarAccess.getVLSNameRule());
+                                        }
+                                        setWithLastConsumed(
+                                                $current,
+                                                "name",
+                                                lv_name_0_2,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE");
+                                }
+                                    |
+                                lv_name_0_3=RULE_LITERAL
+                                {
+                                        newLeafNode(lv_name_0_3, grammarAccess.getVLSNameAccess().getNameLITERALTerminalRuleCall_0_2());
+                                }
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElement(grammarAccess.getVLSNameRule());
+                                        }
+                                        setWithLastConsumed(
+                                                $current,
+                                                "name",
+                                                lv_name_0_3,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.LITERAL");
+                                }
+                                    |
+                                lv_name_0_4=RULE_SIGNED_LITERAL
+                                {
+                                        newLeafNode(lv_name_0_4, grammarAccess.getVLSNameAccess().getNameSIGNED_LITERALTerminalRuleCall_0_3());
+                                }
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElement(grammarAccess.getVLSNameRule());
+                                        }
+                                        setWithLastConsumed(
+                                                $current,
+                                                "name",
+                                                lv_name_0_4,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_LITERAL");
+                                }
+                        )
+                )
+        )
+;
+// Entry rule entryRuleVLSComment
+entryRuleVLSComment returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSCommentRule()); }
+        iv_ruleVLSComment=ruleVLSComment
+        { $current=$iv_ruleVLSComment.current; }
+        EOF;
+// Rule VLSComment
+ruleVLSComment returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        lv_comment_0_0=RULE_SINGLE_COMMENT
+                        {
+                                newLeafNode(lv_comment_0_0, grammarAccess.getVLSCommentAccess().getCommentSINGLE_COMMENTTerminalRuleCall_0());
+                        }
+                        {
+                                if ($current==null) {
+                                        $current = createModelElement(grammarAccess.getVLSCommentRule());
+                                }
+                                setWithLastConsumed(
+                                        $current,
+                                        "comment",
+                                        lv_comment_0_0,
+                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_COMMENT");
+                        }
+                )
+        )
+;
+// Entry rule entryRuleVLSFofFormula
+entryRuleVLSFofFormula returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSFofFormulaRule()); }
+        iv_ruleVLSFofFormula=ruleVLSFofFormula
+        { $current=$iv_ruleVLSFofFormula.current; }
+        EOF;
+// Rule VLSFofFormula
+ruleVLSFofFormula returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                otherlv_0='fof'
+                {
+                        newLeafNode(otherlv_0, grammarAccess.getVLSFofFormulaAccess().getFofKeyword_0());
+                }
+                otherlv_1='('
+                {
+                        newLeafNode(otherlv_1, grammarAccess.getVLSFofFormulaAccess().getLeftParenthesisKeyword_1());
+                }
+                (
+                        (
+                                (
+                                        lv_name_2_1=RULE_LOWER_WORD_ID
+                                        {
+                                                newLeafNode(lv_name_2_1, grammarAccess.getVLSFofFormulaAccess().getNameLOWER_WORD_IDTerminalRuleCall_2_0_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSFofFormulaRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "name",
+                                                        lv_name_2_1,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID");
+                                        }
+                                            |
+                                        lv_name_2_2=RULE_SIGNED_LITERAL
+                                        {
+                                                newLeafNode(lv_name_2_2, grammarAccess.getVLSFofFormulaAccess().getNameSIGNED_LITERALTerminalRuleCall_2_0_1());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSFofFormulaRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "name",
+                                                        lv_name_2_2,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_LITERAL");
+                                        }
+                                            |
+                                        lv_name_2_3=RULE_SINGLE_QUOTE
+                                        {
+                                                newLeafNode(lv_name_2_3, grammarAccess.getVLSFofFormulaAccess().getNameSINGLE_QUOTETerminalRuleCall_2_0_2());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSFofFormulaRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "name",
+                                                        lv_name_2_3,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE");
+                                        }
+                                )
+                        )
+                )
+                otherlv_3=','
+                {
+                        newLeafNode(otherlv_3, grammarAccess.getVLSFofFormulaAccess().getCommaKeyword_3());
+                }
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVLSFofFormulaAccess().getFofRoleVLSRoleParserRuleCall_4_0());
+                                }
+                                lv_fofRole_4_0=ruleVLSRole
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVLSFofFormulaRule());
+                                        }
+                                        set(
+                                                $current,
+                                                "fofRole",
+                                                lv_fofRole_4_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+                otherlv_5=','
+                {
+                        newLeafNode(otherlv_5, grammarAccess.getVLSFofFormulaAccess().getCommaKeyword_5());
+                }
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVLSFofFormulaAccess().getFofFormulaVLSTermParserRuleCall_6_0());
+                                }
+                                lv_fofFormula_6_0=ruleVLSTerm
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVLSFofFormulaRule());
+                                        }
+                                        set(
+                                                $current,
+                                                "fofFormula",
+                                                lv_fofFormula_6_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTerm");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+                (
+                        otherlv_7=','
+                        {
+                                newLeafNode(otherlv_7, grammarAccess.getVLSFofFormulaAccess().getCommaKeyword_7_0());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSFofFormulaAccess().getAnnotationsVLSAnnotationParserRuleCall_7_1_0());
+                                        }
+                                        lv_annotations_8_0=ruleVLSAnnotation
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSFofFormulaRule());
+                                                }
+                                                set(
+                                                        $current,
+                                                        "annotations",
+                                                        lv_annotations_8_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAnnotation");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                )?
+                otherlv_9=')'
+                {
+                        newLeafNode(otherlv_9, grammarAccess.getVLSFofFormulaAccess().getRightParenthesisKeyword_8());
+                }
+                otherlv_10='.'
+                {
+                        newLeafNode(otherlv_10, grammarAccess.getVLSFofFormulaAccess().getFullStopKeyword_9());
+                }
+        )
+;
+// Entry rule entryRuleVLSRole
+entryRuleVLSRole returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSRoleRule()); }
+        iv_ruleVLSRole=ruleVLSRole
+        { $current=$iv_ruleVLSRole.current.getText(); }
+        EOF;
+// Rule VLSRole
+ruleVLSRole returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSAxiomParserRuleCall_0());
+                }
+                this_VLSAxiom_0=ruleVLSAxiom
+                {
+                        $current.merge(this_VLSAxiom_0);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSConjectureParserRuleCall_1());
+                }
+                this_VLSConjecture_1=ruleVLSConjecture
+                {
+                        $current.merge(this_VLSConjecture_1);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSHypothesisParserRuleCall_2());
+                }
+                this_VLSHypothesis_2=ruleVLSHypothesis
+                {
+                        $current.merge(this_VLSHypothesis_2);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSDefinitionParserRuleCall_3());
+                }
+                this_VLSDefinition_3=ruleVLSDefinition
+                {
+                        $current.merge(this_VLSDefinition_3);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSAssumptionParserRuleCall_4());
+                }
+                this_VLSAssumption_4=ruleVLSAssumption
+                {
+                        $current.merge(this_VLSAssumption_4);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSLemmaParserRuleCall_5());
+                }
+                this_VLSLemma_5=ruleVLSLemma
+                {
+                        $current.merge(this_VLSLemma_5);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSTheoremParserRuleCall_6());
+                }
+                this_VLSTheorem_6=ruleVLSTheorem
+                {
+                        $current.merge(this_VLSTheorem_6);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSCorollaryParserRuleCall_7());
+                }
+                this_VLSCorollary_7=ruleVLSCorollary
+                {
+                        $current.merge(this_VLSCorollary_7);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSNegated_ConjectureParserRuleCall_8());
+                }
+                this_VLSNegated_Conjecture_8=ruleVLSNegated_Conjecture
+                {
+                        $current.merge(this_VLSNegated_Conjecture_8);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSPlainParserRuleCall_9());
+                }
+                this_VLSPlain_9=ruleVLSPlain
+                {
+                        $current.merge(this_VLSPlain_9);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSTypeParserRuleCall_10());
+                }
+                this_VLSType_10=ruleVLSType
+                {
+                        $current.merge(this_VLSType_10);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSFi_DomainParserRuleCall_11());
+                }
+                this_VLSFi_Domain_11=ruleVLSFi_Domain
+                {
+                        $current.merge(this_VLSFi_Domain_11);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSFi_FunctorsParserRuleCall_12());
+                }
+                this_VLSFi_Functors_12=ruleVLSFi_Functors
+                {
+                        $current.merge(this_VLSFi_Functors_12);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSFi_PredicatesParserRuleCall_13());
+                }
+                this_VLSFi_Predicates_13=ruleVLSFi_Predicates
+                {
+                        $current.merge(this_VLSFi_Predicates_13);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSRoleAccess().getVLSUnknownParserRuleCall_14());
+                }
+                this_VLSUnknown_14=ruleVLSUnknown
+                {
+                        $current.merge(this_VLSUnknown_14);
+                }
+                {
+                        afterParserOrEnumRuleCall();
+                }
+        )
+;
+// Entry rule entryRuleVLSAxiom
+entryRuleVLSAxiom returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSAxiomRule()); }
+        iv_ruleVLSAxiom=ruleVLSAxiom
+        { $current=$iv_ruleVLSAxiom.current.getText(); }
+        EOF;
+// Rule VLSAxiom
+ruleVLSAxiom returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='axiom'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSAxiomAccess().getAxiomKeyword());
+        }
+;
+// Entry rule entryRuleVLSConjecture
+entryRuleVLSConjecture returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSConjectureRule()); }
+        iv_ruleVLSConjecture=ruleVLSConjecture
+        { $current=$iv_ruleVLSConjecture.current.getText(); }
+        EOF;
+// Rule VLSConjecture
+ruleVLSConjecture returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='conjecture'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSConjectureAccess().getConjectureKeyword());
+        }
+;
+// Entry rule entryRuleVLSHypothesis
+entryRuleVLSHypothesis returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSHypothesisRule()); }
+        iv_ruleVLSHypothesis=ruleVLSHypothesis
+        { $current=$iv_ruleVLSHypothesis.current.getText(); }
+        EOF;
+// Rule VLSHypothesis
+ruleVLSHypothesis returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='hypothesis'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSHypothesisAccess().getHypothesisKeyword());
+        }
+;
+// Entry rule entryRuleVLSDefinition
+entryRuleVLSDefinition returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSDefinitionRule()); }
+        iv_ruleVLSDefinition=ruleVLSDefinition
+        { $current=$iv_ruleVLSDefinition.current.getText(); }
+        EOF;
+// Rule VLSDefinition
+ruleVLSDefinition returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='definition'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSDefinitionAccess().getDefinitionKeyword());
+        }
+;
+// Entry rule entryRuleVLSAssumption
+entryRuleVLSAssumption returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSAssumptionRule()); }
+        iv_ruleVLSAssumption=ruleVLSAssumption
+        { $current=$iv_ruleVLSAssumption.current.getText(); }
+        EOF;
+// Rule VLSAssumption
+ruleVLSAssumption returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='assumption'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSAssumptionAccess().getAssumptionKeyword());
+        }
+;
+// Entry rule entryRuleVLSLemma
+entryRuleVLSLemma returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSLemmaRule()); }
+        iv_ruleVLSLemma=ruleVLSLemma
+        { $current=$iv_ruleVLSLemma.current.getText(); }
+        EOF;
+// Rule VLSLemma
+ruleVLSLemma returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='lemma'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSLemmaAccess().getLemmaKeyword());
+        }
+;
+// Entry rule entryRuleVLSTheorem
+entryRuleVLSTheorem returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSTheoremRule()); }
+        iv_ruleVLSTheorem=ruleVLSTheorem
+        { $current=$iv_ruleVLSTheorem.current.getText(); }
+        EOF;
+// Rule VLSTheorem
+ruleVLSTheorem returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='theorem'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSTheoremAccess().getTheoremKeyword());
+        }
+;
+// Entry rule entryRuleVLSCorollary
+entryRuleVLSCorollary returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSCorollaryRule()); }
+        iv_ruleVLSCorollary=ruleVLSCorollary
+        { $current=$iv_ruleVLSCorollary.current.getText(); }
+        EOF;
+// Rule VLSCorollary
+ruleVLSCorollary returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='corollary'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSCorollaryAccess().getCorollaryKeyword());
+        }
+;
+// Entry rule entryRuleVLSNegated_Conjecture
+entryRuleVLSNegated_Conjecture returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSNegated_ConjectureRule()); }
+        iv_ruleVLSNegated_Conjecture=ruleVLSNegated_Conjecture
+        { $current=$iv_ruleVLSNegated_Conjecture.current.getText(); }
+        EOF;
+// Rule VLSNegated_Conjecture
+ruleVLSNegated_Conjecture returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='negated_conjecture'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSNegated_ConjectureAccess().getNegated_conjectureKeyword());
+        }
+;
+// Entry rule entryRuleVLSPlain
+entryRuleVLSPlain returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSPlainRule()); }
+        iv_ruleVLSPlain=ruleVLSPlain
+        { $current=$iv_ruleVLSPlain.current.getText(); }
+        EOF;
+// Rule VLSPlain
+ruleVLSPlain returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='plain'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSPlainAccess().getPlainKeyword());
+        }
+;
+// Entry rule entryRuleVLSType
+entryRuleVLSType returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSTypeRule()); }
+        iv_ruleVLSType=ruleVLSType
+        { $current=$iv_ruleVLSType.current.getText(); }
+        EOF;
+// Rule VLSType
+ruleVLSType returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='type'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSTypeAccess().getTypeKeyword());
+        }
+;
+// Entry rule entryRuleVLSFi_Domain
+entryRuleVLSFi_Domain returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSFi_DomainRule()); }
+        iv_ruleVLSFi_Domain=ruleVLSFi_Domain
+        { $current=$iv_ruleVLSFi_Domain.current.getText(); }
+        EOF;
+// Rule VLSFi_Domain
+ruleVLSFi_Domain returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='fi_domain'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSFi_DomainAccess().getFi_domainKeyword());
+        }
+;
+// Entry rule entryRuleVLSFi_Functors
+entryRuleVLSFi_Functors returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSFi_FunctorsRule()); }
+        iv_ruleVLSFi_Functors=ruleVLSFi_Functors
+        { $current=$iv_ruleVLSFi_Functors.current.getText(); }
+        EOF;
+// Rule VLSFi_Functors
+ruleVLSFi_Functors returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='fi_functors'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSFi_FunctorsAccess().getFi_functorsKeyword());
+        }
+;
+// Entry rule entryRuleVLSFi_Predicates
+entryRuleVLSFi_Predicates returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSFi_PredicatesRule()); }
+        iv_ruleVLSFi_Predicates=ruleVLSFi_Predicates
+        { $current=$iv_ruleVLSFi_Predicates.current.getText(); }
+        EOF;
+// Rule VLSFi_Predicates
+ruleVLSFi_Predicates returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='fi_predicates'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSFi_PredicatesAccess().getFi_predicatesKeyword());
+        }
+;
+// Entry rule entryRuleVLSUnknown
+entryRuleVLSUnknown returns [String current=null]:
+        { newCompositeNode(grammarAccess.getVLSUnknownRule()); }
+        iv_ruleVLSUnknown=ruleVLSUnknown
+        { $current=$iv_ruleVLSUnknown.current.getText(); }
+        EOF;
+// Rule VLSUnknown
+ruleVLSUnknown returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        kw='unknown'
+        {
+                $current.merge(kw);
+                newLeafNode(kw, grammarAccess.getVLSUnknownAccess().getUnknownKeyword());
+        }
+;
+// Entry rule entryRuleVLSAnnotation
+entryRuleVLSAnnotation returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSAnnotationRule()); }
+        iv_ruleVLSAnnotation=ruleVLSAnnotation
+        { $current=$iv_ruleVLSAnnotation.current; }
+        EOF;
+// Rule VLSAnnotation
+ruleVLSAnnotation returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        otherlv_0='['
+                        {
+                                newLeafNode(otherlv_0, grammarAccess.getVLSAnnotationAccess().getLeftSquareBracketKeyword_0());
+                        }
+                )?
+                (
+                        (
+                                (
+                                        lv_name_1_1=RULE_LOWER_WORD_ID
+                                        {
+                                                newLeafNode(lv_name_1_1, grammarAccess.getVLSAnnotationAccess().getNameLOWER_WORD_IDTerminalRuleCall_1_0_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSAnnotationRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "name",
+                                                        lv_name_1_1,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID");
+                                        }
+                                            |
+                                        lv_name_1_2=RULE_SINGLE_QUOTE
+                                        {
+                                                newLeafNode(lv_name_1_2, grammarAccess.getVLSAnnotationAccess().getNameSINGLE_QUOTETerminalRuleCall_1_0_1());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSAnnotationRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "name",
+                                                        lv_name_1_2,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE");
+                                        }
+                                            |
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSAnnotationAccess().getNameVLSRoleParserRuleCall_1_0_2());
+                                        }
+                                        lv_name_1_3=ruleVLSRole
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSAnnotationRule());
+                                                }
+                                                set(
+                                                        $current,
+                                                        "name",
+                                                        lv_name_1_3,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                )?
+                (
+                        otherlv_2='('
+                        {
+                                newLeafNode(otherlv_2, grammarAccess.getVLSAnnotationAccess().getLeftParenthesisKeyword_2_0());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSAnnotationAccess().getFollowupVLSAnnotationTermsParserRuleCall_2_1_0());
+                                        }
+                                        lv_followup_3_0=ruleVLSAnnotationTerms
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSAnnotationRule());
+                                                }
+                                                set(
+                                                        $current,
+                                                        "followup",
+                                                        lv_followup_3_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAnnotationTerms");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                        otherlv_4=')'
+                        {
+                                newLeafNode(otherlv_4, grammarAccess.getVLSAnnotationAccess().getRightParenthesisKeyword_2_2());
+                        }
+                )?
+                (
+                        otherlv_5=']'
+                        {
+                                newLeafNode(otherlv_5, grammarAccess.getVLSAnnotationAccess().getRightSquareBracketKeyword_3());
+                        }
+                )?
+        )
+;
+// Entry rule entryRuleVLSAnnotationTerms
+entryRuleVLSAnnotationTerms returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSAnnotationTermsRule()); }
+        iv_ruleVLSAnnotationTerms=ruleVLSAnnotationTerms
+        { $current=$iv_ruleVLSAnnotationTerms.current; }
+        EOF;
+// Rule VLSAnnotationTerms
+ruleVLSAnnotationTerms returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVLSAnnotationTermsAccess().getTermsVLSAnnotationParserRuleCall_0_0());
+                                }
+                                lv_terms_0_0=ruleVLSAnnotation
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVLSAnnotationTermsRule());
+                                        }
+                                        add(
+                                                $current,
+                                                "terms",
+                                                lv_terms_0_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAnnotation");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+                (
+                        otherlv_1=','
+                        {
+                                newLeafNode(otherlv_1, grammarAccess.getVLSAnnotationTermsAccess().getCommaKeyword_1_0());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSAnnotationTermsAccess().getTermsVLSAnnotationParserRuleCall_1_1_0());
+                                        }
+                                        lv_terms_2_0=ruleVLSAnnotation
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSAnnotationTermsRule());
+                                                }
+                                                add(
+                                                        $current,
+                                                        "terms",
+                                                        lv_terms_2_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAnnotation");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                )*
+        )
+;
+// Entry rule entryRuleVLSTerm
+entryRuleVLSTerm returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSTermRule()); }
+        iv_ruleVLSTerm=ruleVLSTerm
+        { $current=$iv_ruleVLSTerm.current; }
+        EOF;
+// Rule VLSTerm
+ruleVLSTerm returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        {
+                newCompositeNode(grammarAccess.getVLSTermAccess().getVLSBinaryParserRuleCall());
+        }
+        this_VLSBinary_0=ruleVLSBinary
+        {
+                $current = $this_VLSBinary_0.current;
+                afterParserOrEnumRuleCall();
+        }
+;
+// Entry rule entryRuleVLSBinary
+entryRuleVLSBinary returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSBinaryRule()); }
+        iv_ruleVLSBinary=ruleVLSBinary
+        { $current=$iv_ruleVLSBinary.current; }
+        EOF;
+// Rule VLSBinary
+ruleVLSBinary returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                {
+                        newCompositeNode(grammarAccess.getVLSBinaryAccess().getVLSUnitaryFormulaParserRuleCall_0());
+                }
+                this_VLSUnitaryFormula_0=ruleVLSUnitaryFormula
+                {
+                        $current = $this_VLSUnitaryFormula_0.current;
+                        afterParserOrEnumRuleCall();
+                }
+                (
+                        (
+                                (
+                                        (
+                                                (
+                                                        {
+                                                                $current = forceCreateModelElementAndSet(
+                                                                        grammarAccess.getVLSBinaryAccess().getVLSEquivalentLeftAction_1_0_0_0_0(),
+                                                                        $current);
+                                                        }
+                                                )
+                                                otherlv_2='<=>'
+                                                {
+                                                        newLeafNode(otherlv_2, grammarAccess.getVLSBinaryAccess().getLessThanSignEqualsSignGreaterThanSignKeyword_1_0_0_0_1());
+                                                }
+                                        )
+                                            |
+                                        (
+                                                (
+                                                        {
+                                                                $current = forceCreateModelElementAndSet(
+                                                                        grammarAccess.getVLSBinaryAccess().getVLSImpliesLeftAction_1_0_0_1_0(),
+                                                                        $current);
+                                                        }
+                                                )
+                                                otherlv_4='=>'
+                                                {
+                                                        newLeafNode(otherlv_4, grammarAccess.getVLSBinaryAccess().getEqualsSignGreaterThanSignKeyword_1_0_0_1_1());
+                                                }
+                                        )
+                                            |
+                                        (
+                                                (
+                                                        {
+                                                                $current = forceCreateModelElementAndSet(
+                                                                        grammarAccess.getVLSBinaryAccess().getVLSRevImpliesLeftAction_1_0_0_2_0(),
+                                                                        $current);
+                                                        }
+                                                )
+                                                otherlv_6='<='
+                                                {
+                                                        newLeafNode(otherlv_6, grammarAccess.getVLSBinaryAccess().getLessThanSignEqualsSignKeyword_1_0_0_2_1());
+                                                }
+                                        )
+                                            |
+                                        (
+                                                (
+                                                        {
+                                                                $current = forceCreateModelElementAndSet(
+                                                                        grammarAccess.getVLSBinaryAccess().getVLSXnorLeftAction_1_0_0_3_0(),
+                                                                        $current);
+                                                        }
+                                                )
+                                                otherlv_8='<~>'
+                                                {
+                                                        newLeafNode(otherlv_8, grammarAccess.getVLSBinaryAccess().getLessThanSignTildeGreaterThanSignKeyword_1_0_0_3_1());
+                                                }
+                                        )
+                                            |
+                                        (
+                                                (
+                                                        {
+                                                                $current = forceCreateModelElementAndSet(
+                                                                        grammarAccess.getVLSBinaryAccess().getVLSNorLeftAction_1_0_0_4_0(),
+                                                                        $current);
+                                                        }
+                                                )
+                                                otherlv_10='~|'
+                                                {
+                                                        newLeafNode(otherlv_10, grammarAccess.getVLSBinaryAccess().getTildeVerticalLineKeyword_1_0_0_4_1());
+                                                }
+                                        )
+                                            |
+                                        (
+                                                (
+                                                        {
+                                                                $current = forceCreateModelElementAndSet(
+                                                                        grammarAccess.getVLSBinaryAccess().getVLSNandLeftAction_1_0_0_5_0(),
+                                                                        $current);
+                                                        }
+                                                )
+                                                otherlv_12='~&'
+                                                {
+                                                        newLeafNode(otherlv_12, grammarAccess.getVLSBinaryAccess().getTildeAmpersandKeyword_1_0_0_5_1());
+                                                }
+                                        )
+                                )
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSBinaryAccess().getRightVLSUnitaryFormulaParserRuleCall_1_0_1_0());
+                                                }
+                                                lv_right_13_0=ruleVLSUnitaryFormula
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSBinaryRule());
+                                                        }
+                                                        set(
+                                                                $current,
+                                                                "right",
+                                                                lv_right_13_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryFormula");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )
+                            |
+                        (
+                                (
+                                        {
+                                                $current = forceCreateModelElementAndSet(
+                                                        grammarAccess.getVLSBinaryAccess().getVLSAndLeftAction_1_1_0(),
+                                                        $current);
+                                        }
+                                )
+                                otherlv_15='&'
+                                {
+                                        newLeafNode(otherlv_15, grammarAccess.getVLSBinaryAccess().getAmpersandKeyword_1_1_1());
+                                }
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSBinaryAccess().getRightVLSUnitaryFormulaParserRuleCall_1_1_2_0());
+                                                }
+                                                lv_right_16_0=ruleVLSUnitaryFormula
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSBinaryRule());
+                                                        }
+                                                        set(
+                                                                $current,
+                                                                "right",
+                                                                lv_right_16_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryFormula");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )+
+                            |
+                        (
+                                (
+                                        {
+                                                $current = forceCreateModelElementAndSet(
+                                                        grammarAccess.getVLSBinaryAccess().getVLSOrLeftAction_1_2_0(),
+                                                        $current);
+                                        }
+                                )
+                                otherlv_18='|'
+                                {
+                                        newLeafNode(otherlv_18, grammarAccess.getVLSBinaryAccess().getVerticalLineKeyword_1_2_1());
+                                }
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSBinaryAccess().getRightVLSUnitaryFormulaParserRuleCall_1_2_2_0());
+                                                }
+                                                lv_right_19_0=ruleVLSUnitaryFormula
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSBinaryRule());
+                                                        }
+                                                        set(
+                                                                $current,
+                                                                "right",
+                                                                lv_right_19_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryFormula");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )+
+                )?
+        )
+;
+// Entry rule entryRuleVLSUnitaryFormula
+entryRuleVLSUnitaryFormula returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSUnitaryFormulaRule()); }
+        iv_ruleVLSUnitaryFormula=ruleVLSUnitaryFormula
+        { $current=$iv_ruleVLSUnitaryFormula.current; }
+        EOF;
+// Rule VLSUnitaryFormula
+ruleVLSUnitaryFormula returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                {
+                        newCompositeNode(grammarAccess.getVLSUnitaryFormulaAccess().getVLSUniversalQuantifierParserRuleCall_0());
+                }
+                this_VLSUniversalQuantifier_0=ruleVLSUniversalQuantifier
+                {
+                        $current = $this_VLSUniversalQuantifier_0.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSUnitaryFormulaAccess().getVLSExistentialQuantifierParserRuleCall_1());
+                }
+                this_VLSExistentialQuantifier_1=ruleVLSExistentialQuantifier
+                {
+                        $current = $this_VLSExistentialQuantifier_1.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSUnitaryFormulaAccess().getVLSUnaryNegationParserRuleCall_2());
+                }
+                this_VLSUnaryNegation_2=ruleVLSUnaryNegation
+                {
+                        $current = $this_VLSUnaryNegation_2.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSUnitaryFormulaAccess().getVLSUnaryInfixParserRuleCall_3());
+                }
+                this_VLSUnaryInfix_3=ruleVLSUnaryInfix
+                {
+                        $current = $this_VLSUnaryInfix_3.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                (
+                        otherlv_4='('
+                        {
+                                newLeafNode(otherlv_4, grammarAccess.getVLSUnitaryFormulaAccess().getLeftParenthesisKeyword_4_0());
+                        }
+                        {
+                                newCompositeNode(grammarAccess.getVLSUnitaryFormulaAccess().getVLSTermParserRuleCall_4_1());
+                        }
+                        this_VLSTerm_5=ruleVLSTerm
+                        {
+                                $current = $this_VLSTerm_5.current;
+                                afterParserOrEnumRuleCall();
+                        }
+                        otherlv_6=')'
+                        {
+                                newLeafNode(otherlv_6, grammarAccess.getVLSUnitaryFormulaAccess().getRightParenthesisKeyword_4_2());
+                        }
+                )
+        )
+;
+// Entry rule entryRuleVLSUniversalQuantifier
+entryRuleVLSUniversalQuantifier returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSUniversalQuantifierRule()); }
+        iv_ruleVLSUniversalQuantifier=ruleVLSUniversalQuantifier
+        { $current=$iv_ruleVLSUniversalQuantifier.current; }
+        EOF;
+// Rule VLSUniversalQuantifier
+ruleVLSUniversalQuantifier returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        {
+                                $current = forceCreateModelElement(
+                                        grammarAccess.getVLSUniversalQuantifierAccess().getVLSUniversalQuantifierAction_0(),
+                                        $current);
+                        }
+                )
+                (
+                        otherlv_1='!'
+                        {
+                                newLeafNode(otherlv_1, grammarAccess.getVLSUniversalQuantifierAccess().getExclamationMarkKeyword_1_0());
+                        }
+                        otherlv_2='['
+                        {
+                                newLeafNode(otherlv_2, grammarAccess.getVLSUniversalQuantifierAccess().getLeftSquareBracketKeyword_1_1());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_2_0());
+                                        }
+                                        lv_variables_3_0=ruleVLSVariable
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule());
+                                                }
+                                                add(
+                                                        $current,
+                                                        "variables",
+                                                        lv_variables_3_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                        (
+                                otherlv_4=','
+                                {
+                                        newLeafNode(otherlv_4, grammarAccess.getVLSUniversalQuantifierAccess().getCommaKeyword_1_3_0());
+                                }
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0());
+                                                }
+                                                lv_variables_5_0=ruleVLSVariable
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule());
+                                                        }
+                                                        add(
+                                                                $current,
+                                                                "variables",
+                                                                lv_variables_5_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )*
+                        otherlv_6=']'
+                        {
+                                newLeafNode(otherlv_6, grammarAccess.getVLSUniversalQuantifierAccess().getRightSquareBracketKeyword_1_4());
+                        }
+                        otherlv_7=':'
+                        {
+                                newLeafNode(otherlv_7, grammarAccess.getVLSUniversalQuantifierAccess().getColonKeyword_1_5());
+                        }
+                )
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getOperandVLSUnitaryFormulaParserRuleCall_2_0());
+                                }
+                                lv_operand_8_0=ruleVLSUnitaryFormula
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule());
+                                        }
+                                        set(
+                                                $current,
+                                                "operand",
+                                                lv_operand_8_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryFormula");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+        )
+;
+// Entry rule entryRuleVLSExistentialQuantifier
+entryRuleVLSExistentialQuantifier returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSExistentialQuantifierRule()); }
+        iv_ruleVLSExistentialQuantifier=ruleVLSExistentialQuantifier
+        { $current=$iv_ruleVLSExistentialQuantifier.current; }
+        EOF;
+// Rule VLSExistentialQuantifier
+ruleVLSExistentialQuantifier returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        {
+                                $current = forceCreateModelElement(
+                                        grammarAccess.getVLSExistentialQuantifierAccess().getVLSExistentialQuantifierAction_0(),
+                                        $current);
+                        }
+                )
+                (
+                        otherlv_1='?'
+                        {
+                                newLeafNode(otherlv_1, grammarAccess.getVLSExistentialQuantifierAccess().getQuestionMarkKeyword_1_0());
+                        }
+                        otherlv_2='['
+                        {
+                                newLeafNode(otherlv_2, grammarAccess.getVLSExistentialQuantifierAccess().getLeftSquareBracketKeyword_1_1());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_2_0());
+                                        }
+                                        lv_variables_3_0=ruleVLSVariable
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule());
+                                                }
+                                                add(
+                                                        $current,
+                                                        "variables",
+                                                        lv_variables_3_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                        (
+                                otherlv_4=','
+                                {
+                                        newLeafNode(otherlv_4, grammarAccess.getVLSExistentialQuantifierAccess().getCommaKeyword_1_3_0());
+                                }
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0());
+                                                }
+                                                lv_variables_5_0=ruleVLSVariable
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule());
+                                                        }
+                                                        add(
+                                                                $current,
+                                                                "variables",
+                                                                lv_variables_5_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )*
+                        otherlv_6=']'
+                        {
+                                newLeafNode(otherlv_6, grammarAccess.getVLSExistentialQuantifierAccess().getRightSquareBracketKeyword_1_4());
+                        }
+                        otherlv_7=':'
+                        {
+                                newLeafNode(otherlv_7, grammarAccess.getVLSExistentialQuantifierAccess().getColonKeyword_1_5());
+                        }
+                )
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getOperandVLSUnitaryFormulaParserRuleCall_2_0());
+                                }
+                                lv_operand_8_0=ruleVLSUnitaryFormula
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule());
+                                        }
+                                        set(
+                                                $current,
+                                                "operand",
+                                                lv_operand_8_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryFormula");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+        )
+;
+// Entry rule entryRuleVLSUnaryNegation
+entryRuleVLSUnaryNegation returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSUnaryNegationRule()); }
+        iv_ruleVLSUnaryNegation=ruleVLSUnaryNegation
+        { $current=$iv_ruleVLSUnaryNegation.current; }
+        EOF;
+// Rule VLSUnaryNegation
+ruleVLSUnaryNegation returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        {
+                                $current = forceCreateModelElement(
+                                        grammarAccess.getVLSUnaryNegationAccess().getVLSUnaryNegationAction_0(),
+                                        $current);
+                        }
+                )
+                otherlv_1='~'
+                {
+                        newLeafNode(otherlv_1, grammarAccess.getVLSUnaryNegationAccess().getTildeKeyword_1());
+                }
+                (
+                        (
+                                {
+                                        newCompositeNode(grammarAccess.getVLSUnaryNegationAccess().getOperandVLSUnitaryFormulaParserRuleCall_2_0());
+                                }
+                                lv_operand_2_0=ruleVLSUnitaryFormula
+                                {
+                                        if ($current==null) {
+                                                $current = createModelElementForParent(grammarAccess.getVLSUnaryNegationRule());
+                                        }
+                                        set(
+                                                $current,
+                                                "operand",
+                                                lv_operand_2_0,
+                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryFormula");
+                                        afterParserOrEnumRuleCall();
+                                }
+                        )
+                )
+        )
+;
+// Entry rule entryRuleVLSUnaryInfix
+entryRuleVLSUnaryInfix returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSUnaryInfixRule()); }
+        iv_ruleVLSUnaryInfix=ruleVLSUnaryInfix
+        { $current=$iv_ruleVLSUnaryInfix.current; }
+        EOF;
+// Rule VLSUnaryInfix
+ruleVLSUnaryInfix returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                {
+                        newCompositeNode(grammarAccess.getVLSUnaryInfixAccess().getVLSAtomicParserRuleCall_0());
+                }
+                this_VLSAtomic_0=ruleVLSAtomic
+                {
+                        $current = $this_VLSAtomic_0.current;
+                        afterParserOrEnumRuleCall();
+                }
+                (
+                        (
+                                (
+                                        (
+                                                {
+                                                        $current = forceCreateModelElementAndSet(
+                                                                grammarAccess.getVLSUnaryInfixAccess().getVLSInequalityLeftAction_1_0_0_0(),
+                                                                $current);
+                                                }
+                                        )
+                                        otherlv_2='!='
+                                        {
+                                                newLeafNode(otherlv_2, grammarAccess.getVLSUnaryInfixAccess().getExclamationMarkEqualsSignKeyword_1_0_0_1());
+                                        }
+                                )
+                                    |
+                                (
+                                        (
+                                                {
+                                                        $current = forceCreateModelElementAndSet(
+                                                                grammarAccess.getVLSUnaryInfixAccess().getVLSEqualityLeftAction_1_0_1_0(),
+                                                                $current);
+                                                }
+                                        )
+                                        otherlv_4='='
+                                        {
+                                                newLeafNode(otherlv_4, grammarAccess.getVLSUnaryInfixAccess().getEqualsSignKeyword_1_0_1_1());
+                                        }
+                                )
+                                    |
+                                (
+                                        (
+                                                {
+                                                        $current = forceCreateModelElementAndSet(
+                                                                grammarAccess.getVLSUnaryInfixAccess().getVLSAssignmentLeftAction_1_0_2_0(),
+                                                                $current);
+                                                }
+                                        )
+                                        otherlv_6=':='
+                                        {
+                                                newLeafNode(otherlv_6, grammarAccess.getVLSUnaryInfixAccess().getColonEqualsSignKeyword_1_0_2_1());
+                                        }
+                                )
+                        )
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSUnaryInfixAccess().getRightVLSAtomicParserRuleCall_1_1_0());
+                                        }
+                                        lv_right_7_0=ruleVLSAtomic
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSUnaryInfixRule());
+                                                }
+                                                set(
+                                                        $current,
+                                                        "right",
+                                                        lv_right_7_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomic");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                )?
+        )
+;
+// Entry rule entryRuleVLSAtomic
+entryRuleVLSAtomic returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSAtomicRule()); }
+        iv_ruleVLSAtomic=ruleVLSAtomic
+        { $current=$iv_ruleVLSAtomic.current; }
+        EOF;
+// Rule VLSAtomic
+ruleVLSAtomic returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                {
+                        newCompositeNode(grammarAccess.getVLSAtomicAccess().getVLSAtomicConstantParserRuleCall_0());
+                }
+                this_VLSAtomicConstant_0=ruleVLSAtomicConstant
+                {
+                        $current = $this_VLSAtomicConstant_0.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSAtomicAccess().getVLSAtomicFunctionParserRuleCall_1());
+                }
+                this_VLSAtomicFunction_1=ruleVLSAtomicFunction
+                {
+                        $current = $this_VLSAtomicFunction_1.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSAtomicAccess().getVLSVariableParserRuleCall_2());
+                }
+                this_VLSVariable_2=ruleVLSVariable
+                {
+                        $current = $this_VLSVariable_2.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSAtomicAccess().getVLSDefinedTermParserRuleCall_3());
+                }
+                this_VLSDefinedTerm_3=ruleVLSDefinedTerm
+                {
+                        $current = $this_VLSDefinedTerm_3.current;
+                        afterParserOrEnumRuleCall();
+                }
+        )
+;
+// Entry rule entryRuleVLSAtomicConstant
+entryRuleVLSAtomicConstant returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSAtomicConstantRule()); }
+        iv_ruleVLSAtomicConstant=ruleVLSAtomicConstant
+        { $current=$iv_ruleVLSAtomicConstant.current; }
+        EOF;
+// Rule VLSAtomicConstant
+ruleVLSAtomicConstant returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSAtomicConstantAccess().getVLSConstantAction_0_0(),
+                                                $current);
+                                }
+                        )
+                        (
+                                (
+                                        (
+                                                lv_name_1_1=RULE_LOWER_WORD_ID
+                                                {
+                                                        newLeafNode(lv_name_1_1, grammarAccess.getVLSAtomicConstantAccess().getNameLOWER_WORD_IDTerminalRuleCall_0_1_0_0());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicConstantRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "name",
+                                                                lv_name_1_1,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID");
+                                                }
+                                                    |
+                                                lv_name_1_2=RULE_SINGLE_QUOTE
+                                                {
+                                                        newLeafNode(lv_name_1_2, grammarAccess.getVLSAtomicConstantAccess().getNameSINGLE_QUOTETerminalRuleCall_0_1_0_1());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicConstantRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "name",
+                                                                lv_name_1_2,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE");
+                                                }
+                                                    |
+                                                lv_name_1_3=RULE_DOLLAR_ID
+                                                {
+                                                        newLeafNode(lv_name_1_3, grammarAccess.getVLSAtomicConstantAccess().getNameDOLLAR_IDTerminalRuleCall_0_1_0_2());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicConstantRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "name",
+                                                                lv_name_1_3,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOLLAR_ID");
+                                                }
+                                                    |
+                                                lv_name_1_4=RULE_DOUBLE_DOLLAR_ID
+                                                {
+                                                        newLeafNode(lv_name_1_4, grammarAccess.getVLSAtomicConstantAccess().getNameDOUBLE_DOLLAR_IDTerminalRuleCall_0_1_0_3());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicConstantRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "name",
+                                                                lv_name_1_4,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOUBLE_DOLLAR_ID");
+                                                }
+                                                    |
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSAtomicConstantAccess().getNameVLSRoleParserRuleCall_0_1_0_4());
+                                                }
+                                                lv_name_1_5=ruleVLSRole
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSAtomicConstantRule());
+                                                        }
+                                                        set(
+                                                                $current,
+                                                                "name",
+                                                                lv_name_1_5,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )
+                )
+                    |
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSAtomicConstantAccess().getVLSTrueAction_1_0(),
+                                                $current);
+                                }
+                        )
+                        otherlv_3='$true'
+                        {
+                                newLeafNode(otherlv_3, grammarAccess.getVLSAtomicConstantAccess().getTrueKeyword_1_1());
+                        }
+                )
+                    |
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSAtomicConstantAccess().getVLSFalseAction_2_0(),
+                                                $current);
+                                }
+                        )
+                        otherlv_5='$false'
+                        {
+                                newLeafNode(otherlv_5, grammarAccess.getVLSAtomicConstantAccess().getFalseKeyword_2_1());
+                        }
+                )
+        )
+;
+// Entry rule entryRuleVLSAtomicFunction
+entryRuleVLSAtomicFunction returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSAtomicFunctionRule()); }
+        iv_ruleVLSAtomicFunction=ruleVLSAtomicFunction
+        { $current=$iv_ruleVLSAtomicFunction.current; }
+        EOF;
+// Rule VLSAtomicFunction
+ruleVLSAtomicFunction returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSAtomicFunctionAccess().getVLSFunctionAction_0_0(),
+                                                $current);
+                                }
+                        )
+                        (
+                                (
+                                        (
+                                                lv_constant_1_1=RULE_LOWER_WORD_ID
+                                                {
+                                                        newLeafNode(lv_constant_1_1, grammarAccess.getVLSAtomicFunctionAccess().getConstantLOWER_WORD_IDTerminalRuleCall_0_1_0_0());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicFunctionRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "constant",
+                                                                lv_constant_1_1,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID");
+                                                }
+                                                    |
+                                                lv_constant_1_2=RULE_SINGLE_QUOTE
+                                                {
+                                                        newLeafNode(lv_constant_1_2, grammarAccess.getVLSAtomicFunctionAccess().getConstantSINGLE_QUOTETerminalRuleCall_0_1_0_1());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicFunctionRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "constant",
+                                                                lv_constant_1_2,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE");
+                                                }
+                                                    |
+                                                lv_constant_1_3=RULE_DOLLAR_ID
+                                                {
+                                                        newLeafNode(lv_constant_1_3, grammarAccess.getVLSAtomicFunctionAccess().getConstantDOLLAR_IDTerminalRuleCall_0_1_0_2());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicFunctionRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "constant",
+                                                                lv_constant_1_3,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOLLAR_ID");
+                                                }
+                                                    |
+                                                lv_constant_1_4=RULE_DOUBLE_DOLLAR_ID
+                                                {
+                                                        newLeafNode(lv_constant_1_4, grammarAccess.getVLSAtomicFunctionAccess().getConstantDOUBLE_DOLLAR_IDTerminalRuleCall_0_1_0_3());
+                                                }
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElement(grammarAccess.getVLSAtomicFunctionRule());
+                                                        }
+                                                        setWithLastConsumed(
+                                                                $current,
+                                                                "constant",
+                                                                lv_constant_1_4,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOUBLE_DOLLAR_ID");
+                                                }
+                                                    |
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSAtomicFunctionAccess().getConstantVLSRoleParserRuleCall_0_1_0_4());
+                                                }
+                                                lv_constant_1_5=ruleVLSRole
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSAtomicFunctionRule());
+                                                        }
+                                                        set(
+                                                                $current,
+                                                                "constant",
+                                                                lv_constant_1_5,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )
+                        (
+                                otherlv_2='('
+                                {
+                                        newLeafNode(otherlv_2, grammarAccess.getVLSAtomicFunctionAccess().getLeftParenthesisKeyword_0_2_0());
+                                }
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSAtomicFunctionAccess().getTermsVLSFofTermParserRuleCall_0_2_1_0());
+                                                }
+                                                lv_terms_3_0=ruleVLSFofTerm
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSAtomicFunctionRule());
+                                                        }
+                                                        add(
+                                                                $current,
+                                                                "terms",
+                                                                lv_terms_3_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                                (
+                                        otherlv_4=','
+                                        {
+                                                newLeafNode(otherlv_4, grammarAccess.getVLSAtomicFunctionAccess().getCommaKeyword_0_2_2_0());
+                                        }
+                                        (
+                                                (
+                                                        {
+                                                                newCompositeNode(grammarAccess.getVLSAtomicFunctionAccess().getTermsVLSFofTermParserRuleCall_0_2_2_1_0());
+                                                        }
+                                                        lv_terms_5_0=ruleVLSFofTerm
+                                                        {
+                                                                if ($current==null) {
+                                                                        $current = createModelElementForParent(grammarAccess.getVLSAtomicFunctionRule());
+                                                                }
+                                                                add(
+                                                                        $current,
+                                                                        "terms",
+                                                                        lv_terms_5_0,
+                                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
+                                                                afterParserOrEnumRuleCall();
+                                                        }
+                                                )
+                                        )
+                                )*
+                                otherlv_6=')'
+                                {
+                                        newLeafNode(otherlv_6, grammarAccess.getVLSAtomicFunctionAccess().getRightParenthesisKeyword_0_2_3());
+                                }
+                        )
+                )
+                    |
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSAtomicFunctionAccess().getVLSLessAction_1_0(),
+                                                $current);
+                                }
+                        )
+                        (
+                                (
+                                        lv_name_8_0='$less'
+                                        {
+                                                newLeafNode(lv_name_8_0, grammarAccess.getVLSAtomicFunctionAccess().getNameLessKeyword_1_1_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSAtomicFunctionRule());
+                                                }
+                                                setWithLastConsumed($current, "name", lv_name_8_0, "\$less");
+                                        }
+                                )
+                        )
+                        otherlv_9='('
+                        {
+                                newLeafNode(otherlv_9, grammarAccess.getVLSAtomicFunctionAccess().getLeftParenthesisKeyword_1_2());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSAtomicFunctionAccess().getTermsVLSFofTermParserRuleCall_1_3_0());
+                                        }
+                                        lv_terms_10_0=ruleVLSFofTerm
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSAtomicFunctionRule());
+                                                }
+                                                add(
+                                                        $current,
+                                                        "terms",
+                                                        lv_terms_10_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                        otherlv_11=','
+                        {
+                                newLeafNode(otherlv_11, grammarAccess.getVLSAtomicFunctionAccess().getCommaKeyword_1_4());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSAtomicFunctionAccess().getTermsVLSFofTermParserRuleCall_1_5_0());
+                                        }
+                                        lv_terms_12_0=ruleVLSFofTerm
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSAtomicFunctionRule());
+                                                }
+                                                add(
+                                                        $current,
+                                                        "terms",
+                                                        lv_terms_12_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                        otherlv_13=')'
+                        {
+                                newLeafNode(otherlv_13, grammarAccess.getVLSAtomicFunctionAccess().getRightParenthesisKeyword_1_6());
+                        }
+                )
+        )
+;
+// Entry rule entryRuleVLSVariable
+entryRuleVLSVariable returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSVariableRule()); }
+        iv_ruleVLSVariable=ruleVLSVariable
+        { $current=$iv_ruleVLSVariable.current; }
+        EOF;
+// Rule VLSVariable
+ruleVLSVariable returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        lv_name_0_0=RULE_UPPER_WORD_ID
+                        {
+                                newLeafNode(lv_name_0_0, grammarAccess.getVLSVariableAccess().getNameUPPER_WORD_IDTerminalRuleCall_0());
+                        }
+                        {
+                                if ($current==null) {
+                                        $current = createModelElement(grammarAccess.getVLSVariableRule());
+                                }
+                                setWithLastConsumed(
+                                        $current,
+                                        "name",
+                                        lv_name_0_0,
+                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.UPPER_WORD_ID");
+                        }
+                )
+        )
+;
+// Entry rule entryRuleVLSFofTerm
+entryRuleVLSFofTerm returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSFofTermRule()); }
+        iv_ruleVLSFofTerm=ruleVLSFofTerm
+        { $current=$iv_ruleVLSFofTerm.current; }
+        EOF;
+// Rule VLSFofTerm
+ruleVLSFofTerm returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                {
+                        newCompositeNode(grammarAccess.getVLSFofTermAccess().getVLSVariableParserRuleCall_0());
+                }
+                this_VLSVariable_0=ruleVLSVariable
+                {
+                        $current = $this_VLSVariable_0.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSFofTermAccess().getVLSFunctionFofParserRuleCall_1());
+                }
+                this_VLSFunctionFof_1=ruleVLSFunctionFof
+                {
+                        $current = $this_VLSFunctionFof_1.current;
+                        afterParserOrEnumRuleCall();
+                }
+                    |
+                {
+                        newCompositeNode(grammarAccess.getVLSFofTermAccess().getVLSDefinedTermParserRuleCall_2());
+                }
+                this_VLSDefinedTerm_2=ruleVLSDefinedTerm
+                {
+                        $current = $this_VLSDefinedTerm_2.current;
+                        afterParserOrEnumRuleCall();
+                }
+        )
+;
+// Entry rule entryRuleVLSFunctionFof
+entryRuleVLSFunctionFof returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSFunctionFofRule()); }
+        iv_ruleVLSFunctionFof=ruleVLSFunctionFof
+        { $current=$iv_ruleVLSFunctionFof.current; }
+        EOF;
+// Rule VLSFunctionFof
+ruleVLSFunctionFof returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        (
+                                (
+                                        lv_functor_0_1=RULE_LOWER_WORD_ID
+                                        {
+                                                newLeafNode(lv_functor_0_1, grammarAccess.getVLSFunctionFofAccess().getFunctorLOWER_WORD_IDTerminalRuleCall_0_0_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSFunctionFofRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "functor",
+                                                        lv_functor_0_1,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.LOWER_WORD_ID");
+                                        }
+                                            |
+                                        lv_functor_0_2=RULE_SINGLE_QUOTE
+                                        {
+                                                newLeafNode(lv_functor_0_2, grammarAccess.getVLSFunctionFofAccess().getFunctorSINGLE_QUOTETerminalRuleCall_0_0_1());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSFunctionFofRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "functor",
+                                                        lv_functor_0_2,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_QUOTE");
+                                        }
+                                            |
+                                        lv_functor_0_3=RULE_DOLLAR_ID
+                                        {
+                                                newLeafNode(lv_functor_0_3, grammarAccess.getVLSFunctionFofAccess().getFunctorDOLLAR_IDTerminalRuleCall_0_0_2());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSFunctionFofRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "functor",
+                                                        lv_functor_0_3,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOLLAR_ID");
+                                        }
+                                            |
+                                        lv_functor_0_4=RULE_DOUBLE_DOLLAR_ID
+                                        {
+                                                newLeafNode(lv_functor_0_4, grammarAccess.getVLSFunctionFofAccess().getFunctorDOUBLE_DOLLAR_IDTerminalRuleCall_0_0_3());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSFunctionFofRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "functor",
+                                                        lv_functor_0_4,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOUBLE_DOLLAR_ID");
+                                        }
+                                )
+                        )
+                )
+                (
+                        otherlv_1='('
+                        {
+                                newLeafNode(otherlv_1, grammarAccess.getVLSFunctionFofAccess().getLeftParenthesisKeyword_1_0());
+                        }
+                        (
+                                (
+                                        {
+                                                newCompositeNode(grammarAccess.getVLSFunctionFofAccess().getTermsVLSFofTermParserRuleCall_1_1_0());
+                                        }
+                                        lv_terms_2_0=ruleVLSFofTerm
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElementForParent(grammarAccess.getVLSFunctionFofRule());
+                                                }
+                                                add(
+                                                        $current,
+                                                        "terms",
+                                                        lv_terms_2_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
+                                                afterParserOrEnumRuleCall();
+                                        }
+                                )
+                        )
+                        (
+                                otherlv_3=','
+                                {
+                                        newLeafNode(otherlv_3, grammarAccess.getVLSFunctionFofAccess().getCommaKeyword_1_2_0());
+                                }
+                                (
+                                        (
+                                                {
+                                                        newCompositeNode(grammarAccess.getVLSFunctionFofAccess().getTermsVLSFofTermParserRuleCall_1_2_1_0());
+                                                }
+                                                lv_terms_4_0=ruleVLSFofTerm
+                                                {
+                                                        if ($current==null) {
+                                                                $current = createModelElementForParent(grammarAccess.getVLSFunctionFofRule());
+                                                        }
+                                                        add(
+                                                                $current,
+                                                                "terms",
+                                                                lv_terms_4_0,
+                                                                "ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
+                                                        afterParserOrEnumRuleCall();
+                                                }
+                                        )
+                                )
+                        )*
+                        otherlv_5=')'
+                        {
+                                newLeafNode(otherlv_5, grammarAccess.getVLSFunctionFofAccess().getRightParenthesisKeyword_1_3());
+                        }
+                )?
+        )
+;
+// Entry rule entryRuleVLSDefinedTerm
+entryRuleVLSDefinedTerm returns [EObject current=null]:
+        { newCompositeNode(grammarAccess.getVLSDefinedTermRule()); }
+        iv_ruleVLSDefinedTerm=ruleVLSDefinedTerm
+        { $current=$iv_ruleVLSDefinedTerm.current; }
+        EOF;
+// Rule VLSDefinedTerm
+ruleVLSDefinedTerm returns [EObject current=null]
+@init {
+        enterRule();
+}
+@after {
+        leaveRule();
+}:
+        (
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSDefinedTermAccess().getVLSIntAction_0_0(),
+                                                $current);
+                                }
+                        )
+                        (
+                                (
+                                        lv_value_1_0=RULE_SIGNED_LITERAL
+                                        {
+                                                newLeafNode(lv_value_1_0, grammarAccess.getVLSDefinedTermAccess().getValueSIGNED_LITERALTerminalRuleCall_0_1_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSDefinedTermRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "value",
+                                                        lv_value_1_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_LITERAL");
+                                        }
+                                )
+                        )
+                )
+                    |
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSDefinedTermAccess().getVLSRealAction_1_0(),
+                                                $current);
+                                }
+                        )
+                        (
+                                (
+                                        lv_value_3_0=RULE_SIGNED_REAL_ID
+                                        {
+                                                newLeafNode(lv_value_3_0, grammarAccess.getVLSDefinedTermAccess().getValueSIGNED_REAL_IDTerminalRuleCall_1_1_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSDefinedTermRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "value",
+                                                        lv_value_3_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_REAL_ID");
+                                        }
+                                )
+                        )
+                )
+                    |
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSDefinedTermAccess().getVLSRationalAction_2_0(),
+                                                $current);
+                                }
+                        )
+                        (
+                                (
+                                        lv_value_5_0=RULE_SIGNED_RAT_ID
+                                        {
+                                                newLeafNode(lv_value_5_0, grammarAccess.getVLSDefinedTermAccess().getValueSIGNED_RAT_IDTerminalRuleCall_2_1_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSDefinedTermRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "value",
+                                                        lv_value_5_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.SIGNED_RAT_ID");
+                                        }
+                                )
+                        )
+                )
+                    |
+                (
+                        (
+                                {
+                                        $current = forceCreateModelElement(
+                                                grammarAccess.getVLSDefinedTermAccess().getVLSDoubleQuoteAction_3_0(),
+                                                $current);
+                                }
+                        )
+                        (
+                                (
+                                        lv_value_7_0=RULE_DOUBLE_QUOTE
+                                        {
+                                                newLeafNode(lv_value_7_0, grammarAccess.getVLSDefinedTermAccess().getValueDOUBLE_QUOTETerminalRuleCall_3_1_0());
+                                        }
+                                        {
+                                                if ($current==null) {
+                                                        $current = createModelElement(grammarAccess.getVLSDefinedTermRule());
+                                                }
+                                                setWithLastConsumed(
+                                                        $current,
+                                                        "value",
+                                                        lv_value_7_0,
+                                                        "ca.mcgill.ecse.dslreasoner.VampireLanguage.DOUBLE_QUOTE");
+                                        }
+                                )
+                        )
+                )
+        )
+;
+fragment RULE_ALPHA_NUMERIC : ('a'..'z'|'A'..'Z'|'0'..'9'|'_');
+RULE_UPPER_WORD_ID : 'A'..'Z' RULE_ALPHA_NUMERIC*;
+RULE_LOWER_WORD_ID : 'a'..'z' RULE_ALPHA_NUMERIC*;
+RULE_DOUBLE_QUOTE : '"' ('\\' ('"'|'\\')|~(('\\'|'"')))* '"';
+RULE_SINGLE_QUOTE : '\'' ('\\' ('\''|'\\')|~(('\\'|'\'')))+ '\'';
+fragment RULE_SIGN : ('+'|'-');
+RULE_DOLLAR_ID : '$' RULE_LOWER_WORD_ID;
+RULE_DOUBLE_DOLLAR_ID : '$$' RULE_LOWER_WORD_ID;
+RULE_LITERAL : ('0'|'1'..'9' RULE_INT?);
+RULE_SIGNED_LITERAL : RULE_SIGN* RULE_LITERAL;
+fragment RULE_UNSIGNED_REAL_FRAC_ID : RULE_LITERAL '.' RULE_INT;
+fragment RULE_UNSIGNED_REAL_EXP_ID : (RULE_LITERAL|RULE_UNSIGNED_REAL_FRAC_ID) 'Ee' RULE_SIGN* RULE_INT;
+RULE_SIGNED_REAL_ID : RULE_SIGN* (RULE_UNSIGNED_REAL_FRAC_ID|RULE_UNSIGNED_REAL_EXP_ID);
+fragment RULE_UNSIGNED_RAT_ID : RULE_LITERAL '/' '1'..'9' RULE_INT?;
+RULE_SIGNED_RAT_ID : RULE_SIGN* RULE_UNSIGNED_RAT_ID;
+fragment RULE_ANY_OTHER : '%' ~(('\n'|'\r'))* '\r';
+RULE_SINGLE_COMMENT : RULE_ANY_OTHER;
+RULE_ID : '^'? ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'0'..'9')*;
+fragment RULE_INT : ('0'..'9')+;
+RULE_STRING : ('"' ('\\' .|~(('\\'|'"')))* '"'|'\'' ('\\' .|~(('\\'|'\'')))* '\'');
+RULE_ML_COMMENT : '/*' ( options {greedy=false;} : . )*'*/';
+RULE_SL_COMMENT : '//' ~(('\n'|'\r'))* ('\r'? '\n')?;
+RULE_WS : (' '|'\t'|'\r'|'\n')+;