/*
 * generated by Xtext 2.14.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().getCommentsVLSCommentParserRuleCall_0_0());
				}
				lv_comments_0_0=ruleVLSComment
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVampireModelRule());
					}
					add(
						$current,
						"comments",
						lv_comments_0_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSComment");
					afterParserOrEnumRuleCall();
				}
			)
		)
		    |
		(
			(
				{
					newCompositeNode(grammarAccess.getVampireModelAccess().getConfirmationsVLSConfirmationsParserRuleCall_1_0());
				}
				lv_confirmations_1_0=ruleVLSConfirmations
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVampireModelRule());
					}
					add(
						$current,
						"confirmations",
						lv_confirmations_1_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSConfirmations");
					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();
				}
			)
		)
		    |
		(
			(
				{
					newCompositeNode(grammarAccess.getVampireModelAccess().getTfformulasVLSTffFormulaParserRuleCall_3_0());
				}
				lv_tfformulas_3_0=ruleVLSTffFormula
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVampireModelRule());
					}
					add(
						$current,
						"tfformulas",
						lv_tfformulas_3_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffFormula");
					afterParserOrEnumRuleCall();
				}
			)
		)
	)*
;

// 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 entryRuleVLSConfirmations
entryRuleVLSConfirmations returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSConfirmationsRule()); }
	iv_ruleVLSConfirmations=ruleVLSConfirmations
	{ $current=$iv_ruleVLSConfirmations.current; }
	EOF;

// Rule VLSConfirmations
ruleVLSConfirmations returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			(
				{
					$current = forceCreateModelElement(
						grammarAccess.getVLSConfirmationsAccess().getVLSSatisfiableAction_0_0(),
						$current);
				}
			)
			otherlv_1='Satisfiable!'
			{
				newLeafNode(otherlv_1, grammarAccess.getVLSConfirmationsAccess().getSatisfiableKeyword_0_1());
			}
		)
		    |
		(
			(
				{
					$current = forceCreateModelElement(
						grammarAccess.getVLSConfirmationsAccess().getVLSWarningAction_1_0(),
						$current);
				}
			)
			otherlv_3='WARNING!'
			{
				newLeafNode(otherlv_3, grammarAccess.getVLSConfirmationsAccess().getWARNINGKeyword_1_1());
			}
			otherlv_4='Could'
			{
				newLeafNode(otherlv_4, grammarAccess.getVLSConfirmationsAccess().getCouldKeyword_1_2());
			}
			otherlv_5='not'
			{
				newLeafNode(otherlv_5, grammarAccess.getVLSConfirmationsAccess().getNotKeyword_1_3());
			}
			otherlv_6='set'
			{
				newLeafNode(otherlv_6, grammarAccess.getVLSConfirmationsAccess().getSetKeyword_1_4());
			}
			otherlv_7='resource'
			{
				newLeafNode(otherlv_7, grammarAccess.getVLSConfirmationsAccess().getResourceKeyword_1_5());
			}
			otherlv_8='limit:'
			{
				newLeafNode(otherlv_8, grammarAccess.getVLSConfirmationsAccess().getLimitKeyword_1_6());
			}
			otherlv_9='Virtual'
			{
				newLeafNode(otherlv_9, grammarAccess.getVLSConfirmationsAccess().getVirtualKeyword_1_7());
			}
			otherlv_10='memory.'
			{
				newLeafNode(otherlv_10, grammarAccess.getVLSConfirmationsAccess().getMemoryKeyword_1_8());
			}
		)
		    |
		(
			(
				{
					$current = forceCreateModelElement(
						grammarAccess.getVLSConfirmationsAccess().getVLSTryingAction_2_0(),
						$current);
				}
			)
			otherlv_12='TRYING'
			{
				newLeafNode(otherlv_12, grammarAccess.getVLSConfirmationsAccess().getTRYINGKeyword_2_1());
			}
			otherlv_13='['
			{
				newLeafNode(otherlv_13, grammarAccess.getVLSConfirmationsAccess().getLeftSquareBracketKeyword_2_2());
			}
			(
				(
					lv_name_14_0=RULE_LITERAL
					{
						newLeafNode(lv_name_14_0, grammarAccess.getVLSConfirmationsAccess().getNameLITERALTerminalRuleCall_2_3_0());
					}
					{
						if ($current==null) {
							$current = createModelElement(grammarAccess.getVLSConfirmationsRule());
						}
						setWithLastConsumed(
							$current,
							"name",
							lv_name_14_0,
							"ca.mcgill.ecse.dslreasoner.VampireLanguage.LITERAL");
					}
				)
			)
			otherlv_15=']'
			{
				newLeafNode(otherlv_15, grammarAccess.getVLSConfirmationsAccess().getRightSquareBracketKeyword_2_4());
			}
		)
		    |
		(
			(
				{
					$current = forceCreateModelElement(
						grammarAccess.getVLSConfirmationsAccess().getVLSFiniteModelAction_3_0(),
						$current);
				}
			)
			otherlv_17='Finite'
			{
				newLeafNode(otherlv_17, grammarAccess.getVLSConfirmationsAccess().getFiniteKeyword_3_1());
			}
			otherlv_18='Model'
			{
				newLeafNode(otherlv_18, grammarAccess.getVLSConfirmationsAccess().getModelKeyword_3_2());
			}
			otherlv_19='Found!'
			{
				newLeafNode(otherlv_19, grammarAccess.getVLSConfirmationsAccess().getFoundKeyword_3_3());
			}
		)
	)
;

// 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 entryRuleVLSTffFormula
entryRuleVLSTffFormula returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSTffFormulaRule()); }
	iv_ruleVLSTffFormula=ruleVLSTffFormula
	{ $current=$iv_ruleVLSTffFormula.current; }
	EOF;

// Rule VLSTffFormula
ruleVLSTffFormula returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		otherlv_0='tff'
		{
			newLeafNode(otherlv_0, grammarAccess.getVLSTffFormulaAccess().getTffKeyword_0());
		}
		otherlv_1='('
		{
			newLeafNode(otherlv_1, grammarAccess.getVLSTffFormulaAccess().getLeftParenthesisKeyword_1());
		}
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getNameVLSTffNameParserRuleCall_2_0());
				}
				lv_name_2_0=ruleVLSTffName
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule());
					}
					set(
						$current,
						"name",
						lv_name_2_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffName");
					afterParserOrEnumRuleCall();
				}
			)
		)
		otherlv_3=','
		{
			newLeafNode(otherlv_3, grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_3());
		}
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getTffRoleVLSRoleParserRuleCall_4_0());
				}
				lv_tffRole_4_0=ruleVLSRole
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule());
					}
					set(
						$current,
						"tffRole",
						lv_tffRole_4_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSRole");
					afterParserOrEnumRuleCall();
				}
			)
		)
		otherlv_5=','
		{
			newLeafNode(otherlv_5, grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_5());
		}
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getFofFormulaVLSTffTermParserRuleCall_6_0());
				}
				lv_fofFormula_6_0=ruleVLSTffTerm
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule());
					}
					set(
						$current,
						"fofFormula",
						lv_fofFormula_6_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTffTerm");
					afterParserOrEnumRuleCall();
				}
			)
		)
		(
			otherlv_7=','
			{
				newLeafNode(otherlv_7, grammarAccess.getVLSTffFormulaAccess().getCommaKeyword_7_0());
			}
			(
				(
					{
						newCompositeNode(grammarAccess.getVLSTffFormulaAccess().getAnnotationsVLSAnnotationParserRuleCall_7_1_0());
					}
					lv_annotations_8_0=ruleVLSAnnotation
					{
						if ($current==null) {
							$current = createModelElementForParent(grammarAccess.getVLSTffFormulaRule());
						}
						set(
							$current,
							"annotations",
							lv_annotations_8_0,
							"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAnnotation");
						afterParserOrEnumRuleCall();
					}
				)
			)
		)?
		otherlv_9=')'
		{
			newLeafNode(otherlv_9, grammarAccess.getVLSTffFormulaAccess().getRightParenthesisKeyword_8());
		}
		otherlv_10='.'
		{
			newLeafNode(otherlv_10, grammarAccess.getVLSTffFormulaAccess().getFullStopKeyword_9());
		}
	)
;

// Entry rule entryRuleVLSTffName
entryRuleVLSTffName returns [String current=null]:
	{ newCompositeNode(grammarAccess.getVLSTffNameRule()); }
	iv_ruleVLSTffName=ruleVLSTffName
	{ $current=$iv_ruleVLSTffName.current.getText(); }
	EOF;

// Rule VLSTffName
ruleVLSTffName returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		{
			newCompositeNode(grammarAccess.getVLSTffNameAccess().getVLSTffDeclPredParserRuleCall_0());
		}
		this_VLSTffDeclPred_0=ruleVLSTffDeclPred
		{
			$current.merge(this_VLSTffDeclPred_0);
		}
		{
			afterParserOrEnumRuleCall();
		}
		    |
		{
			newCompositeNode(grammarAccess.getVLSTffNameAccess().getVLSTffFiniteParserRuleCall_1());
		}
		this_VLSTffFinite_1=ruleVLSTffFinite
		{
			$current.merge(this_VLSTffFinite_1);
		}
		{
			afterParserOrEnumRuleCall();
		}
		    |
		{
			newCompositeNode(grammarAccess.getVLSTffNameAccess().getVLSTffDistinctParserRuleCall_2());
		}
		this_VLSTffDistinct_2=ruleVLSTffDistinct
		{
			$current.merge(this_VLSTffDistinct_2);
		}
		{
			afterParserOrEnumRuleCall();
		}
	)
;

// Entry rule entryRuleVLSTffDistinct
entryRuleVLSTffDistinct returns [String current=null]:
	{ newCompositeNode(grammarAccess.getVLSTffDistinctRule()); }
	iv_ruleVLSTffDistinct=ruleVLSTffDistinct
	{ $current=$iv_ruleVLSTffDistinct.current.getText(); }
	EOF;

// Rule VLSTffDistinct
ruleVLSTffDistinct returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	kw='distinct_domain'
	{
		$current.merge(kw);
		newLeafNode(kw, grammarAccess.getVLSTffDistinctAccess().getDistinct_domainKeyword());
	}
;

// Entry rule entryRuleVLSTffFinite
entryRuleVLSTffFinite returns [String current=null]:
	{ newCompositeNode(grammarAccess.getVLSTffFiniteRule()); }
	iv_ruleVLSTffFinite=ruleVLSTffFinite
	{ $current=$iv_ruleVLSTffFinite.current.getText(); }
	EOF;

// Rule VLSTffFinite
ruleVLSTffFinite returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	kw='finite_domain'
	{
		$current.merge(kw);
		newLeafNode(kw, grammarAccess.getVLSTffFiniteAccess().getFinite_domainKeyword());
	}
;

// Entry rule entryRuleVLSTffDeclPred
entryRuleVLSTffDeclPred returns [String current=null]:
	{ newCompositeNode(grammarAccess.getVLSTffDeclPredRule()); }
	iv_ruleVLSTffDeclPred=ruleVLSTffDeclPred
	{ $current=$iv_ruleVLSTffDeclPred.current.getText(); }
	EOF;

// Rule VLSTffDeclPred
ruleVLSTffDeclPred returns [AntlrDatatypeRuleToken current=new AntlrDatatypeRuleToken()]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			kw='declare_'
			{
				$current.merge(kw);
				newLeafNode(kw, grammarAccess.getVLSTffDeclPredAccess().getDeclare_Keyword_0_0());
			}
			this_DOLLAR_ID_1=RULE_DOLLAR_ID
			{
				$current.merge(this_DOLLAR_ID_1);
			}
			{
				newLeafNode(this_DOLLAR_ID_1, grammarAccess.getVLSTffDeclPredAccess().getDOLLAR_IDTerminalRuleCall_0_1());
			}
		)
		    |
		this_LOWER_WORD_ID_2=RULE_LOWER_WORD_ID
		{
			$current.merge(this_LOWER_WORD_ID_2);
		}
		{
			newLeafNode(this_LOWER_WORD_ID_2, grammarAccess.getVLSTffDeclPredAccess().getLOWER_WORD_IDTerminalRuleCall_1());
		}
	)
;

// 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();
}:
	(
		kw='axiom'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getAxiomKeyword_0());
		}
		    |
		kw='conjecture'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getConjectureKeyword_1());
		}
		    |
		kw='hypothesis'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getHypothesisKeyword_2());
		}
		    |
		kw='definition'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getDefinitionKeyword_3());
		}
		    |
		kw='assumption'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getAssumptionKeyword_4());
		}
		    |
		kw='lemma'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getLemmaKeyword_5());
		}
		    |
		kw='theorem'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getTheoremKeyword_6());
		}
		    |
		kw='corollary'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getCorollaryKeyword_7());
		}
		    |
		kw='negated_conjecture'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getNegated_conjectureKeyword_8());
		}
		    |
		kw='plain'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getPlainKeyword_9());
		}
		    |
		kw='type'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getTypeKeyword_10());
		}
		    |
		kw='fi_domain'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getFi_domainKeyword_11());
		}
		    |
		kw='fi_functors'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getFi_functorsKeyword_12());
		}
		    |
		kw='fi_predicates'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getFi_predicatesKeyword_13());
		}
		    |
		kw='unknown'
		{
			$current.merge(kw);
			newLeafNode(kw, grammarAccess.getVLSRoleAccess().getUnknownKeyword_14());
		}
	)
;

// 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 entryRuleVLSTffTerm
entryRuleVLSTffTerm returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSTffTermRule()); }
	iv_ruleVLSTffTerm=ruleVLSTffTerm
	{ $current=$iv_ruleVLSTffTerm.current; }
	EOF;

// Rule VLSTffTerm
ruleVLSTffTerm returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		{
			newCompositeNode(grammarAccess.getVLSTffTermAccess().getVLSTermParserRuleCall_0());
		}
		this_VLSTerm_0=ruleVLSTerm
		{
			$current = $this_VLSTerm_0.current;
			afterParserOrEnumRuleCall();
		}
		    |
		{
			newCompositeNode(grammarAccess.getVLSTffTermAccess().getVLSDeclarationParserRuleCall_1());
		}
		this_VLSDeclaration_1=ruleVLSDeclaration
		{
			$current = $this_VLSDeclaration_1.current;
			afterParserOrEnumRuleCall();
		}
		    |
		{
			newCompositeNode(grammarAccess.getVLSTffTermAccess().getVLSCommentTermParserRuleCall_2());
		}
		this_VLSCommentTerm_2=ruleVLSCommentTerm
		{
			$current = $this_VLSCommentTerm_2.current;
			afterParserOrEnumRuleCall();
		}
	)
;

// Entry rule entryRuleVLSCommentTerm
entryRuleVLSCommentTerm returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSCommentTermRule()); }
	iv_ruleVLSCommentTerm=ruleVLSCommentTerm
	{ $current=$iv_ruleVLSCommentTerm.current; }
	EOF;

// Rule VLSCommentTerm
ruleVLSCommentTerm returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			lv_comment_0_0=RULE_SINGLE_COMMENT
			{
				newLeafNode(lv_comment_0_0, grammarAccess.getVLSCommentTermAccess().getCommentSINGLE_COMMENTTerminalRuleCall_0());
			}
			{
				if ($current==null) {
					$current = createModelElement(grammarAccess.getVLSCommentTermRule());
				}
				setWithLastConsumed(
					$current,
					"comment",
					lv_comment_0_0,
					"ca.mcgill.ecse.dslreasoner.VampireLanguage.SINGLE_COMMENT");
			}
		)
	)
;

// Entry rule entryRuleVLSDeclaration
entryRuleVLSDeclaration returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSDeclarationRule()); }
	iv_ruleVLSDeclaration=ruleVLSDeclaration
	{ $current=$iv_ruleVLSDeclaration.current; }
	EOF;

// Rule VLSDeclaration
ruleVLSDeclaration returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		{
			newCompositeNode(grammarAccess.getVLSDeclarationAccess().getVLSVariableDeclarationParserRuleCall_0());
		}
		this_VLSVariableDeclaration_0=ruleVLSVariableDeclaration
		{
			$current = $this_VLSVariableDeclaration_0.current;
			afterParserOrEnumRuleCall();
		}
		    |
		{
			newCompositeNode(grammarAccess.getVLSDeclarationAccess().getVLSOtherDeclarationParserRuleCall_1());
		}
		this_VLSOtherDeclaration_1=ruleVLSOtherDeclaration
		{
			$current = $this_VLSOtherDeclaration_1.current;
			afterParserOrEnumRuleCall();
		}
	)
;

// Entry rule entryRuleVLSOtherDeclaration
entryRuleVLSOtherDeclaration returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSOtherDeclarationRule()); }
	iv_ruleVLSOtherDeclaration=ruleVLSOtherDeclaration
	{ $current=$iv_ruleVLSOtherDeclaration.current; }
	EOF;

// Rule VLSOtherDeclaration
ruleVLSOtherDeclaration returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSOtherDeclarationAccess().getNameVLSAtomicConstantParserRuleCall_0_0());
				}
				lv_name_0_0=ruleVLSAtomicConstant
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSOtherDeclarationRule());
					}
					set(
						$current,
						"name",
						lv_name_0_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomicConstant");
					afterParserOrEnumRuleCall();
				}
			)
		)
		otherlv_1=':'
		{
			newLeafNode(otherlv_1, grammarAccess.getVLSOtherDeclarationAccess().getColonKeyword_1());
		}
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSOtherDeclarationAccess().getTypeVLSTypeDefParserRuleCall_2_0());
				}
				lv_type_2_0=ruleVLSTypeDef
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSOtherDeclarationRule());
					}
					set(
						$current,
						"type",
						lv_type_2_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTypeDef");
					afterParserOrEnumRuleCall();
				}
			)
		)
	)
;

// Entry rule entryRuleVLSVariableDeclaration
entryRuleVLSVariableDeclaration returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSVariableDeclarationRule()); }
	iv_ruleVLSVariableDeclaration=ruleVLSVariableDeclaration
	{ $current=$iv_ruleVLSVariableDeclaration.current; }
	EOF;

// Rule VLSVariableDeclaration
ruleVLSVariableDeclaration returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSVariableDeclarationAccess().getNameVLSVariableParserRuleCall_0_0());
				}
				lv_name_0_0=ruleVLSVariable
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSVariableDeclarationRule());
					}
					set(
						$current,
						"name",
						lv_name_0_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
					afterParserOrEnumRuleCall();
				}
			)
		)
		otherlv_1=':'
		{
			newLeafNode(otherlv_1, grammarAccess.getVLSVariableDeclarationAccess().getColonKeyword_1());
		}
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSVariableDeclarationAccess().getTypeVLSTypeDefParserRuleCall_2_0());
				}
				lv_type_2_0=ruleVLSTypeDef
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSVariableDeclarationRule());
					}
					set(
						$current,
						"type",
						lv_type_2_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSTypeDef");
					afterParserOrEnumRuleCall();
				}
			)
		)
	)
;

// Entry rule entryRuleVLSTypeDef
entryRuleVLSTypeDef returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSTypeDefRule()); }
	iv_ruleVLSTypeDef=ruleVLSTypeDef
	{ $current=$iv_ruleVLSTypeDef.current; }
	EOF;

// Rule VLSTypeDef
ruleVLSTypeDef returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSTypeDefAccess().getTypeSigVLSUnitaryTermParserRuleCall_0_0());
				}
				lv_typeSig_0_0=ruleVLSUnitaryTerm
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSTypeDefRule());
					}
					set(
						$current,
						"typeSig",
						lv_typeSig_0_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSUnitaryTerm");
					afterParserOrEnumRuleCall();
				}
			)
		)
		(
			otherlv_1='>'
			{
				newLeafNode(otherlv_1, grammarAccess.getVLSTypeDefAccess().getGreaterThanSignKeyword_1_0());
			}
			(
				(
					{
						newCompositeNode(grammarAccess.getVLSTypeDefAccess().getMapsToVLSAtomicConstantParserRuleCall_1_1_0());
					}
					lv_mapsTo_2_0=ruleVLSAtomicConstant
					{
						if ($current==null) {
							$current = createModelElementForParent(grammarAccess.getVLSTypeDefRule());
						}
						set(
							$current,
							"mapsTo",
							lv_mapsTo_2_0,
							"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomicConstant");
						afterParserOrEnumRuleCall();
					}
				)
			)
		)?
	)
;

// Entry rule entryRuleVLSUnitaryTerm
entryRuleVLSUnitaryTerm returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSUnitaryTermRule()); }
	iv_ruleVLSUnitaryTerm=ruleVLSUnitaryTerm
	{ $current=$iv_ruleVLSUnitaryTerm.current; }
	EOF;

// Rule VLSUnitaryTerm
ruleVLSUnitaryTerm returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			(
				{
					newCompositeNode(grammarAccess.getVLSUnitaryTermAccess().getInitTypeVLSAtomicParserRuleCall_0_0());
				}
				lv_initType_0_0=ruleVLSAtomic
				{
					if ($current==null) {
						$current = createModelElementForParent(grammarAccess.getVLSUnitaryTermRule());
					}
					set(
						$current,
						"initType",
						lv_initType_0_0,
						"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomic");
					afterParserOrEnumRuleCall();
				}
			)
		)
		(
			otherlv_1='*'
			{
				newLeafNode(otherlv_1, grammarAccess.getVLSUnitaryTermAccess().getAsteriskKeyword_1_0());
			}
			(
				(
					{
						newCompositeNode(grammarAccess.getVLSUnitaryTermAccess().getNextTypeVLSAtomicConstantParserRuleCall_1_1_0());
					}
					lv_nextType_2_0=ruleVLSAtomicConstant
					{
						if ($current==null) {
							$current = createModelElementForParent(grammarAccess.getVLSUnitaryTermRule());
						}
						set(
							$current,
							"nextType",
							lv_nextType_2_0,
							"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSAtomicConstant");
						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_0());
						}
						lv_variables_3_1=ruleVLSVariable
						{
							if ($current==null) {
								$current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule());
							}
							add(
								$current,
								"variables",
								lv_variables_3_1,
								"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
							afterParserOrEnumRuleCall();
						}
						    |
						{
							newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_2_0_1());
						}
						lv_variables_3_2=ruleVLSVariableDeclaration
						{
							if ($current==null) {
								$current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule());
							}
							add(
								$current,
								"variables",
								lv_variables_3_2,
								"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration");
							afterParserOrEnumRuleCall();
						}
					)
				)
			)
			(
				otherlv_4=','
				{
					newLeafNode(otherlv_4, grammarAccess.getVLSUniversalQuantifierAccess().getCommaKeyword_1_3_0());
				}
				(
					(
						(
							{
								newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0_0());
							}
							lv_variables_5_1=ruleVLSVariable
							{
								if ($current==null) {
									$current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule());
								}
								add(
									$current,
									"variables",
									lv_variables_5_1,
									"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
								afterParserOrEnumRuleCall();
							}
							    |
							{
								newCompositeNode(grammarAccess.getVLSUniversalQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_3_1_0_1());
							}
							lv_variables_5_2=ruleVLSVariableDeclaration
							{
								if ($current==null) {
									$current = createModelElementForParent(grammarAccess.getVLSUniversalQuantifierRule());
								}
								add(
									$current,
									"variables",
									lv_variables_5_2,
									"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration");
								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_0());
						}
						lv_variables_3_1=ruleVLSVariable
						{
							if ($current==null) {
								$current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule());
							}
							add(
								$current,
								"variables",
								lv_variables_3_1,
								"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
							afterParserOrEnumRuleCall();
						}
						    |
						{
							newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_2_0_1());
						}
						lv_variables_3_2=ruleVLSVariableDeclaration
						{
							if ($current==null) {
								$current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule());
							}
							add(
								$current,
								"variables",
								lv_variables_3_2,
								"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration");
							afterParserOrEnumRuleCall();
						}
					)
				)
			)
			(
				otherlv_4=','
				{
					newLeafNode(otherlv_4, grammarAccess.getVLSExistentialQuantifierAccess().getCommaKeyword_1_3_0());
				}
				(
					(
						(
							{
								newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableParserRuleCall_1_3_1_0_0());
							}
							lv_variables_5_1=ruleVLSVariable
							{
								if ($current==null) {
									$current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule());
								}
								add(
									$current,
									"variables",
									lv_variables_5_1,
									"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariable");
								afterParserOrEnumRuleCall();
							}
							    |
							{
								newCompositeNode(grammarAccess.getVLSExistentialQuantifierAccess().getVariablesVLSVariableDeclarationParserRuleCall_1_3_1_0_1());
							}
							lv_variables_5_2=ruleVLSVariableDeclaration
							{
								if ($current==null) {
									$current = createModelElementForParent(grammarAccess.getVLSExistentialQuantifierRule());
								}
								add(
									$current,
									"variables",
									lv_variables_5_2,
									"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSVariableDeclaration");
								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().getVLSFunctionAsTermParserRuleCall_1());
		}
		this_VLSFunctionAsTerm_1=ruleVLSFunctionAsTerm
		{
			$current = $this_VLSFunctionAsTerm_1.current;
			afterParserOrEnumRuleCall();
		}
		    |
		{
			newCompositeNode(grammarAccess.getVLSFofTermAccess().getVLSDefinedTermParserRuleCall_2());
		}
		this_VLSDefinedTerm_2=ruleVLSDefinedTerm
		{
			$current = $this_VLSDefinedTerm_2.current;
			afterParserOrEnumRuleCall();
		}
	)
;

// Entry rule entryRuleVLSFunctionAsTerm
entryRuleVLSFunctionAsTerm returns [EObject current=null]:
	{ newCompositeNode(grammarAccess.getVLSFunctionAsTermRule()); }
	iv_ruleVLSFunctionAsTerm=ruleVLSFunctionAsTerm
	{ $current=$iv_ruleVLSFunctionAsTerm.current; }
	EOF;

// Rule VLSFunctionAsTerm
ruleVLSFunctionAsTerm returns [EObject current=null]
@init {
	enterRule();
}
@after {
	leaveRule();
}:
	(
		(
			(
				(
					lv_functor_0_1=RULE_LOWER_WORD_ID
					{
						newLeafNode(lv_functor_0_1, grammarAccess.getVLSFunctionAsTermAccess().getFunctorLOWER_WORD_IDTerminalRuleCall_0_0_0());
					}
					{
						if ($current==null) {
							$current = createModelElement(grammarAccess.getVLSFunctionAsTermRule());
						}
						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.getVLSFunctionAsTermAccess().getFunctorSINGLE_QUOTETerminalRuleCall_0_0_1());
					}
					{
						if ($current==null) {
							$current = createModelElement(grammarAccess.getVLSFunctionAsTermRule());
						}
						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.getVLSFunctionAsTermAccess().getFunctorDOLLAR_IDTerminalRuleCall_0_0_2());
					}
					{
						if ($current==null) {
							$current = createModelElement(grammarAccess.getVLSFunctionAsTermRule());
						}
						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.getVLSFunctionAsTermAccess().getFunctorDOUBLE_DOLLAR_IDTerminalRuleCall_0_0_3());
					}
					{
						if ($current==null) {
							$current = createModelElement(grammarAccess.getVLSFunctionAsTermRule());
						}
						setWithLastConsumed(
							$current,
							"functor",
							lv_functor_0_4,
							"ca.mcgill.ecse.dslreasoner.VampireLanguage.DOUBLE_DOLLAR_ID");
					}
				)
			)
		)
		(
			otherlv_1='('
			{
				newLeafNode(otherlv_1, grammarAccess.getVLSFunctionAsTermAccess().getLeftParenthesisKeyword_1_0());
			}
			(
				(
					{
						newCompositeNode(grammarAccess.getVLSFunctionAsTermAccess().getTermsVLSFofTermParserRuleCall_1_1_0());
					}
					lv_terms_2_0=ruleVLSFofTerm
					{
						if ($current==null) {
							$current = createModelElementForParent(grammarAccess.getVLSFunctionAsTermRule());
						}
						add(
							$current,
							"terms",
							lv_terms_2_0,
							"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
						afterParserOrEnumRuleCall();
					}
				)
			)
			(
				otherlv_3=','
				{
					newLeafNode(otherlv_3, grammarAccess.getVLSFunctionAsTermAccess().getCommaKeyword_1_2_0());
				}
				(
					(
						{
							newCompositeNode(grammarAccess.getVLSFunctionAsTermAccess().getTermsVLSFofTermParserRuleCall_1_2_1_0());
						}
						lv_terms_4_0=ruleVLSFofTerm
						{
							if ($current==null) {
								$current = createModelElementForParent(grammarAccess.getVLSFunctionAsTermRule());
							}
							add(
								$current,
								"terms",
								lv_terms_4_0,
								"ca.mcgill.ecse.dslreasoner.VampireLanguage.VLSFofTerm");
							afterParserOrEnumRuleCall();
						}
					)
				)
			)*
			otherlv_5=')'
			{
				newLeafNode(otherlv_5, grammarAccess.getVLSFunctionAsTermAccess().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().getVLSDoubleQuoteAction_1_0(),
						$current);
				}
			)
			(
				(
					lv_value_3_0=RULE_DOUBLE_QUOTE
					{
						newLeafNode(lv_value_3_0, grammarAccess.getVLSDefinedTermAccess().getValueDOUBLE_QUOTETerminalRuleCall_1_1_0());
					}
					{
						if ($current==null) {
							$current = createModelElement(grammarAccess.getVLSDefinedTermRule());
						}
						setWithLastConsumed(
							$current,
							"value",
							lv_value_3_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;

RULE_SINGLE_COMMENT : '%' ~(('\n'|'\r'))* ('\r'? '\n')?;

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

RULE_ANY_OTHER : .;