Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/parser/tptp/TptpLexer.c	Lines:	1406	1828	76.9 %
Date:	2021-05-21	Branches:	494	887	55.7 %

/** \file
 *  This C source file was generated by $ANTLR version 3.4
 *
 *     -  From the grammar source file : /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g
 *     -                            On : 2021-05-21 01:05:10
 *     -                 for the lexer : TptpLexerLexer
 *
 * Editing it, at least manually, is not wise.
 *
 * C language generator and runtime by Jim Idle, jimi|hereisanat|idle|dotgoeshere|ws.
 *
 *
*/
// [The "BSD license"]
// Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC
// http://www.temporal-wave.com
// http://www.linkedin.com/in/jimidle
//
// All rights reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions
// are met:
// 1. Redistributions of source code must retain the above copyright
//    notice, this list of conditions and the following disclaimer.
// 2. Redistributions in binary form must reproduce the above copyright
//    notice, this list of conditions and the following disclaimer in the
//    documentation and/or other materials provided with the distribution.
// 3. The name of the author may not be used to endorse or promote products
//    derived from this software without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
// IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
// OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
// IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
// INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
// NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

/* -----------------------------------------
 * Include the ANTLR3 generated header file.
 */
#include    "TptpLexer.h"


#include "parser/tptp/tptp.h"
#include "parser/antlr_input.h"

using namespace cvc5;
using namespace cvc5::parser;

/* These need to be macros so they can refer to the PARSER macro, which will be defined
 * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
#undef PARSER_STATE
#define PARSER_STATE ((Tptp*)LEXER->super)
#undef SOLVER
#define SOLVER PARSER_STATE->getSolver()
#undef MK_TERM
#define MK_TERM SOLVER->mkTerm
#undef MK_TERM
#define MK_TERM SOLVER->mkTerm
#define UNSUPPORTED PARSER_STATE->unimplementedFeature


/* ----------------------------------------- */


/** String literals used by TptpLexer that we must do things like MATCHS() with.
 *  C will normally just lay down 8 bit characters, and you can use L"xxx" to
 *  get wchar_t, but wchar_t is 16 bits on Windows, which is not UTF32 and so
 *  we perform this little trick of defining the literals as arrays of UINT32
 *  and passing in the address of these.
 */
static ANTLR3_UCHAR	lit_1[]  = { 0x24, 0x63, 0x65, 0x69, 0x6C, 0x69, 0x6E, 0x67,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_2[]  = { 0x24, 0x64, 0x69, 0x66, 0x66, 0x65, 0x72, 0x65, 0x6E, 0x63, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_3[]  = { 0x24, 0x64, 0x69, 0x73, 0x74, 0x69, 0x6E, 0x63, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_4[]  = { 0x24, 0x66, 0x6C, 0x6F, 0x6F, 0x72,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_5[]  = { 0x24, 0x67, 0x72, 0x65, 0x61, 0x74, 0x65, 0x72,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_6[]  = { 0x24, 0x67, 0x72, 0x65, 0x61, 0x74, 0x65, 0x72, 0x65, 0x71,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_7[]  = { 0x24, 0x69, 0x73, 0x5F, 0x69, 0x6E, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_8[]  = { 0x24, 0x69, 0x73, 0x5F, 0x72, 0x61, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_9[]  = { 0x24, 0x69, 0x74, 0x65, 0x5F, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_10[]  = { 0x24, 0x69, 0x74, 0x65, 0x5F, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_11[]  = { 0x24, 0x6C, 0x65, 0x73, 0x73,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_12[]  = { 0x24, 0x6C, 0x65, 0x73, 0x73, 0x65, 0x71,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_13[]  = { 0x24, 0x6C, 0x65, 0x74, 0x5F, 0x66, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_14[]  = { 0x24, 0x6C, 0x65, 0x74, 0x5F, 0x66, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_15[]  = { 0x24, 0x6C, 0x65, 0x74, 0x5F, 0x74, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_16[]  = { 0x24, 0x6C, 0x65, 0x74, 0x5F, 0x74, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_17[]  = { 0x24, 0x70, 0x72, 0x6F, 0x64, 0x75, 0x63, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_18[]  = { 0x24, 0x71, 0x75, 0x6F, 0x74, 0x69, 0x65, 0x6E, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_19[]  = { 0x24, 0x71, 0x75, 0x6F, 0x74, 0x69, 0x65, 0x6E, 0x74, 0x5F, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_20[]  = { 0x24, 0x71, 0x75, 0x6F, 0x74, 0x69, 0x65, 0x6E, 0x74, 0x5F, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_21[]  = { 0x24, 0x71, 0x75, 0x6F, 0x74, 0x69, 0x65, 0x6E, 0x74, 0x5F, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_22[]  = { 0x24, 0x72, 0x65, 0x6D, 0x61, 0x69, 0x6E, 0x64, 0x65, 0x72, 0x5F, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_23[]  = { 0x24, 0x72, 0x65, 0x6D, 0x61, 0x69, 0x6E, 0x64, 0x65, 0x72, 0x5F, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_24[]  = { 0x24, 0x72, 0x65, 0x6D, 0x61, 0x69, 0x6E, 0x64, 0x65, 0x72, 0x5F, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_25[]  = { 0x24, 0x72, 0x6F, 0x75, 0x6E, 0x64,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_26[]  = { 0x24, 0x73, 0x75, 0x6D,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_27[]  = { 0x24, 0x74, 0x54, 0x79, 0x70, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_28[]  = { 0x24, 0x74, 0x6F, 0x5F, 0x69, 0x6E, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_29[]  = { 0x24, 0x74, 0x6F, 0x5F, 0x72, 0x61, 0x74,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_30[]  = { 0x24, 0x74, 0x6F, 0x5F, 0x72, 0x65, 0x61, 0x6C,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_31[]  = { 0x24, 0x74, 0x72, 0x75, 0x6E, 0x63, 0x61, 0x74, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_32[]  = { 0x24, 0x75, 0x6D, 0x69, 0x6E, 0x75, 0x73,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_33[]  = { 0x3E, 0x3E,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_34[]  = { 0x40, 0x2B,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_35[]  = { 0x40, 0x2D,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_36[]  = { 0x3C, 0x3D, 0x3E,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_37[]  = { 0x3D, 0x3E,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_38[]  = { 0x3C, 0x3D,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_39[]  = { 0x3C, 0x7E, 0x3E,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_40[]  = { 0x7E, 0x7C,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_41[]  = { 0x7E, 0x26,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_42[]  = { 0x21, 0x21,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_43[]  = { 0x3F, 0x3F,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_44[]  = { 0x24, 0x74, 0x72, 0x75, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_45[]  = { 0x24, 0x66, 0x61, 0x6C, 0x73, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_46[]  = { 0x21, 0x3D,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_47[]  = { 0x63, 0x6E, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_48[]  = { 0x66, 0x6F, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_49[]  = { 0x74, 0x68, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_50[]  = { 0x74, 0x66, 0x66,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_51[]  = { 0x74, 0x79, 0x70, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_52[]  = { 0x69, 0x6E, 0x63, 0x6C, 0x75, 0x64, 0x65,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_53[]  = { 0x5C, 0x22,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_54[]  = { 0x5C, 0x5C,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_55[]  = { 0x5C, 0x27,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_56[]  = { 0x2F, 0x2A,  ANTLR3_STRING_TERMINATOR};
static ANTLR3_UCHAR	lit_57[]  = { 0x2A, 0x2F,  ANTLR3_STRING_TERMINATOR};





/* MACROS that hide the C interface implementations from the
 * generated code, which makes it a little more understandable to the human eye.
 * I am very much against using C pre-processor macros for function calls and bits
 * of code as you cannot see what is happening when single stepping in debuggers
 * and so on. The exception (in my book at least) is for generated code, where you are
 * not maintaining it, but may wish to read and understand it. If you single step it, you know that input()
 * hides some indirect calls, but is always referring to the input stream. This is
 * probably more readable than ctx->input->istream->input(snarfle0->blarg) and allows me to rejig
 * the runtime interfaces without changing the generated code too often, without
 * confusing the reader of the generated output, who may not wish to know the gory
 * details of the interface inheritance.
 */

#define		CTX	ctx

/* Aids in accessing scopes for grammar programmers
 */
#undef	SCOPE_TYPE
#undef	SCOPE_STACK
#undef	SCOPE_TOP
#define	SCOPE_TYPE(scope)   pTptpLexer_##scope##_SCOPE
#define SCOPE_STACK(scope)  pTptpLexer_##scope##Stack
#define	SCOPE_TOP(scope)    ctx->pTptpLexer_##scope##Top
#define	SCOPE_SIZE(scope)		ctx->pTptpLexer_##scope##Stack_limit
#define SCOPE_INSTANCE(scope, i)	(ctx->SCOPE_STACK(scope)->get(ctx->SCOPE_STACK(scope),i))


/* Macros for accessing things in a lexer
 */
#undef	    LEXER
#undef	    RECOGNIZER
#undef	    RULEMEMO
#undef	    GETCHARINDEX
#undef	    GETLINE
#undef	    GETCHARPOSITIONINLINE
#undef	    EMIT
#undef	    EMITNEW
#undef	    MATCHC
#undef	    MATCHS
#undef	    MATCHRANGE
#undef	    LTOKEN
#undef	    HASFAILED
#undef	    FAILEDFLAG
#undef	    INPUT
#undef	    STRSTREAM
#undef	    LA
#undef	    HASEXCEPTION
#undef	    EXCEPTION
#undef	    CONSTRUCTEX
#undef	    CONSUME
#undef	    LRECOVER
#undef	    MARK
#undef	    REWIND
#undef	    REWINDLAST
#undef	    BACKTRACKING
#undef		MATCHANY
#undef		MEMOIZE
#undef		HAVEPARSEDRULE
#undef		GETTEXT
#undef		INDEX
#undef		SEEK
#undef		PUSHSTREAM
#undef		POPSTREAM
#undef		SETTEXT
#undef		SETTEXT8

#define	    LEXER					ctx->pLexer
#define	    RECOGNIZER			    LEXER->rec
#define		LEXSTATE				RECOGNIZER->state
#define		TOKSOURCE				LEXSTATE->tokSource
#define	    GETCHARINDEX()			LEXER->getCharIndex(LEXER)
#define	    GETLINE()				LEXER->getLine(LEXER)
#define	    GETTEXT()				LEXER->getText(LEXER)
#define	    GETCHARPOSITIONINLINE() LEXER->getCharPositionInLine(LEXER)
#define	    EMIT()					LEXSTATE->type = _type; LEXER->emit(LEXER)
#define	    EMITNEW(t)				LEXER->emitNew(LEXER, t)
#define	    MATCHC(c)				LEXER->matchc(LEXER, c)
#define	    MATCHS(s)				LEXER->matchs(LEXER, s)
#define	    MATCHRANGE(c1,c2)	    LEXER->matchRange(LEXER, c1, c2)
#define	    MATCHANY()				LEXER->matchAny(LEXER)
#define	    LTOKEN  				LEXSTATE->token
#define	    HASFAILED()				(LEXSTATE->failed == ANTLR3_TRUE)
#define	    BACKTRACKING			LEXSTATE->backtracking
#define	    FAILEDFLAG				LEXSTATE->failed
#define	    INPUT					LEXER->input
#define	    STRSTREAM				INPUT
#define		ISTREAM					INPUT->istream
#define		INDEX()					ISTREAM->index(ISTREAM)
#define		SEEK(n)					ISTREAM->seek(ISTREAM, n)
#define	    EOF_TOKEN				&(LEXSTATE->tokSource->eofToken)
#define	    HASEXCEPTION()			(LEXSTATE->error == ANTLR3_TRUE)
#define	    EXCEPTION				LEXSTATE->exception
#define	    CONSTRUCTEX()			RECOGNIZER->exConstruct(RECOGNIZER)
#define	    LRECOVER()				LEXER->recover(LEXER)
#define	    MARK()					ISTREAM->mark(ISTREAM)
#define	    REWIND(m)				ISTREAM->rewind(ISTREAM, m)
#define	    REWINDLAST()			ISTREAM->rewindLast(ISTREAM)
#define		MEMOIZE(ri,si)			RECOGNIZER->memoize(RECOGNIZER, ri, si)
#define		HAVEPARSEDRULE(r)		RECOGNIZER->alreadyParsedRule(RECOGNIZER, r)
#define		PUSHSTREAM(str)			LEXER->pushCharStream(LEXER, str)
#define		POPSTREAM()				LEXER->popCharStream(LEXER)
#define		SETTEXT(str)			LEXSTATE->text = str
#define		SKIP()					LEXSTATE->token = &(TOKSOURCE->skipToken)
#define		USER1					LEXSTATE->user1
#define		USER2					LEXSTATE->user2
#define		USER3					LEXSTATE->user3
#define		CUSTOM					LEXSTATE->custom
#define		RULEMEMO				LEXSTATE->ruleMemo
#define		DBG						RECOGNIZER->debugger

/* If we have been told we can rely on the standard 8 bit or UTF16 input
 * stream, then we can define our macros to use the direct pointers
 * in the input object, which is much faster than indirect calls. This
 * is really only significant to lexers with a lot of fragment rules (which
 * do not place LA(1) in a temporary at the moment) and even then
 * only if there is a lot of input (order of say 1M or so).
 */
#if	defined(ANTLR3_INLINE_INPUT_8BIT) || defined(ANTLR3_INLINE_INPUT_UTF16)

# ifdef	ANTLR3_INLINE_INPUT_8BIT

/* 8 bit character set */

#  define	    NEXTCHAR	((pANTLR3_UINT8)(INPUT->nextChar))
#  define	    DATAP	((pANTLR3_UINT8)(INPUT->data))

# else

#  define	    NEXTCHAR	((pANTLR3_UINT16)(INPUT->nextChar))
#  define	    DATAP	((pANTLR3_UINT16)(INPUT->data))

# endif

# define	    LA(n) ((NEXTCHAR + n) > (DATAP + INPUT->sizeBuf) ? ANTLR3_CHARSTREAM_EOF : (ANTLR3_UCHAR)(*(NEXTCHAR + n - 1)))
# define            CONSUME()                                           \
{                                                                       \
    if        (NEXTCHAR < (DATAP + INPUT->sizeBuf))                     \
    {                                                                   \
        INPUT->charPositionInLine++;                                    \
        if  ((ANTLR3_UCHAR)(*NEXTCHAR) == INPUT->newlineChar)           \
        {                                                               \
            INPUT->line++;                                              \
            INPUT->charPositionInLine        = 0;                       \
            INPUT->currentLine                = (void *)(NEXTCHAR + 1); \
        }                                                               \
        INPUT->nextChar = (void *)(NEXTCHAR + 1);                       \
    }                                                                   \
}

#else

// Pick up the input character by calling the input stream implementation.
//
#define	    CONSUME()   INPUT->istream->consume(INPUT->istream)
#define	    LA(n)       INPUT->istream->_LA(INPUT->istream, n)

#endif

#define		TOKTEXT(tok, txt)				tok, (pANTLR3_UINT8)txt

/* The 4 tokens defined below may well clash with your own #defines or token types. If so
 * then for the present you must use different names for your defines as these are hard coded
 * in the code generator. It would be better not to use such names internally, and maybe
 * we can change this in a forthcoming release. I deliberately do not #undef these
 * here as this will at least give you a redefined error somewhere if they clash.
 */
#define	    UP	    ANTLR3_TOKEN_UP
#define	    DOWN    ANTLR3_TOKEN_DOWN
#define	    EOR	    ANTLR3_TOKEN_EOR
#define	    INVALID ANTLR3_TOKEN_INVALID


/* =============================================================================
 * Functions to create and destroy scopes. First come the rule scopes, followed
 * by the global declared scopes.
 */



/* ============================================================================= */

/* =============================================================================
 * Start of recognizer
 */

/* Forward declare the locally static matching functions we have generated and any predicate functions.
 */
static ANTLR3_INLINE
 void
	mT__63    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__64    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__65    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__66    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__67    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__68    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__69    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__70    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__71    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__72    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__73    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__74    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__75    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__76    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__77    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__78    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__79    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__80    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__81    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__82    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__83    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__84    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__85    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__86    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__87    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__88    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__89    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__90    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__91    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__92    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__93    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mT__94    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mCOMMA_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDOT_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mLPAREN_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mRPAREN_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mLBRACK_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mRBRACK_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mCOLON_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mARROW_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mSUBTYPE_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mOR_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mNOT_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mFORALL_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mEXISTS_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mLAMBDA_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mCHOICE_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDEF_DESC_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mAND_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mIFF_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mIMPLIES_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mREVIMPLIES_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mREVIFF_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mREVOR_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mREVAND_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTIMES_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mPLUS_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mMINUS_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mAPP_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTH1_UN_A    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTH1_UN_E    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTRUE_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mFALSE_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mEQUAL_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDISEQUAL_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mCNF_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mFOF_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTHF_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTFF_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTYPE_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mINCLUDE_TOK    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDEFINED_SYMBOL    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mWHITESPACE    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDISTINCT_OBJECT    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDO_CHAR    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mLOWER_WORD_SINGLE_QUOTED    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mSINGLE_QUOTED    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mSQ_CHAR    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mNUMERIC    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mLOWER_ALPHA    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mUPPER_ALPHA    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mALPHA_NUMERIC    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mUPPER_WORD    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mLOWER_WORD    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDOT    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mEXPONENT    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mSLASH    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mDECIMAL    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mSIGN    (pTptpLexer ctx, bool& pos);
static ANTLR3_INLINE
 void
	mNUMBER    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mCOMMENT    (pTptpLexer ctx);
static ANTLR3_INLINE
 void
	mTokens    (pTptpLexer ctx);
static void	TptpLexerFree(pTptpLexer ctx);

/* =========================================================================
 * Lexer matching rules end.
 * =========================================================================
 */



static void
TptpLexerFree  (pTptpLexer ctx)
{
    LEXER->free(LEXER);

    ANTLR3_FREE(ctx);
}

static void
TptpLexerReset (pTptpLexer ctx)
{
    RECOGNIZER->reset(RECOGNIZER);
}

/** \brief Name of the grammar file that generated this code
 */
static const char fileName[] = "/barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g";

/** \brief Return the name of the grammar file that generated this code.
 */
static const char * getGrammarFileName()
{
	return fileName;
}

/** \brief Create a new lexer called TptpLexer
 *
 * \param[in]    instream Pointer to an initialized input stream
 * \return
 *     - Success pTptpLexer initialized for the lex start
 *     - Fail NULL
 */
ANTLR3_API pTptpLexer TptpLexerNew
(
pANTLR3_INPUT_STREAM
 instream)
{
	// See if we can create a new lexer with the standard constructor
	//
	return TptpLexerNewSSD(instream, NULL);
}

/** \brief Create a new lexer called TptpLexer
 *
 * \param[in]    instream Pointer to an initialized input stream
 * \param[state] state Previously created shared recognizer stat
 * \return
 *     - Success pTptpLexer initialized for the lex start
 *     - Fail NULL
 */
ANTLR3_API pTptpLexer TptpLexerNewSSD
(pANTLR3_INPUT_STREAM instream, pANTLR3_RECOGNIZER_SHARED_STATE state)
{
    pTptpLexer ctx; // Context structure we will build and return

    ctx = (pTptpLexer) ANTLR3_CALLOC(1, sizeof(TptpLexer));

    if  (ctx == NULL)
    {
        // Failed to allocate memory for lexer context
        return  NULL;
    }

    /* -------------------------------------------------------------------
     * Memory for basic structure is allocated, now to fill in
     * in base ANTLR3 structures. We initialize the function pointers
     * for the standard ANTLR3 lexer function set, but upon return
     * from here, the programmer may set the pointers to provide custom
     * implementations of each function.
     *
     * We don't use the macros defined in TptpLexer.h here so you can get a sense
     * of what goes where.
     */

    /* Create a base lexer, using the supplied input stream
     */
    ctx->pLexer	= antlr3LexerNewStream(ANTLR3_SIZE_HINT, instream, state);

    /* Check that we allocated the memory correctly
     */
    if	(ctx->pLexer == NULL)
    {
		ANTLR3_FREE(ctx);
		return  NULL;
    }
    /* Install the implementation of our TptpLexer interface
     */
    ctx->mT__63	= mT__63;
    ctx->mT__64	= mT__64;
    ctx->mT__65	= mT__65;
    ctx->mT__66	= mT__66;
    ctx->mT__67	= mT__67;
    ctx->mT__68	= mT__68;
    ctx->mT__69	= mT__69;
    ctx->mT__70	= mT__70;
    ctx->mT__71	= mT__71;
    ctx->mT__72	= mT__72;
    ctx->mT__73	= mT__73;
    ctx->mT__74	= mT__74;
    ctx->mT__75	= mT__75;
    ctx->mT__76	= mT__76;
    ctx->mT__77	= mT__77;
    ctx->mT__78	= mT__78;
    ctx->mT__79	= mT__79;
    ctx->mT__80	= mT__80;
    ctx->mT__81	= mT__81;
    ctx->mT__82	= mT__82;
    ctx->mT__83	= mT__83;
    ctx->mT__84	= mT__84;
    ctx->mT__85	= mT__85;
    ctx->mT__86	= mT__86;
    ctx->mT__87	= mT__87;
    ctx->mT__88	= mT__88;
    ctx->mT__89	= mT__89;
    ctx->mT__90	= mT__90;
    ctx->mT__91	= mT__91;
    ctx->mT__92	= mT__92;
    ctx->mT__93	= mT__93;
    ctx->mT__94	= mT__94;
    ctx->mCOMMA_TOK	= mCOMMA_TOK;
    ctx->mDOT_TOK	= mDOT_TOK;
    ctx->mLPAREN_TOK	= mLPAREN_TOK;
    ctx->mRPAREN_TOK	= mRPAREN_TOK;
    ctx->mLBRACK_TOK	= mLBRACK_TOK;
    ctx->mRBRACK_TOK	= mRBRACK_TOK;
    ctx->mCOLON_TOK	= mCOLON_TOK;
    ctx->mARROW_TOK	= mARROW_TOK;
    ctx->mSUBTYPE_TOK	= mSUBTYPE_TOK;
    ctx->mOR_TOK	= mOR_TOK;
    ctx->mNOT_TOK	= mNOT_TOK;
    ctx->mFORALL_TOK	= mFORALL_TOK;
    ctx->mEXISTS_TOK	= mEXISTS_TOK;
    ctx->mLAMBDA_TOK	= mLAMBDA_TOK;
    ctx->mCHOICE_TOK	= mCHOICE_TOK;
    ctx->mDEF_DESC_TOK	= mDEF_DESC_TOK;
    ctx->mAND_TOK	= mAND_TOK;
    ctx->mIFF_TOK	= mIFF_TOK;
    ctx->mIMPLIES_TOK	= mIMPLIES_TOK;
    ctx->mREVIMPLIES_TOK	= mREVIMPLIES_TOK;
    ctx->mREVIFF_TOK	= mREVIFF_TOK;
    ctx->mREVOR_TOK	= mREVOR_TOK;
    ctx->mREVAND_TOK	= mREVAND_TOK;
    ctx->mTIMES_TOK	= mTIMES_TOK;
    ctx->mPLUS_TOK	= mPLUS_TOK;
    ctx->mMINUS_TOK	= mMINUS_TOK;
    ctx->mAPP_TOK	= mAPP_TOK;
    ctx->mTH1_UN_A	= mTH1_UN_A;
    ctx->mTH1_UN_E	= mTH1_UN_E;
    ctx->mTRUE_TOK	= mTRUE_TOK;
    ctx->mFALSE_TOK	= mFALSE_TOK;
    ctx->mEQUAL_TOK	= mEQUAL_TOK;
    ctx->mDISEQUAL_TOK	= mDISEQUAL_TOK;
    ctx->mCNF_TOK	= mCNF_TOK;
    ctx->mFOF_TOK	= mFOF_TOK;
    ctx->mTHF_TOK	= mTHF_TOK;
    ctx->mTFF_TOK	= mTFF_TOK;
    ctx->mTYPE_TOK	= mTYPE_TOK;
    ctx->mINCLUDE_TOK	= mINCLUDE_TOK;
    ctx->mDEFINED_SYMBOL	= mDEFINED_SYMBOL;
    ctx->mWHITESPACE	= mWHITESPACE;
    ctx->mDISTINCT_OBJECT	= mDISTINCT_OBJECT;
    ctx->mDO_CHAR	= mDO_CHAR;
    ctx->mLOWER_WORD_SINGLE_QUOTED	= mLOWER_WORD_SINGLE_QUOTED;
    ctx->mSINGLE_QUOTED	= mSINGLE_QUOTED;
    ctx->mSQ_CHAR	= mSQ_CHAR;
    ctx->mNUMERIC	= mNUMERIC;
    ctx->mLOWER_ALPHA	= mLOWER_ALPHA;
    ctx->mUPPER_ALPHA	= mUPPER_ALPHA;
    ctx->mALPHA_NUMERIC	= mALPHA_NUMERIC;
    ctx->mUPPER_WORD	= mUPPER_WORD;
    ctx->mLOWER_WORD	= mLOWER_WORD;
    ctx->mDOT	= mDOT;
    ctx->mEXPONENT	= mEXPONENT;
    ctx->mSLASH	= mSLASH;
    ctx->mDECIMAL	= mDECIMAL;
    ctx->mSIGN	= mSIGN;
    ctx->mNUMBER	= mNUMBER;
    ctx->mCOMMENT	= mCOMMENT;
    ctx->mTokens	= mTokens;

    /** When the nextToken() call is made to this lexer's pANTLR3_TOKEN_SOURCE
     *  it will call mTokens() in this generated code, and will pass it the ctx
     * pointer of this lexer, not the context of the base lexer, so store that now.
     */
    ctx->pLexer->ctx	    = ctx;

    /**Install the token matching function
     */
    ctx->pLexer->mTokens = (void (*) (void *))(mTokens);

    ctx->getGrammarFileName	= getGrammarFileName;
    ctx->free		= TptpLexerFree;
    ctx->reset          = TptpLexerReset;


    /* Return the newly built lexer to the caller
     */
    return  ctx;
}

/* =========================================================================
 * DFA tables for the lexer
 */
/** Static dfa state tables for Cyclic dfa:
 *    1745:5: ( ( SIGN[pos] )? num= DECIMAL | ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? | ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL )
 */
static const ANTLR3_INT32 dfa15_eot[7] =
    {
	-1, -1, -1, 4, -1, -1, -1
    };
static const ANTLR3_INT32 dfa15_eof[7] =
    {
	-1, -1, -1, -1, -1, -1, -1
    };
static const ANTLR3_INT32 dfa15_min[7] =
    {
	43, 48, 48, 46, -1, -1, -1
    };
static const ANTLR3_INT32 dfa15_max[7] =
    {
	57, 57, 57, 57, -1, -1, -1
    };
static const ANTLR3_INT32 dfa15_accept[7] =
    {
	-1, -1, -1, -1, 1, 2, 3
    };
static const ANTLR3_INT32 dfa15_special[7] =
    {
	-1, -1, -1, -1, -1, -1, -1
    };

/** Used when there is no transition table entry for a particular state */
#define dfa15_T_empty	    NULL

static const ANTLR3_INT32 dfa15_T0[] =
    {
	1, -1, 2, -1, -1, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3
    };

static const ANTLR3_INT32 dfa15_T1[] =
    {
	5, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3
    };

static const ANTLR3_INT32 dfa15_T2[] =
    {
	3, 3, 3, 3, 3, 3, 3, 3, 3, 3
    };


/* Transition tables are a table of sub tables, with some tables
 * reused for efficiency.
 */
static const ANTLR3_INT32 * const dfa15_transitions[] =
{
    dfa15_T0, dfa15_T2, dfa15_T2, dfa15_T1, NULL, NULL, NULL
};


/* Declare tracking structure for Cyclic DFA 15
 */
static
ANTLR3_CYCLIC_DFA cdfa15
    =	{
	    15,		    /* Decision number of this dfa	    */
	    /* Which decision this represents:   */
	    (const pANTLR3_UCHAR)"1745:5: ( ( SIGN[pos] )? num= DECIMAL | ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? | ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL )",
	    (CDFA_SPECIAL_FUNC) antlr3dfaspecialStateTransition,	/* Default special state transition function	*/

	    antlr3dfaspecialTransition,		/* DFA specialTransition is currently just a default function in the runtime */
	    antlr3dfapredict,			/* DFA simulator function is in the runtime */
	    dfa15_eot,	    /* EOT table			    */
	    dfa15_eof,	    /* EOF table			    */
	    dfa15_min,	    /* Minimum tokens for each state    */
	    dfa15_max,	    /* Maximum tokens for each state    */
	    dfa15_accept,	/* Accept table			    */
	    dfa15_special,	/* Special transition states	    */
	    dfa15_transitions	/* Table of transition tables	    */

	};
/* End of Cyclic DFA 15
 * ---------------------
 *//** Static dfa state tables for Cyclic dfa:
 *    1:1: Tokens : ( T__63 | T__64 | T__65 | T__66 | T__67 | T__68 | T__69 | T__70 | T__71 | T__72 | T__73 | T__74 | T__75 | T__76 | T__77 | T__78 | T__79 | T__80 | T__81 | T__82 | T__83 | T__84 | T__85 | T__86 | T__87 | T__88 | T__89 | T__90 | T__91 | T__92 | T__93 | T__94 | COMMA_TOK | DOT_TOK | LPAREN_TOK | RPAREN_TOK | LBRACK_TOK | RBRACK_TOK | COLON_TOK | ARROW_TOK | SUBTYPE_TOK | OR_TOK | NOT_TOK | FORALL_TOK | EXISTS_TOK | LAMBDA_TOK | CHOICE_TOK | DEF_DESC_TOK | AND_TOK | IFF_TOK | IMPLIES_TOK | REVIMPLIES_TOK | REVIFF_TOK | REVOR_TOK | REVAND_TOK | TIMES_TOK | PLUS_TOK | MINUS_TOK | APP_TOK | TH1_UN_A | TH1_UN_E | TRUE_TOK | FALSE_TOK | EQUAL_TOK | DISEQUAL_TOK | CNF_TOK | FOF_TOK | THF_TOK | TFF_TOK | TYPE_TOK | INCLUDE_TOK | DEFINED_SYMBOL | WHITESPACE | DISTINCT_OBJECT | LOWER_WORD_SINGLE_QUOTED | SINGLE_QUOTED | UPPER_WORD | LOWER_WORD | NUMBER | COMMENT );
 */
static const ANTLR3_INT32 dfa19_eot[256] =
    {
	-1, -1, -1, -1, -1, -1, -1, -1, -1, 47, -1, 50, 53, 55, -1, 58, -1, -1,
	62, -1, 63, 64, 30, 30, 30, 30, -1, -1, -1, -1, -1, -1, -1, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, 91, -1, -1, -1, -1, -1, 30, 30, 30, 30, 30, 30, -1,
	-1, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	-1, -1, 120, 121, 122, 123, 30, 30, -1, -1, -1, 45, 45, 45, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 142, 45, 45, 45, 45, -1, -1, -1, -1, 149,
	30, -1, 45, 45, 45, 45, 45, 45, 45, 45, 45, 162, 45, 45, 45, 45, 45, -1,
	45, 45, 45, 45, 174, 45, -1, 30, 45, 45, 45, 180, 181, 45, 45, 45, 185,
	186, 45, -1, 45, 45, 45, 45, 45, 195, 196, 45, 45, 45, 45, -1, 45, 30,
	45, 45, 45, -1, -1, 45, 207, 208, -1, -1, 209, 210, 211, 212, 213, 45,
	45, 45, -1, -1, 217, 218, 45, 45, 221, 222, 223, 45, 45, 227, -1, -1, -1,
	-1, -1, -1, -1, 228, 45, 45, -1, -1, 231, 45, -1, -1, -1, 45, 234, 45,
	-1, -1, 237, 45, -1, 239, 45, -1, 241, 45, -1, 45, -1, 246, -1, 247, 248,
	249, 45, -1, -1, -1, -1, 253, 254, 255, -1, -1, -1
    };
static const ANTLR3_INT32 dfa19_eof[256] =
    {
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1
    };
static const ANTLR3_INT32 dfa19_min[256] =
    {
	9, 97, -1, -1, -1, -1, -1, -1, -1, 62, -1, 38, 33, 63, -1, 43, -1, 61,
	62, -1, 48, 48, 110, 111, 102, 110, -1, -1, 32, -1, -1, -1, -1, 101, 105,
	97, 114, 115, 101, 114, 117, 101, 117, 84, 109, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, 62, -1, -1, -1, -1, -1, 102, 102, 102,
	102, 112, 99, 32, -1, 105, 102, 111, 108, 101, 95, 101, 115, 111, 111,
	109, 117, 109, 121, 95, 117, 105, -1, -1, 48, 48, 48, 48, 101, 108, 32,
	-1, 32, 108, 102, 116, 111, 115, 97, 105, 95, 115, 95, 100, 116, 97, 110,
	48, 112, 105, 101, 110, -1, -1, -1, -1, 48, 117, -1, 105, 101, 105, 114,
	101, 116, 110, 97, 102, 48, 102, 117, 105, 105, 100, -1, 101, 110, 97,
	99, 48, 117, -1, 100, 110, 114, 110, 48, 48, 101, 116, 116, 48, 48, 113,
	-1, 102, 102, 99, 101, 110, 48, 48, 116, 116, 97, 97, -1, 115, 101, 103,
	101, 99, -1, -1, 114, 48, 48, -1, -1, 48, 48, 48, 48, 48, 116, 110, 100,
	-1, -1, 48, 48, 108, 116, 48, 48, 48, 110, 116, 48, -1, -1, -1, -1, -1,
	-1, -1, 48, 116, 101, -1, -1, 48, 101, -1, -1, -1, 99, 48, 113, -1, -1,
	48, 114, -1, 48, 101, -1, 48, 101, -1, 95, -1, 48, -1, 48, 48, 48, 101,
	-1, -1, -1, -1, 48, 48, 48, -1, -1, -1
    };
static const ANTLR3_INT32 dfa19_max[256] =
    {
	126, 122, -1, -1, -1, -1, -1, -1, -1, 62, -1, 124, 61, 63, -1, 45, -1,
	126, 62, -1, 57, 57, 110, 111, 121, 110, -1, -1, 126, -1, -1, -1, -1, 101,
	105, 108, 114, 116, 101, 114, 117, 111, 117, 114, 109, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 62, -1, -1, -1, -1, -1, 102, 102,
	102, 102, 112, 99, 126, -1, 105, 115, 111, 108, 101, 95, 101, 116, 111,
	111, 109, 117, 109, 121, 95, 117, 105, -1, -1, 122, 122, 122, 122, 101,
	108, 126, -1, 126, 108, 102, 116, 111, 115, 97, 114, 95, 115, 95, 100,
	116, 97, 110, 122, 112, 114, 110, 110, -1, -1, -1, -1, 122, 117, -1, 105,
	101, 105, 114, 101, 116, 110, 97, 116, 122, 116, 117, 105, 105, 100, -1,
	101, 110, 101, 99, 122, 117, -1, 100, 110, 114, 110, 122, 122, 101, 116,
	116, 122, 122, 113, -1, 116, 116, 99, 101, 110, 122, 122, 116, 116, 97,
	97, -1, 115, 101, 103, 101, 99, -1, -1, 114, 122, 122, -1, -1, 122, 122,
	122, 122, 122, 116, 110, 100, -1, -1, 122, 122, 108, 116, 122, 122, 122,
	110, 116, 122, -1, -1, -1, -1, -1, -1, -1, 122, 116, 101, -1, -1, 122,
	101, -1, -1, -1, 99, 122, 113, -1, -1, 122, 114, -1, 122, 101, -1, 122,
	116, -1, 95, -1, 122, -1, 122, 122, 122, 116, -1, -1, -1, -1, 122, 122,
	122, -1, -1, -1
    };
static const ANTLR3_INT32 dfa19_accept[256] =
    {
	-1, -1, 33, 34, 35, 36, 37, 38, 39, -1, 42, -1, -1, -1, 46, -1, 49, -1,
	-1, 56, -1, -1, -1, -1, -1, -1, 73, 74, -1, 77, 78, 79, 80, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, 72, 41, 40, 54, 55, 43, 60, 65, 44,
	61, 45, 47, 48, 59, -1, 53, 51, 64, 57, 58, -1, -1, -1, -1, -1, -1, -1,
	76, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	50, 52, -1, -1, -1, -1, -1, -1, -1, 75, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 66, 67, 68, 69, -1, -1,
	75, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 26, -1,
	-1, -1, -1, -1, -1, 70, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	11, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 62, -1, -1, -1, -1, -1,
	4, 63, -1, -1, -1, 9, 10, -1, -1, -1, -1, -1, -1, -1, -1, 25, 27, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, 7, 8, 12, 13, 14, 15, 16, -1, -1, -1, 28,
	29, -1, -1, 32, 71, 1, -1, -1, -1, 5, 17, -1, -1, 30, -1, -1, 3, -1, -1,
	18, -1, 31, -1, 6, -1, -1, -1, -1, 2, 19, 20, 21, -1, -1, -1, 22, 23, 24
    };
static const ANTLR3_INT32 dfa19_special[256] =
    {
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1
    };

/** Used when there is no transition table entry for a particular state */
#define dfa19_T_empty	    NULL

static const ANTLR3_INT32 dfa19_T0[] =
    {
	82
    };

static const ANTLR3_INT32 dfa19_T1[] =
    {
	105
    };

static const ANTLR3_INT32 dfa19_T2[] =
    {
	118
    };

static const ANTLR3_INT32 dfa19_T3[] =
    {
	131
    };

static const ANTLR3_INT32 dfa19_T4[] =
    {
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, -1, -1, -1, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, 45, -1, 45, 45, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45
    };

static const ANTLR3_INT32 dfa19_T5[] =
    {
	147, -1, -1, -1, -1, -1, -1, -1, -1, 146
    };

static const ANTLR3_INT32 dfa19_T6[] =
    {
	155
    };

static const ANTLR3_INT32 dfa19_T7[] =
    {
	242, 243, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 244
    };

static const ANTLR3_INT32 dfa19_T8[] =
    {
	190, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 191
    };

static const ANTLR3_INT32 dfa19_T9[] =
    {
	89
    };

static const ANTLR3_INT32 dfa19_T10[] =
    {
	101
    };

static const ANTLR3_INT32 dfa19_T11[] =
    {
	127
    };

static const ANTLR3_INT32 dfa19_T12[] =
    {
	151
    };

static const ANTLR3_INT32 dfa19_T13[] =
    {
	177
    };

static const ANTLR3_INT32 dfa19_T14[] =
    {
	203
    };

static const ANTLR3_INT32 dfa19_T15[] =
    {
	128
    };

static const ANTLR3_INT32 dfa19_T16[] =
    {
	152
    };

static const ANTLR3_INT32 dfa19_T17[] =
    {
	178
    };

static const ANTLR3_INT32 dfa19_T18[] =
    {
	204
    };

static const ANTLR3_INT32 dfa19_T19[] =
    {
	224
    };

static const ANTLR3_INT32 dfa19_T20[] =
    {
	233
    };

static const ANTLR3_INT32 dfa19_T21[] =
    {
	240
    };

static const ANTLR3_INT32 dfa19_T22[] =
    {
	129
    };

static const ANTLR3_INT32 dfa19_T23[] =
    {
	153
    };

static const ANTLR3_INT32 dfa19_T24[] =
    {
	179
    };

static const ANTLR3_INT32 dfa19_T25[] =
    {
	205
    };

static const ANTLR3_INT32 dfa19_T26[] =
    {
	225
    };

static const ANTLR3_INT32 dfa19_T27[] =
    {
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, -1, -1, -1, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, 236, -1, 45, 45, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45
    };

static const ANTLR3_INT32 dfa19_T28[] =
    {
	104
    };

static const ANTLR3_INT32 dfa19_T29[] =
    {
	130
    };

static const ANTLR3_INT32 dfa19_T30[] =
    {
	26, 26, -1, 26, 26, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, 26, 12, 27, -1, 1, 32, 16, 28, 4, 5, 19, 20, 2, 21,
	3, 32, 31, 31, 31, 31, 31, 31, 31, 31, 31, 31, 8, -1, 17, 18, 9, 13, 15,
	29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29,
	29, 29, 29, 29, 29, 29, 29, 29, 6, -1, 7, 14, -1, -1, 30, 30, 22, 30, 30,
	23, 30, 30, 25, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 24, 30, 30, 30,
	30, 30, 30, -1, 10, -1, 11
    };

static const ANTLR3_INT32 dfa19_T31[] =
    {
	154
    };

static const ANTLR3_INT32 dfa19_T32[] =
    {
	78, 79
    };

static const ANTLR3_INT32 dfa19_T33[] =
    {
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, -1, -1, -1, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, 45, -1, 45, 45, 45, 45, 161,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45
    };

static const ANTLR3_INT32 dfa19_T34[] =
    {
	235
    };

static const ANTLR3_INT32 dfa19_T35[] =
    {
	86, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, 87, -1, -1, 88
    };

static const ANTLR3_INT32 dfa19_T36[] =
    {
	157
    };

static const ANTLR3_INT32 dfa19_T37[] =
    {
	183
    };

static const ANTLR3_INT32 dfa19_T38[] =
    {
	158
    };

static const ANTLR3_INT32 dfa19_T39[] =
    {
	184
    };

static const ANTLR3_INT32 dfa19_T40[] =
    {
	31, 31, 31, 31, 31, 31, 31, 31, 31, 31
    };

static const ANTLR3_INT32 dfa19_T41[] =
    {
	113
    };

static const ANTLR3_INT32 dfa19_T42[] =
    {
	140
    };

static const ANTLR3_INT32 dfa19_T43[] =
    {
	167
    };

static const ANTLR3_INT32 dfa19_T44[] =
    {
	194
    };

static const ANTLR3_INT32 dfa19_T45[] =
    {
	216
    };

static const ANTLR3_INT32 dfa19_T46[] =
    {
	54
    };

static const ANTLR3_INT32 dfa19_T47[] =
    {
	230
    };

static const ANTLR3_INT32 dfa19_T48[] =
    {
	137
    };

static const ANTLR3_INT32 dfa19_T49[] =
    {
	238
    };

static const ANTLR3_INT32 dfa19_T50[] =
    {
	245
    };

static const ANTLR3_INT32 dfa19_T51[] =
    {
	163, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 164
    };

static const ANTLR3_INT32 dfa19_T52[] =
    {
	250, 251, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 252
    };

static const ANTLR3_INT32 dfa19_T53[] =
    {
	187
    };

static const ANTLR3_INT32 dfa19_T54[] =
    {
	92
    };

static const ANTLR3_INT32 dfa19_T55[] =
    {
	93
    };

static const ANTLR3_INT32 dfa19_T56[] =
    {
	94
    };

static const ANTLR3_INT32 dfa19_T57[] =
    {
	90
    };

static const ANTLR3_INT32 dfa19_T58[] =
    {
	95
    };

static const ANTLR3_INT32 dfa19_T59[] =
    {
	96
    };

static const ANTLR3_INT32 dfa19_T60[] =
    {
	124
    };

static const ANTLR3_INT32 dfa19_T61[] =
    {
	97
    };

static const ANTLR3_INT32 dfa19_T62[] =
    {
	125
    };

static const ANTLR3_INT32 dfa19_T63[] =
    {
	150
    };

static const ANTLR3_INT32 dfa19_T64[] =
    {
	176
    };

static const ANTLR3_INT32 dfa19_T65[] =
    {
	202
    };

static const ANTLR3_INT32 dfa19_T66[] =
    {
	73
    };

static const ANTLR3_INT32 dfa19_T67[] =
    {
	111
    };

static const ANTLR3_INT32 dfa19_T68[] =
    {
	138
    };

static const ANTLR3_INT32 dfa19_T69[] =
    {
	165
    };

static const ANTLR3_INT32 dfa19_T70[] =
    {
	192
    };

static const ANTLR3_INT32 dfa19_T71[] =
    {
	214
    };

static const ANTLR3_INT32 dfa19_T72[] =
    {
	49, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 48
    };

static const ANTLR3_INT32 dfa19_T73[] =
    {
	109, 110
    };

static const ANTLR3_INT32 dfa19_T74[] =
    {
	30, 30, 30, 30, 30, 30, 30, 30, 30, 30, -1, -1, -1, -1, -1, -1, -1, 30,
	30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30,
	30, 30, 30, 30, 30, 30, 30, -1, -1, -1, -1, 30, -1, 30, 30, 30, 30, 30,
	30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30, 30,
	30, 30, 30
    };

static const ANTLR3_INT32 dfa19_T75[] =
    {
	83, -1, -1, -1, -1, -1, -1, -1, -1, -1, 84
    };

static const ANTLR3_INT32 dfa19_T76[] =
    {
	72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72,
	72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72,
	72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72,
	72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, 71, 71, 71, 71, 71, 71, 71,
	71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71, 71,
	71, 72, 72, 72, 72
    };

static const ANTLR3_INT32 dfa19_T77[] =
    {
	68, -1, 67, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, 69
    };

static const ANTLR3_INT32 dfa19_T78[] =
    {
	102, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 103
    };

static const ANTLR3_INT32 dfa19_T79[] =
    {
	51, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 52
    };

static const ANTLR3_INT32 dfa19_T80[] =
    {
	114
    };

static const ANTLR3_INT32 dfa19_T81[] =
    {
	141
    };

static const ANTLR3_INT32 dfa19_T82[] =
    {
	168
    };

static const ANTLR3_INT32 dfa19_T83[] =
    {
	72, 72, 72, 72, 72, 72, 72, 99, 72, 72, 72, 72, 72, 72, 72, 72, 98, 98,
	98, 98, 98, 98, 98, 98, 98, 98, 72, 72, 72, 72, 72, 72, 72, 98, 98, 98,
	98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98, 98,
	98, 98, 98, 98, 98, 72, 72, 72, 72, 100, 72, 100, 100, 100, 100, 100, 100,
	100, 100, 100, 100, 100, 100, 100, 100, 100, 100, 100, 100, 100, 100, 100,
	100, 100, 100, 100, 100, 72, 72, 72, 72
    };

static const ANTLR3_INT32 dfa19_T84[] =
    {
	115
    };

static const ANTLR3_INT32 dfa19_T85[] =
    {
	117
    };

static const ANTLR3_INT32 dfa19_T86[] =
    {
	144, -1, -1, -1, -1, -1, -1, -1, -1, 145
    };

static const ANTLR3_INT32 dfa19_T87[] =
    {
	106
    };

static const ANTLR3_INT32 dfa19_T88[] =
    {
	116
    };

static const ANTLR3_INT32 dfa19_T89[] =
    {
	132
    };

static const ANTLR3_INT32 dfa19_T90[] =
    {
	143
    };

static const ANTLR3_INT32 dfa19_T91[] =
    {
	169
    };

static const ANTLR3_INT32 dfa19_T92[] =
    {
	156
    };

static const ANTLR3_INT32 dfa19_T93[] =
    {
	182
    };

static const ANTLR3_INT32 dfa19_T94[] =
    {
	59, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
	-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 60
    };

static const ANTLR3_INT32 dfa19_T95[] =
    {
	206
    };

static const ANTLR3_INT32 dfa19_T96[] =
    {
	170
    };

static const ANTLR3_INT32 dfa19_T97[] =
    {
	197
    };

static const ANTLR3_INT32 dfa19_T98[] =
    {
	56, -1, 57
    };

static const ANTLR3_INT32 dfa19_T99[] =
    {
	61
    };

static const ANTLR3_INT32 dfa19_T100[] =
    {
	171, -1, -1, -1, 172
    };

static const ANTLR3_INT32 dfa19_T101[] =
    {
	198
    };

static const ANTLR3_INT32 dfa19_T102[] =
    {
	65
    };

static const ANTLR3_INT32 dfa19_T103[] =
    {
	66
    };

static const ANTLR3_INT32 dfa19_T104[] =
    {
	199
    };

static const ANTLR3_INT32 dfa19_T105[] =
    {
	219
    };

static const ANTLR3_INT32 dfa19_T106[] =
    {
	112
    };

static const ANTLR3_INT32 dfa19_T107[] =
    {
	81
    };

static const ANTLR3_INT32 dfa19_T108[] =
    {
	139
    };

static const ANTLR3_INT32 dfa19_T109[] =
    {
	166
    };

static const ANTLR3_INT32 dfa19_T110[] =
    {
	173
    };

static const ANTLR3_INT32 dfa19_T111[] =
    {
	200
    };

static const ANTLR3_INT32 dfa19_T112[] =
    {
	220
    };

static const ANTLR3_INT32 dfa19_T113[] =
    {
	232
    };

static const ANTLR3_INT32 dfa19_T114[] =
    {
	107
    };

static const ANTLR3_INT32 dfa19_T115[] =
    {
	193
    };

static const ANTLR3_INT32 dfa19_T116[] =
    {
	133, -1, -1, -1, -1, -1, -1, -1, -1, 134
    };

static const ANTLR3_INT32 dfa19_T117[] =
    {
	215
    };

static const ANTLR3_INT32 dfa19_T118[] =
    {
	119
    };

static const ANTLR3_INT32 dfa19_T119[] =
    {
	45, 45, 33, 34, 45, 35, 36, 45, 37, 45, 45, 38, 45, 45, 45, 39, 40, 41,
	42, 43, 44, 45, 45, 45, 45, 45
    };

static const ANTLR3_INT32 dfa19_T120[] =
    {
	148
    };

static const ANTLR3_INT32 dfa19_T121[] =
    {
	70
    };

static const ANTLR3_INT32 dfa19_T122[] =
    {
	175
    };

static const ANTLR3_INT32 dfa19_T123[] =
    {
	229
    };

static const ANTLR3_INT32 dfa19_T124[] =
    {
	201
    };

static const ANTLR3_INT32 dfa19_T125[] =
    {
	80
    };

static const ANTLR3_INT32 dfa19_T126[] =
    {
	76, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 75
    };

static const ANTLR3_INT32 dfa19_T127[] =
    {
	108
    };

static const ANTLR3_INT32 dfa19_T128[] =
    {
	135
    };

static const ANTLR3_INT32 dfa19_T129[] =
    {
	159, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 160
    };

static const ANTLR3_INT32 dfa19_T130[] =
    {
	74
    };

static const ANTLR3_INT32 dfa19_T131[] =
    {
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, -1, -1, -1, 45,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45, 45, 45, 45, 45, -1, -1, -1, -1, 45, -1, 45, 45, 45, 45, 226,
	45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45, 45,
	45, 45, 45
    };

static const ANTLR3_INT32 dfa19_T132[] =
    {
	136
    };

static const ANTLR3_INT32 dfa19_T133[] =
    {
	85
    };

static const ANTLR3_INT32 dfa19_T134[] =
    {
	77
    };

static const ANTLR3_INT32 dfa19_T135[] =
    {
	188, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 189
    };

static const ANTLR3_INT32 dfa19_T136[] =
    {
	46
    };


/* Transition tables are a table of sub tables, with some tables
 * reused for efficiency.
 */
static const ANTLR3_INT32 * const dfa19_transitions[] =
{
    dfa19_T30, dfa19_T119, NULL, NULL, NULL, NULL, NULL, NULL, NULL, dfa19_T136,
    NULL, dfa19_T72, dfa19_T79, dfa19_T46, NULL, dfa19_T98, NULL, dfa19_T94,
    dfa19_T99, NULL, dfa19_T40, dfa19_T40, dfa19_T102, dfa19_T103, dfa19_T77,
    dfa19_T121, NULL, NULL, dfa19_T76, NULL, NULL, NULL, NULL, dfa19_T66,
    dfa19_T130, dfa19_T126, dfa19_T134, dfa19_T32, dfa19_T125, dfa19_T107,
    dfa19_T0, dfa19_T75, dfa19_T133, dfa19_T35, dfa19_T9, NULL, NULL, NULL,
    NULL, NULL, NULL, NULL, NULL, NULL, NULL, NULL, NULL, NULL, NULL, dfa19_T57,
    NULL, NULL, NULL, NULL, NULL, dfa19_T54, dfa19_T55, dfa19_T56, dfa19_T58,
    dfa19_T59, dfa19_T61, dfa19_T83, NULL, dfa19_T10, dfa19_T78, dfa19_T28,
    dfa19_T1, dfa19_T87, dfa19_T114, dfa19_T127, dfa19_T73, dfa19_T67, dfa19_T106,
    dfa19_T41, dfa19_T80, dfa19_T84, dfa19_T88, dfa19_T85, dfa19_T2, dfa19_T118,
    NULL, NULL, dfa19_T74, dfa19_T74, dfa19_T74, dfa19_T74, dfa19_T60, dfa19_T62,
    dfa19_T83, NULL, dfa19_T83, dfa19_T11, dfa19_T15, dfa19_T22, dfa19_T29,
    dfa19_T3, dfa19_T89, dfa19_T116, dfa19_T128, dfa19_T132, dfa19_T48,
    dfa19_T68, dfa19_T108, dfa19_T42, dfa19_T81, dfa19_T4, dfa19_T90, dfa19_T86,
    dfa19_T5, dfa19_T120, NULL, NULL, NULL, NULL, dfa19_T74, dfa19_T63,
    NULL, dfa19_T12, dfa19_T16, dfa19_T23, dfa19_T31, dfa19_T6, dfa19_T92,
    dfa19_T36, dfa19_T38, dfa19_T129, dfa19_T33, dfa19_T51, dfa19_T69, dfa19_T109,
    dfa19_T43, dfa19_T82, NULL, dfa19_T91, dfa19_T96, dfa19_T100, dfa19_T110,
    dfa19_T4, dfa19_T122, NULL, dfa19_T64, dfa19_T13, dfa19_T17, dfa19_T24,
    dfa19_T4, dfa19_T4, dfa19_T93, dfa19_T37, dfa19_T39, dfa19_T4, dfa19_T4,
    dfa19_T53, NULL, dfa19_T135, dfa19_T8, dfa19_T70, dfa19_T115, dfa19_T44,
    dfa19_T4, dfa19_T4, dfa19_T97, dfa19_T101, dfa19_T104, dfa19_T111, NULL,
    dfa19_T124, dfa19_T65, dfa19_T14, dfa19_T18, dfa19_T25, NULL, NULL,
    dfa19_T95, dfa19_T4, dfa19_T4, NULL, NULL, dfa19_T4, dfa19_T4, dfa19_T4,
    dfa19_T4, dfa19_T4, dfa19_T71, dfa19_T117, dfa19_T45, NULL, NULL, dfa19_T4,
    dfa19_T4, dfa19_T105, dfa19_T112, dfa19_T4, dfa19_T74, dfa19_T4, dfa19_T19,
    dfa19_T26, dfa19_T131, NULL, NULL, NULL, NULL, NULL, NULL, NULL, dfa19_T4,
    dfa19_T123, dfa19_T47, NULL, NULL, dfa19_T4, dfa19_T113, NULL, NULL,
    NULL, dfa19_T20, dfa19_T4, dfa19_T34, NULL, NULL, dfa19_T27, dfa19_T49,
    NULL, dfa19_T4, dfa19_T21, NULL, dfa19_T4, dfa19_T7, NULL, dfa19_T50,
    NULL, dfa19_T4, NULL, dfa19_T4, dfa19_T4, dfa19_T4, dfa19_T52, NULL,
    NULL, NULL, NULL, dfa19_T4, dfa19_T4, dfa19_T4, NULL, NULL, NULL
};


/* Declare tracking structure for Cyclic DFA 19
 */
static
ANTLR3_CYCLIC_DFA cdfa19
    =	{
	    19,		    /* Decision number of this dfa	    */
	    /* Which decision this represents:   */
	    (const pANTLR3_UCHAR)"1:1: Tokens : ( T__63 | T__64 | T__65 | T__66 | T__67 | T__68 | T__69 | T__70 | T__71 | T__72 | T__73 | T__74 | T__75 | T__76 | T__77 | T__78 | T__79 | T__80 | T__81 | T__82 | T__83 | T__84 | T__85 | T__86 | T__87 | T__88 | T__89 | T__90 | T__91 | T__92 | T__93 | T__94 | COMMA_TOK | DOT_TOK | LPAREN_TOK | RPAREN_TOK | LBRACK_TOK | RBRACK_TOK | COLON_TOK | ARROW_TOK | SUBTYPE_TOK | OR_TOK | NOT_TOK | FORALL_TOK | EXISTS_TOK | LAMBDA_TOK | CHOICE_TOK | DEF_DESC_TOK | AND_TOK | IFF_TOK | IMPLIES_TOK | REVIMPLIES_TOK | REVIFF_TOK | REVOR_TOK | REVAND_TOK | TIMES_TOK | PLUS_TOK | MINUS_TOK | APP_TOK | TH1_UN_A | TH1_UN_E | TRUE_TOK | FALSE_TOK | EQUAL_TOK | DISEQUAL_TOK | CNF_TOK | FOF_TOK | THF_TOK | TFF_TOK | TYPE_TOK | INCLUDE_TOK | DEFINED_SYMBOL | WHITESPACE | DISTINCT_OBJECT | LOWER_WORD_SINGLE_QUOTED | SINGLE_QUOTED | UPPER_WORD | LOWER_WORD | NUMBER | COMMENT );",
	    (CDFA_SPECIAL_FUNC) antlr3dfaspecialStateTransition,	/* Default special state transition function	*/

	    antlr3dfaspecialTransition,		/* DFA specialTransition is currently just a default function in the runtime */
	    antlr3dfapredict,			/* DFA simulator function is in the runtime */
	    dfa19_eot,	    /* EOT table			    */
	    dfa19_eof,	    /* EOF table			    */
	    dfa19_min,	    /* Minimum tokens for each state    */
	    dfa19_max,	    /* Maximum tokens for each state    */
	    dfa19_accept,	/* Accept table			    */
	    dfa19_special,	/* Special transition states	    */
	    dfa19_transitions	/* Table of transition tables	    */

	};
/* End of Cyclic DFA 19
 * ---------------------
 */
/* =========================================================================
 * End of DFA tables for the lexer
 */

/* =========================================================================
 * Functions to match the lexer grammar defined tokens from the input stream
 */

//   Comes from: 48:7: ( '$ceiling' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__63
 *
 * Looks to match the characters the constitute the token T__63
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__63(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__63;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:48:7: ( '$ceiling' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:48:9: '$ceiling'
    {
        MATCHS(lit_1);
        if  (HASEXCEPTION())
        {
            goto ruleT__63Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__63Ex; /* Prevent compiler warnings */
    ruleT__63Ex: ;

}
// $ANTLR end T__63

//   Comes from: 49:7: ( '$difference' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__64
 *
 * Looks to match the characters the constitute the token T__64
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__64(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__64;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:49:7: ( '$difference' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:49:9: '$difference'
    {
        MATCHS(lit_2);
        if  (HASEXCEPTION())
        {
            goto ruleT__64Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__64Ex; /* Prevent compiler warnings */
    ruleT__64Ex: ;

}
// $ANTLR end T__64

//   Comes from: 50:7: ( '$distinct' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__65
 *
 * Looks to match the characters the constitute the token T__65
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__65(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__65;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:50:7: ( '$distinct' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:50:9: '$distinct'
    {
        MATCHS(lit_3);
        if  (HASEXCEPTION())
        {
            goto ruleT__65Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__65Ex; /* Prevent compiler warnings */
    ruleT__65Ex: ;

}
// $ANTLR end T__65

//   Comes from: 51:7: ( '$floor' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__66
 *
 * Looks to match the characters the constitute the token T__66
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__66(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__66;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:51:7: ( '$floor' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:51:9: '$floor'
    {
        MATCHS(lit_4);
        if  (HASEXCEPTION())
        {
            goto ruleT__66Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__66Ex; /* Prevent compiler warnings */
    ruleT__66Ex: ;

}
// $ANTLR end T__66

//   Comes from: 52:7: ( '$greater' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__67
 *
 * Looks to match the characters the constitute the token T__67
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__67(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__67;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:52:7: ( '$greater' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:52:9: '$greater'
    {
        MATCHS(lit_5);
        if  (HASEXCEPTION())
        {
            goto ruleT__67Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__67Ex; /* Prevent compiler warnings */
    ruleT__67Ex: ;

}
// $ANTLR end T__67

//   Comes from: 53:7: ( '$greatereq' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__68
 *
 * Looks to match the characters the constitute the token T__68
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__68(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__68;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:53:7: ( '$greatereq' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:53:9: '$greatereq'
    {
        MATCHS(lit_6);
        if  (HASEXCEPTION())
        {
            goto ruleT__68Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__68Ex; /* Prevent compiler warnings */
    ruleT__68Ex: ;

}
// $ANTLR end T__68

//   Comes from: 54:7: ( '$is_int' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__69
 *
 * Looks to match the characters the constitute the token T__69
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__69(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__69;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:54:7: ( '$is_int' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:54:9: '$is_int'
    {
        MATCHS(lit_7);
        if  (HASEXCEPTION())
        {
            goto ruleT__69Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__69Ex; /* Prevent compiler warnings */
    ruleT__69Ex: ;

}
// $ANTLR end T__69

//   Comes from: 55:7: ( '$is_rat' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__70
 *
 * Looks to match the characters the constitute the token T__70
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__70(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__70;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:55:7: ( '$is_rat' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:55:9: '$is_rat'
    {
        MATCHS(lit_8);
        if  (HASEXCEPTION())
        {
            goto ruleT__70Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__70Ex; /* Prevent compiler warnings */
    ruleT__70Ex: ;

}
// $ANTLR end T__70

//   Comes from: 56:7: ( '$ite_f' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__71
 *
 * Looks to match the characters the constitute the token T__71
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__71(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__71;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:56:7: ( '$ite_f' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:56:9: '$ite_f'
    {
        MATCHS(lit_9);
        if  (HASEXCEPTION())
        {
            goto ruleT__71Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__71Ex; /* Prevent compiler warnings */
    ruleT__71Ex: ;

}
// $ANTLR end T__71

//   Comes from: 57:7: ( '$ite_t' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__72
 *
 * Looks to match the characters the constitute the token T__72
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__72(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__72;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:57:7: ( '$ite_t' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:57:9: '$ite_t'
    {
        MATCHS(lit_10);
        if  (HASEXCEPTION())
        {
            goto ruleT__72Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__72Ex; /* Prevent compiler warnings */
    ruleT__72Ex: ;

}
// $ANTLR end T__72

//   Comes from: 58:7: ( '$less' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__73
 *
 * Looks to match the characters the constitute the token T__73
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__73(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__73;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:58:7: ( '$less' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:58:9: '$less'
    {
        MATCHS(lit_11);
        if  (HASEXCEPTION())
        {
            goto ruleT__73Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__73Ex; /* Prevent compiler warnings */
    ruleT__73Ex: ;

}
// $ANTLR end T__73

//   Comes from: 59:7: ( '$lesseq' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__74
 *
 * Looks to match the characters the constitute the token T__74
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__74(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__74;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:59:7: ( '$lesseq' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:59:9: '$lesseq'
    {
        MATCHS(lit_12);
        if  (HASEXCEPTION())
        {
            goto ruleT__74Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__74Ex; /* Prevent compiler warnings */
    ruleT__74Ex: ;

}
// $ANTLR end T__74

//   Comes from: 60:7: ( '$let_ff' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__75
 *
 * Looks to match the characters the constitute the token T__75
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__75(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__75;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:60:7: ( '$let_ff' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:60:9: '$let_ff'
    {
        MATCHS(lit_13);
        if  (HASEXCEPTION())
        {
            goto ruleT__75Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__75Ex; /* Prevent compiler warnings */
    ruleT__75Ex: ;

}
// $ANTLR end T__75

//   Comes from: 61:7: ( '$let_ft' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__76
 *
 * Looks to match the characters the constitute the token T__76
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__76(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__76;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:61:7: ( '$let_ft' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:61:9: '$let_ft'
    {
        MATCHS(lit_14);
        if  (HASEXCEPTION())
        {
            goto ruleT__76Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__76Ex; /* Prevent compiler warnings */
    ruleT__76Ex: ;

}
// $ANTLR end T__76

//   Comes from: 62:7: ( '$let_tf' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__77
 *
 * Looks to match the characters the constitute the token T__77
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__77(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__77;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:62:7: ( '$let_tf' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:62:9: '$let_tf'
    {
        MATCHS(lit_15);
        if  (HASEXCEPTION())
        {
            goto ruleT__77Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__77Ex; /* Prevent compiler warnings */
    ruleT__77Ex: ;

}
// $ANTLR end T__77

//   Comes from: 63:7: ( '$let_tt' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__78
 *
 * Looks to match the characters the constitute the token T__78
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__78(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__78;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:63:7: ( '$let_tt' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:63:9: '$let_tt'
    {
        MATCHS(lit_16);
        if  (HASEXCEPTION())
        {
            goto ruleT__78Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__78Ex; /* Prevent compiler warnings */
    ruleT__78Ex: ;

}
// $ANTLR end T__78

//   Comes from: 64:7: ( '$product' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__79
 *
 * Looks to match the characters the constitute the token T__79
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__79(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__79;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:64:7: ( '$product' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:64:9: '$product'
    {
        MATCHS(lit_17);
        if  (HASEXCEPTION())
        {
            goto ruleT__79Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__79Ex; /* Prevent compiler warnings */
    ruleT__79Ex: ;

}
// $ANTLR end T__79

//   Comes from: 65:7: ( '$quotient' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__80
 *
 * Looks to match the characters the constitute the token T__80
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__80(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__80;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:65:7: ( '$quotient' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:65:9: '$quotient'
    {
        MATCHS(lit_18);
        if  (HASEXCEPTION())
        {
            goto ruleT__80Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__80Ex; /* Prevent compiler warnings */
    ruleT__80Ex: ;

}
// $ANTLR end T__80

//   Comes from: 66:7: ( '$quotient_e' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__81
 *
 * Looks to match the characters the constitute the token T__81
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__81(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__81;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:66:7: ( '$quotient_e' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:66:9: '$quotient_e'
    {
        MATCHS(lit_19);
        if  (HASEXCEPTION())
        {
            goto ruleT__81Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__81Ex; /* Prevent compiler warnings */
    ruleT__81Ex: ;

}
// $ANTLR end T__81

//   Comes from: 67:7: ( '$quotient_f' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__82
 *
 * Looks to match the characters the constitute the token T__82
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__82(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__82;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:67:7: ( '$quotient_f' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:67:9: '$quotient_f'
    {
        MATCHS(lit_20);
        if  (HASEXCEPTION())
        {
            goto ruleT__82Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__82Ex; /* Prevent compiler warnings */
    ruleT__82Ex: ;

}
// $ANTLR end T__82

//   Comes from: 68:7: ( '$quotient_t' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__83
 *
 * Looks to match the characters the constitute the token T__83
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__83(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__83;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:68:7: ( '$quotient_t' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:68:9: '$quotient_t'
    {
        MATCHS(lit_21);
        if  (HASEXCEPTION())
        {
            goto ruleT__83Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__83Ex; /* Prevent compiler warnings */
    ruleT__83Ex: ;

}
// $ANTLR end T__83

//   Comes from: 69:7: ( '$remainder_e' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__84
 *
 * Looks to match the characters the constitute the token T__84
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__84(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__84;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:69:7: ( '$remainder_e' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:69:9: '$remainder_e'
    {
        MATCHS(lit_22);
        if  (HASEXCEPTION())
        {
            goto ruleT__84Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__84Ex; /* Prevent compiler warnings */
    ruleT__84Ex: ;

}
// $ANTLR end T__84

//   Comes from: 70:7: ( '$remainder_f' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__85
 *
 * Looks to match the characters the constitute the token T__85
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__85(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__85;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:70:7: ( '$remainder_f' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:70:9: '$remainder_f'
    {
        MATCHS(lit_23);
        if  (HASEXCEPTION())
        {
            goto ruleT__85Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__85Ex; /* Prevent compiler warnings */
    ruleT__85Ex: ;

}
// $ANTLR end T__85

//   Comes from: 71:7: ( '$remainder_t' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__86
 *
 * Looks to match the characters the constitute the token T__86
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__86(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__86;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:71:7: ( '$remainder_t' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:71:9: '$remainder_t'
    {
        MATCHS(lit_24);
        if  (HASEXCEPTION())
        {
            goto ruleT__86Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__86Ex; /* Prevent compiler warnings */
    ruleT__86Ex: ;

}
// $ANTLR end T__86

//   Comes from: 72:7: ( '$round' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__87
 *
 * Looks to match the characters the constitute the token T__87
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__87(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__87;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:72:7: ( '$round' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:72:9: '$round'
    {
        MATCHS(lit_25);
        if  (HASEXCEPTION())
        {
            goto ruleT__87Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__87Ex; /* Prevent compiler warnings */
    ruleT__87Ex: ;

}
// $ANTLR end T__87

//   Comes from: 73:7: ( '$sum' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__88
 *
 * Looks to match the characters the constitute the token T__88
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__88(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__88;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:73:7: ( '$sum' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:73:9: '$sum'
    {
        MATCHS(lit_26);
        if  (HASEXCEPTION())
        {
            goto ruleT__88Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__88Ex; /* Prevent compiler warnings */
    ruleT__88Ex: ;

}
// $ANTLR end T__88

//   Comes from: 74:7: ( '$tType' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__89
 *
 * Looks to match the characters the constitute the token T__89
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__89(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__89;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:74:7: ( '$tType' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:74:9: '$tType'
    {
        MATCHS(lit_27);
        if  (HASEXCEPTION())
        {
            goto ruleT__89Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__89Ex; /* Prevent compiler warnings */
    ruleT__89Ex: ;

}
// $ANTLR end T__89

//   Comes from: 75:7: ( '$to_int' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__90
 *
 * Looks to match the characters the constitute the token T__90
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__90(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__90;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:75:7: ( '$to_int' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:75:9: '$to_int'
    {
        MATCHS(lit_28);
        if  (HASEXCEPTION())
        {
            goto ruleT__90Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__90Ex; /* Prevent compiler warnings */
    ruleT__90Ex: ;

}
// $ANTLR end T__90

//   Comes from: 76:7: ( '$to_rat' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__91
 *
 * Looks to match the characters the constitute the token T__91
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__91(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__91;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:76:7: ( '$to_rat' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:76:9: '$to_rat'
    {
        MATCHS(lit_29);
        if  (HASEXCEPTION())
        {
            goto ruleT__91Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__91Ex; /* Prevent compiler warnings */
    ruleT__91Ex: ;

}
// $ANTLR end T__91

//   Comes from: 77:7: ( '$to_real' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__92
 *
 * Looks to match the characters the constitute the token T__92
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__92(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__92;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:77:7: ( '$to_real' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:77:9: '$to_real'
    {
        MATCHS(lit_30);
        if  (HASEXCEPTION())
        {
            goto ruleT__92Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__92Ex; /* Prevent compiler warnings */
    ruleT__92Ex: ;

}
// $ANTLR end T__92

//   Comes from: 78:7: ( '$truncate' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__93
 *
 * Looks to match the characters the constitute the token T__93
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__93(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__93;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:78:7: ( '$truncate' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:78:9: '$truncate'
    {
        MATCHS(lit_31);
        if  (HASEXCEPTION())
        {
            goto ruleT__93Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__93Ex; /* Prevent compiler warnings */
    ruleT__93Ex: ;

}
// $ANTLR end T__93

//   Comes from: 79:7: ( '$uminus' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start T__94
 *
 * Looks to match the characters the constitute the token T__94
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mT__94(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = T__94;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:79:7: ( '$uminus' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:79:9: '$uminus'
    {
        MATCHS(lit_32);
        if  (HASEXCEPTION())
        {
            goto ruleT__94Ex;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleT__94Ex; /* Prevent compiler warnings */
    ruleT__94Ex: ;

}
// $ANTLR end T__94

//   Comes from: 1614:12: ( ',' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start COMMA_TOK
 *
 * Looks to match the characters the constitute the token COMMA_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mCOMMA_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = COMMA_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1614:12: ( ',' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1614:14: ','
    {
        MATCHC(',');
        if  (HASEXCEPTION())
        {
            goto ruleCOMMA_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleCOMMA_TOKEx; /* Prevent compiler warnings */
    ruleCOMMA_TOKEx: ;

}
// $ANTLR end COMMA_TOK

//   Comes from: 1612:12: ( '.' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DOT_TOK
 *
 * Looks to match the characters the constitute the token DOT_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDOT_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = DOT_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1612:12: ( '.' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1612:14: '.'
    {
        MATCHC('.');
        if  (HASEXCEPTION())
        {
            goto ruleDOT_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleDOT_TOKEx; /* Prevent compiler warnings */
    ruleDOT_TOKEx: ;

}
// $ANTLR end DOT_TOK

//   Comes from: 1613:12: ( '(' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start LPAREN_TOK
 *
 * Looks to match the characters the constitute the token LPAREN_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mLPAREN_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = LPAREN_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1613:12: ( '(' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1613:14: '('
    {
        MATCHC('(');
        if  (HASEXCEPTION())
        {
            goto ruleLPAREN_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleLPAREN_TOKEx; /* Prevent compiler warnings */
    ruleLPAREN_TOKEx: ;

}
// $ANTLR end LPAREN_TOK

//   Comes from: 1614:12: ( ')' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start RPAREN_TOK
 *
 * Looks to match the characters the constitute the token RPAREN_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mRPAREN_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = RPAREN_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1614:12: ( ')' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1614:14: ')'
    {
        MATCHC(')');
        if  (HASEXCEPTION())
        {
            goto ruleRPAREN_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleRPAREN_TOKEx; /* Prevent compiler warnings */
    ruleRPAREN_TOKEx: ;

}
// $ANTLR end RPAREN_TOK

//   Comes from: 1615:12: ( '[' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start LBRACK_TOK
 *
 * Looks to match the characters the constitute the token LBRACK_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mLBRACK_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = LBRACK_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1615:12: ( '[' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1615:14: '['
    {
        MATCHC('[');
        if  (HASEXCEPTION())
        {
            goto ruleLBRACK_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleLBRACK_TOKEx; /* Prevent compiler warnings */
    ruleLBRACK_TOKEx: ;

}
// $ANTLR end LBRACK_TOK

//   Comes from: 1616:12: ( ']' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start RBRACK_TOK
 *
 * Looks to match the characters the constitute the token RBRACK_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mRBRACK_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = RBRACK_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1616:12: ( ']' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1616:14: ']'
    {
        MATCHC(']');
        if  (HASEXCEPTION())
        {
            goto ruleRBRACK_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleRBRACK_TOKEx; /* Prevent compiler warnings */
    ruleRBRACK_TOKEx: ;

}
// $ANTLR end RBRACK_TOK

//   Comes from: 1617:12: ( ':' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start COLON_TOK
 *
 * Looks to match the characters the constitute the token COLON_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mCOLON_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = COLON_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1617:12: ( ':' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1617:14: ':'
    {
        MATCHC(':');
        if  (HASEXCEPTION())
        {
            goto ruleCOLON_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleCOLON_TOKEx; /* Prevent compiler warnings */
    ruleCOLON_TOKEx: ;

}
// $ANTLR end COLON_TOK

//   Comes from: 1620:13: ( '>' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start ARROW_TOK
 *
 * Looks to match the characters the constitute the token ARROW_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mARROW_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = ARROW_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1620:13: ( '>' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1620:15: '>'
    {
        MATCHC('>');
        if  (HASEXCEPTION())
        {
            goto ruleARROW_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleARROW_TOKEx; /* Prevent compiler warnings */
    ruleARROW_TOKEx: ;

}
// $ANTLR end ARROW_TOK

//   Comes from: 1621:13: ( '>>' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start SUBTYPE_TOK
 *
 * Looks to match the characters the constitute the token SUBTYPE_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mSUBTYPE_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = SUBTYPE_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1621:13: ( '>>' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1621:15: '>>'
    {
        MATCHS(lit_33);
        if  (HASEXCEPTION())
        {
            goto ruleSUBTYPE_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleSUBTYPE_TOKEx; /* Prevent compiler warnings */
    ruleSUBTYPE_TOKEx: ;

}
// $ANTLR end SUBTYPE_TOK

//   Comes from: 1624:16: ( '|' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start OR_TOK
 *
 * Looks to match the characters the constitute the token OR_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mOR_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = OR_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1624:16: ( '|' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1624:18: '|'
    {
        MATCHC('|');
        if  (HASEXCEPTION())
        {
            goto ruleOR_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleOR_TOKEx; /* Prevent compiler warnings */
    ruleOR_TOKEx: ;

}
// $ANTLR end OR_TOK

//   Comes from: 1625:16: ( '~' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start NOT_TOK
 *
 * Looks to match the characters the constitute the token NOT_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mNOT_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = NOT_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1625:16: ( '~' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1625:18: '~'
    {
        MATCHC('~');
        if  (HASEXCEPTION())
        {
            goto ruleNOT_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleNOT_TOKEx; /* Prevent compiler warnings */
    ruleNOT_TOKEx: ;

}
// $ANTLR end NOT_TOK

//   Comes from: 1626:16: ( '!' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start FORALL_TOK
 *
 * Looks to match the characters the constitute the token FORALL_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mFORALL_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = FORALL_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1626:16: ( '!' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1626:18: '!'
    {
        MATCHC('!');
        if  (HASEXCEPTION())
        {
            goto ruleFORALL_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleFORALL_TOKEx; /* Prevent compiler warnings */
    ruleFORALL_TOKEx: ;

}
// $ANTLR end FORALL_TOK

//   Comes from: 1627:16: ( '?' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start EXISTS_TOK
 *
 * Looks to match the characters the constitute the token EXISTS_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mEXISTS_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = EXISTS_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1627:16: ( '?' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1627:18: '?'
    {
        MATCHC('?');
        if  (HASEXCEPTION())
        {
            goto ruleEXISTS_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleEXISTS_TOKEx; /* Prevent compiler warnings */
    ruleEXISTS_TOKEx: ;

}
// $ANTLR end EXISTS_TOK

//   Comes from: 1628:16: ( '^' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start LAMBDA_TOK
 *
 * Looks to match the characters the constitute the token LAMBDA_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mLAMBDA_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = LAMBDA_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1628:16: ( '^' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1628:18: '^'
    {
        MATCHC('^');
        if  (HASEXCEPTION())
        {
            goto ruleLAMBDA_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleLAMBDA_TOKEx; /* Prevent compiler warnings */
    ruleLAMBDA_TOKEx: ;

}
// $ANTLR end LAMBDA_TOK

//   Comes from: 1629:16: ( '@+' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start CHOICE_TOK
 *
 * Looks to match the characters the constitute the token CHOICE_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mCHOICE_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = CHOICE_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1629:16: ( '@+' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1629:18: '@+'
    {
        MATCHS(lit_34);
        if  (HASEXCEPTION())
        {
            goto ruleCHOICE_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleCHOICE_TOKEx; /* Prevent compiler warnings */
    ruleCHOICE_TOKEx: ;

}
// $ANTLR end CHOICE_TOK

//   Comes from: 1630:16: ( '@-' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DEF_DESC_TOK
 *
 * Looks to match the characters the constitute the token DEF_DESC_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDEF_DESC_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = DEF_DESC_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1630:16: ( '@-' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1630:18: '@-'
    {
        MATCHS(lit_35);
        if  (HASEXCEPTION())
        {
            goto ruleDEF_DESC_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleDEF_DESC_TOKEx; /* Prevent compiler warnings */
    ruleDEF_DESC_TOKEx: ;

}
// $ANTLR end DEF_DESC_TOK

//   Comes from: 1631:16: ( '&' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start AND_TOK
 *
 * Looks to match the characters the constitute the token AND_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mAND_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = AND_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1631:16: ( '&' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1631:18: '&'
    {
        MATCHC('&');
        if  (HASEXCEPTION())
        {
            goto ruleAND_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleAND_TOKEx; /* Prevent compiler warnings */
    ruleAND_TOKEx: ;

}
// $ANTLR end AND_TOK

//   Comes from: 1632:16: ( '<=>' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start IFF_TOK
 *
 * Looks to match the characters the constitute the token IFF_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mIFF_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = IFF_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1632:16: ( '<=>' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1632:18: '<=>'
    {
        MATCHS(lit_36);
        if  (HASEXCEPTION())
        {
            goto ruleIFF_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleIFF_TOKEx; /* Prevent compiler warnings */
    ruleIFF_TOKEx: ;

}
// $ANTLR end IFF_TOK

//   Comes from: 1633:16: ( '=>' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start IMPLIES_TOK
 *
 * Looks to match the characters the constitute the token IMPLIES_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mIMPLIES_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = IMPLIES_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1633:16: ( '=>' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1633:18: '=>'
    {
        MATCHS(lit_37);
        if  (HASEXCEPTION())
        {
            goto ruleIMPLIES_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleIMPLIES_TOKEx; /* Prevent compiler warnings */
    ruleIMPLIES_TOKEx: ;

}
// $ANTLR end IMPLIES_TOK

//   Comes from: 1634:16: ( '<=' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start REVIMPLIES_TOK
 *
 * Looks to match the characters the constitute the token REVIMPLIES_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mREVIMPLIES_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = REVIMPLIES_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1634:16: ( '<=' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1634:18: '<='
    {
        MATCHS(lit_38);
        if  (HASEXCEPTION())
        {
            goto ruleREVIMPLIES_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleREVIMPLIES_TOKEx; /* Prevent compiler warnings */
    ruleREVIMPLIES_TOKEx: ;

}
// $ANTLR end REVIMPLIES_TOK

//   Comes from: 1635:16: ( '<~>' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start REVIFF_TOK
 *
 * Looks to match the characters the constitute the token REVIFF_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mREVIFF_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = REVIFF_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1635:16: ( '<~>' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1635:18: '<~>'
    {
        MATCHS(lit_39);
        if  (HASEXCEPTION())
        {
            goto ruleREVIFF_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleREVIFF_TOKEx; /* Prevent compiler warnings */
    ruleREVIFF_TOKEx: ;

}
// $ANTLR end REVIFF_TOK

//   Comes from: 1636:16: ( '~|' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start REVOR_TOK
 *
 * Looks to match the characters the constitute the token REVOR_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mREVOR_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = REVOR_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1636:16: ( '~|' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1636:18: '~|'
    {
        MATCHS(lit_40);
        if  (HASEXCEPTION())
        {
            goto ruleREVOR_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleREVOR_TOKEx; /* Prevent compiler warnings */
    ruleREVOR_TOKEx: ;

}
// $ANTLR end REVOR_TOK

//   Comes from: 1637:16: ( '~&' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start REVAND_TOK
 *
 * Looks to match the characters the constitute the token REVAND_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mREVAND_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = REVAND_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1637:16: ( '~&' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1637:18: '~&'
    {
        MATCHS(lit_41);
        if  (HASEXCEPTION())
        {
            goto ruleREVAND_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleREVAND_TOKEx; /* Prevent compiler warnings */
    ruleREVAND_TOKEx: ;

}
// $ANTLR end REVAND_TOK

//   Comes from: 1638:16: ( '*' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start TIMES_TOK
 *
 * Looks to match the characters the constitute the token TIMES_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mTIMES_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = TIMES_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1638:16: ( '*' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1638:18: '*'
    {
        MATCHC('*');
        if  (HASEXCEPTION())
        {
            goto ruleTIMES_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleTIMES_TOKEx; /* Prevent compiler warnings */
    ruleTIMES_TOKEx: ;

}
// $ANTLR end TIMES_TOK

//   Comes from: 1639:16: ( '+' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start PLUS_TOK
 *
 * Looks to match the characters the constitute the token PLUS_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mPLUS_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = PLUS_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1639:16: ( '+' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1639:18: '+'
    {
        MATCHC('+');
        if  (HASEXCEPTION())
        {
            goto rulePLUS_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto rulePLUS_TOKEx; /* Prevent compiler warnings */
    rulePLUS_TOKEx: ;

}
// $ANTLR end PLUS_TOK

//   Comes from: 1640:16: ( '-' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start MINUS_TOK
 *
 * Looks to match the characters the constitute the token MINUS_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mMINUS_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = MINUS_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1640:16: ( '-' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1640:18: '-'
    {
        MATCHC('-');
        if  (HASEXCEPTION())
        {
            goto ruleMINUS_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleMINUS_TOKEx; /* Prevent compiler warnings */
    ruleMINUS_TOKEx: ;

}
// $ANTLR end MINUS_TOK

//   Comes from: 1641:16: ( '@' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start APP_TOK
 *
 * Looks to match the characters the constitute the token APP_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mAPP_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = APP_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1641:16: ( '@' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1641:18: '@'
    {
        MATCHC('@');
        if  (HASEXCEPTION())
        {
            goto ruleAPP_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleAPP_TOKEx; /* Prevent compiler warnings */
    ruleAPP_TOKEx: ;

}
// $ANTLR end APP_TOK

//   Comes from: 1643:16: ( '!!' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start TH1_UN_A
 *
 * Looks to match the characters the constitute the token TH1_UN_A
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mTH1_UN_A(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = TH1_UN_A;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1643:16: ( '!!' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1643:18: '!!'
    {
        MATCHS(lit_42);
        if  (HASEXCEPTION())
        {
            goto ruleTH1_UN_AEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleTH1_UN_AEx; /* Prevent compiler warnings */
    ruleTH1_UN_AEx: ;

}
// $ANTLR end TH1_UN_A

//   Comes from: 1644:16: ( '??' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start TH1_UN_E
 *
 * Looks to match the characters the constitute the token TH1_UN_E
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mTH1_UN_E(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = TH1_UN_E;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1644:16: ( '??' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1644:18: '??'
    {
        MATCHS(lit_43);
        if  (HASEXCEPTION())
        {
            goto ruleTH1_UN_EEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleTH1_UN_EEx; /* Prevent compiler warnings */
    ruleTH1_UN_EEx: ;

}
// $ANTLR end TH1_UN_E

//   Comes from: 1647:14: ( '$true' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start TRUE_TOK
 *
 * Looks to match the characters the constitute the token TRUE_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mTRUE_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = TRUE_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1647:14: ( '$true' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1647:16: '$true'
    {
        MATCHS(lit_44);
        if  (HASEXCEPTION())
        {
            goto ruleTRUE_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleTRUE_TOKEx; /* Prevent compiler warnings */
    ruleTRUE_TOKEx: ;

}
// $ANTLR end TRUE_TOK

//   Comes from: 1648:14: ( '$false' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start FALSE_TOK
 *
 * Looks to match the characters the constitute the token FALSE_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mFALSE_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = FALSE_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1648:14: ( '$false' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1648:16: '$false'
    {
        MATCHS(lit_45);
        if  (HASEXCEPTION())
        {
            goto ruleFALSE_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleFALSE_TOKEx; /* Prevent compiler warnings */
    ruleFALSE_TOKEx: ;

}
// $ANTLR end FALSE_TOK

//   Comes from: 1649:14: ( '=' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start EQUAL_TOK
 *
 * Looks to match the characters the constitute the token EQUAL_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mEQUAL_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = EQUAL_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1649:14: ( '=' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1649:16: '='
    {
        MATCHC('=');
        if  (HASEXCEPTION())
        {
            goto ruleEQUAL_TOKEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleEQUAL_TOKEx; /* Prevent compiler warnings */
    ruleEQUAL_TOKEx: ;

}
// $ANTLR end EQUAL_TOK

//   Comes from: 1650:14: ( '!=' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DISEQUAL_TOK
 *
 * Looks to match the characters the constitute the token DISEQUAL_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDISEQUAL_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = DISEQUAL_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1650:14: ( '!=' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1650:16: '!='
    {
        MATCHS(lit_46);
        if  (HASEXCEPTION())
        {
            goto ruleDISEQUAL_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleDISEQUAL_TOKEx; /* Prevent compiler warnings */
    ruleDISEQUAL_TOKEx: ;

}
// $ANTLR end DISEQUAL_TOK

//   Comes from: 1653:13: ( 'cnf' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start CNF_TOK
 *
 * Looks to match the characters the constitute the token CNF_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mCNF_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = CNF_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1653:13: ( 'cnf' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1653:15: 'cnf'
    {
        MATCHS(lit_47);
        if  (HASEXCEPTION())
        {
            goto ruleCNF_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleCNF_TOKEx; /* Prevent compiler warnings */
    ruleCNF_TOKEx: ;

}
// $ANTLR end CNF_TOK

//   Comes from: 1654:13: ( 'fof' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start FOF_TOK
 *
 * Looks to match the characters the constitute the token FOF_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mFOF_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = FOF_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1654:13: ( 'fof' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1654:15: 'fof'
    {
        MATCHS(lit_48);
        if  (HASEXCEPTION())
        {
            goto ruleFOF_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleFOF_TOKEx; /* Prevent compiler warnings */
    ruleFOF_TOKEx: ;

}
// $ANTLR end FOF_TOK

//   Comes from: 1655:13: ( 'thf' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start THF_TOK
 *
 * Looks to match the characters the constitute the token THF_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mTHF_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = THF_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1655:13: ( 'thf' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1655:15: 'thf'
    {
        MATCHS(lit_49);
        if  (HASEXCEPTION())
        {
            goto ruleTHF_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleTHF_TOKEx; /* Prevent compiler warnings */
    ruleTHF_TOKEx: ;

}
// $ANTLR end THF_TOK

//   Comes from: 1656:13: ( 'tff' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start TFF_TOK
 *
 * Looks to match the characters the constitute the token TFF_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mTFF_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = TFF_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1656:13: ( 'tff' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1656:15: 'tff'
    {
        MATCHS(lit_50);
        if  (HASEXCEPTION())
        {
            goto ruleTFF_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleTFF_TOKEx; /* Prevent compiler warnings */
    ruleTFF_TOKEx: ;

}
// $ANTLR end TFF_TOK

//   Comes from: 1657:13: ( 'type' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start TYPE_TOK
 *
 * Looks to match the characters the constitute the token TYPE_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mTYPE_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = TYPE_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1657:13: ( 'type' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1657:15: 'type'
    {
        MATCHS(lit_51);
        if  (HASEXCEPTION())
        {
            goto ruleTYPE_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleTYPE_TOKEx; /* Prevent compiler warnings */
    ruleTYPE_TOKEx: ;

}
// $ANTLR end TYPE_TOK

//   Comes from: 1658:13: ( 'include' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start INCLUDE_TOK
 *
 * Looks to match the characters the constitute the token INCLUDE_TOK
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mINCLUDE_TOK(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = INCLUDE_TOK;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1658:13: ( 'include' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1658:15: 'include'
    {
        MATCHS(lit_52);
        if  (HASEXCEPTION())
        {
            goto ruleINCLUDE_TOKEx;
        }




    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleINCLUDE_TOKEx; /* Prevent compiler warnings */
    ruleINCLUDE_TOKEx: ;

}
// $ANTLR end INCLUDE_TOK

//   Comes from: 1661:16: ( '$' LOWER_WORD )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DEFINED_SYMBOL
 *
 * Looks to match the characters the constitute the token DEFINED_SYMBOL
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDEFINED_SYMBOL(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = DEFINED_SYMBOL;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1661:16: ( '$' LOWER_WORD )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1661:18: '$' LOWER_WORD
    {
        MATCHC('$');
        if  (HASEXCEPTION())
        {
            goto ruleDEFINED_SYMBOLEx;
        }


        /* 1661:18: '$' LOWER_WORD */
        mLOWER_WORD(ctx );
        if  (HASEXCEPTION())
        {
            goto ruleDEFINED_SYMBOLEx;
        }



    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleDEFINED_SYMBOLEx; /* Prevent compiler warnings */
    ruleDEFINED_SYMBOLEx: ;

}
// $ANTLR end DEFINED_SYMBOL

//   Comes from: 1678:3: ( ( ' ' | '\\t' | '\\f' | '\\r' | '\\n' )+ )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start WHITESPACE
 *
 * Looks to match the characters the constitute the token WHITESPACE
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mWHITESPACE(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = WHITESPACE;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1678:3: ( ( ' ' | '\\t' | '\\f' | '\\r' | '\\n' )+ )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1678:5: ( ' ' | '\\t' | '\\f' | '\\r' | '\\n' )+
    {
        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1678:5: ( ' ' | '\\t' | '\\f' | '\\r' | '\\n' )+
        {
            int cnt1=0;

            for (;;)
            {
                int alt1=2;
        	switch ( LA(1) )
        	{
        	case '\t':
        	case '\n':
        	case '\f':
        	case '\r':
        	case ' ':
        		{
        			alt1=1;
        		}
        	    break;

        	}

        	switch (alt1)
        	{
        	    case 1:
        	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
        	        {
        	            if ( ((LA(1) >= '\t') && (LA(1) <= '\n')) || ((LA(1) >= '\f') && (LA(1) <= '\r')) || LA(1) == ' ' )
        	            {
        	                CONSUME();
        	            }
        	            else
        	            {
        	                CONSTRUCTEX();
        	                EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
        	                EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

        	                LRECOVER();
        	                goto ruleWHITESPACEEx;
        	            }


        	        }
        	        break;

        	    default:

        		if ( cnt1 >= 1 )
        		{
        		    goto loop1;
        		}
        		/* mismatchedSetEx()
        		 */
        		CONSTRUCTEX();
        		EXCEPTION->type = ANTLR3_EARLY_EXIT_EXCEPTION;
        		EXCEPTION->name = (void *)ANTLR3_EARLY_EXIT_NAME;


        		goto ruleWHITESPACEEx;
        	}
        	cnt1++;
            }
            loop1: ;	/* Jump to here if this rule does not match */
        }

        {
             SKIP();
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleWHITESPACEEx; /* Prevent compiler warnings */
    ruleWHITESPACEEx: ;

}
// $ANTLR end WHITESPACE

//   Comes from: 1683:17: ( '\"' ( DO_CHAR )* '\"' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DISTINCT_OBJECT
 *
 * Looks to match the characters the constitute the token DISTINCT_OBJECT
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDISTINCT_OBJECT(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = DISTINCT_OBJECT;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1683:17: ( '\"' ( DO_CHAR )* '\"' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1683:19: '\"' ( DO_CHAR )* '\"'
    {
        MATCHC('"');
        if  (HASEXCEPTION())
        {
            goto ruleDISTINCT_OBJECTEx;
        }


        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1683:23: ( DO_CHAR )*

        for (;;)
        {
            int alt2=2;
            switch ( LA(1) )
            {
            case ' ':
            case '!':
            case '#':
            case '$':
            case '%':
            case '&':
            case '\'':
            case '(':
            case ')':
            case '*':
            case '+':
            case ',':
            case '-':
            case '.':
            case '/':
            case '0':
            case '1':
            case '2':
            case '3':
            case '4':
            case '5':
            case '6':
            case '7':
            case '8':
            case '9':
            case ':':
            case ';':
            case '<':
            case '=':
            case '>':
            case '?':
            case '@':
            case 'A':
            case 'B':
            case 'C':
            case 'D':
            case 'E':
            case 'F':
            case 'G':
            case 'H':
            case 'I':
            case 'J':
            case 'K':
            case 'L':
            case 'M':
            case 'N':
            case 'O':
            case 'P':
            case 'Q':
            case 'R':
            case 'S':
            case 'T':
            case 'U':
            case 'V':
            case 'W':
            case 'X':
            case 'Y':
            case 'Z':
            case '[':
            case '\\':
            case ']':
            case '^':
            case '_':
            case '`':
            case 'a':
            case 'b':
            case 'c':
            case 'd':
            case 'e':
            case 'f':
            case 'g':
            case 'h':
            case 'i':
            case 'j':
            case 'k':
            case 'l':
            case 'm':
            case 'n':
            case 'o':
            case 'p':
            case 'q':
            case 'r':
            case 's':
            case 't':
            case 'u':
            case 'v':
            case 'w':
            case 'x':
            case 'y':
            case 'z':
            case '{':
            case '|':
            case '}':
            case '~':
            	{
            		alt2=1;
            	}
                break;

            }

            switch (alt2)
            {
        	case 1:
        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1683:24: DO_CHAR
        	    {
        	        /* 1683:24: DO_CHAR */
        	        mDO_CHAR(ctx );
        	        if  (HASEXCEPTION())
        	        {
        	            goto ruleDISTINCT_OBJECTEx;
        	        }



        	    }
        	    break;

        	default:
        	    goto loop2;	/* break out of the loop */
        	    break;
            }
        }
        loop2: ; /* Jump out to here if this rule does not match */


        MATCHC('"');
        if  (HASEXCEPTION())
        {
            goto ruleDISTINCT_OBJECTEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleDISTINCT_OBJECTEx; /* Prevent compiler warnings */
    ruleDISTINCT_OBJECTEx: ;

}
// $ANTLR end DISTINCT_OBJECT

//   Comes from: 1680:18: ( ' ' .. '!' | '#' .. '[' | ']' .. '~' | '\\\\\"' | '\\\\\\\\' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DO_CHAR
 *
 * Looks to match the characters the constitute the token DO_CHAR
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDO_CHAR(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    {
        //  /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1680:18: ( ' ' .. '!' | '#' .. '[' | ']' .. '~' | '\\\\\"' | '\\\\\\\\' )

        ANTLR3_UINT32 alt3;

        alt3=5;

        switch ( LA(1) )
        {
        case ' ':
        case '!':
        	{
        		alt3=1;
        	}
            break;
        case '#':
        case '$':
        case '%':
        case '&':
        case '\'':
        case '(':
        case ')':
        case '*':
        case '+':
        case ',':
        case '-':
        case '.':
        case '/':
        case '0':
        case '1':
        case '2':
        case '3':
        case '4':
        case '5':
        case '6':
        case '7':
        case '8':
        case '9':
        case ':':
        case ';':
        case '<':
        case '=':
        case '>':
        case '?':
        case '@':
        case 'A':
        case 'B':
        case 'C':
        case 'D':
        case 'E':
        case 'F':
        case 'G':
        case 'H':
        case 'I':
        case 'J':
        case 'K':
        case 'L':
        case 'M':
        case 'N':
        case 'O':
        case 'P':
        case 'Q':
        case 'R':
        case 'S':
        case 'T':
        case 'U':
        case 'V':
        case 'W':
        case 'X':
        case 'Y':
        case 'Z':
        case '[':
        	{
        		alt3=2;
        	}
            break;
        case ']':
        case '^':
        case '_':
        case '`':
        case 'a':
        case 'b':
        case 'c':
        case 'd':
        case 'e':
        case 'f':
        case 'g':
        case 'h':
        case 'i':
        case 'j':
        case 'k':
        case 'l':
        case 'm':
        case 'n':
        case 'o':
        case 'p':
        case 'q':
        case 'r':
        case 's':
        case 't':
        case 'u':
        case 'v':
        case 'w':
        case 'x':
        case 'y':
        case 'z':
        case '{':
        case '|':
        case '}':
        case '~':
        	{
        		alt3=3;
        	}
            break;
        case '\\':
        	{
        		switch ( LA(2) )
        		{
        		case '"':
        			{
        				alt3=4;
        			}
        		    break;
        		case '\\':
        			{
        				alt3=5;
        			}
        		    break;

        		default:
        		    CONSTRUCTEX();
        		    EXCEPTION->type         = ANTLR3_NO_VIABLE_ALT_EXCEPTION;
        		    EXCEPTION->message      = (void *)"";
        		    EXCEPTION->decisionNum  = 3;
        		    EXCEPTION->state        = 4;


        		    goto ruleDO_CHAREx;

        		}

        	}
            break;

        default:
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_NO_VIABLE_ALT_EXCEPTION;
            EXCEPTION->message      = (void *)"";
            EXCEPTION->decisionNum  = 3;
            EXCEPTION->state        = 0;


            goto ruleDO_CHAREx;

        }

        switch (alt3)
        {
    	case 1:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1680:20: ' ' .. '!'
    	    {
    	        MATCHRANGE(' ', '!');
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleDO_CHAREx;
    	        }


    	    }
    	    break;
    	case 2:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1680:30: '#' .. '['
    	    {
    	        MATCHRANGE('#', '[');
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleDO_CHAREx;
    	        }


    	    }
    	    break;
    	case 3:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1680:41: ']' .. '~'
    	    {
    	        MATCHRANGE(']', '~');
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleDO_CHAREx;
    	        }


    	    }
    	    break;
    	case 4:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1680:52: '\\\\\"'
    	    {
    	        MATCHS(lit_53);
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleDO_CHAREx;
    	        }




    	    }
    	    break;
    	case 5:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1680:60: '\\\\\\\\'
    	    {
    	        MATCHS(lit_54);
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleDO_CHAREx;
    	        }




    	    }
    	    break;

        }
    }

    // This is where rules clean up and exit
    //
    goto ruleDO_CHAREx; /* Prevent compiler warnings */
    ruleDO_CHAREx: ;

}
// $ANTLR end DO_CHAR

//   Comes from: 1683:26: ( '\\'' LOWER_WORD '\\'' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start LOWER_WORD_SINGLE_QUOTED
 *
 * Looks to match the characters the constitute the token LOWER_WORD_SINGLE_QUOTED
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mLOWER_WORD_SINGLE_QUOTED(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = LOWER_WORD_SINGLE_QUOTED;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1683:26: ( '\\'' LOWER_WORD '\\'' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1683:28: '\\'' LOWER_WORD '\\''
    {
        MATCHC('\'');
        if  (HASEXCEPTION())
        {
            goto ruleLOWER_WORD_SINGLE_QUOTEDEx;
        }


        /* 1683:28: '\\'' LOWER_WORD '\\'' */
        mLOWER_WORD(ctx );
        if  (HASEXCEPTION())
        {
            goto ruleLOWER_WORD_SINGLE_QUOTEDEx;
        }



        MATCHC('\'');
        if  (HASEXCEPTION())
        {
            goto ruleLOWER_WORD_SINGLE_QUOTEDEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleLOWER_WORD_SINGLE_QUOTEDEx; /* Prevent compiler warnings */
    ruleLOWER_WORD_SINGLE_QUOTEDEx: ;

}
// $ANTLR end LOWER_WORD_SINGLE_QUOTED

//   Comes from: 1684:15: ( '\\'' ( SQ_CHAR )* '\\'' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start SINGLE_QUOTED
 *
 * Looks to match the characters the constitute the token SINGLE_QUOTED
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mSINGLE_QUOTED(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = SINGLE_QUOTED;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1684:15: ( '\\'' ( SQ_CHAR )* '\\'' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1684:17: '\\'' ( SQ_CHAR )* '\\''
    {
        MATCHC('\'');
        if  (HASEXCEPTION())
        {
            goto ruleSINGLE_QUOTEDEx;
        }


        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1684:22: ( SQ_CHAR )*

        for (;;)
        {
            int alt4=2;
            switch ( LA(1) )
            {
            case ' ':
            case '!':
            case '"':
            case '#':
            case '$':
            case '%':
            case '&':
            case '(':
            case ')':
            case '*':
            case '+':
            case ',':
            case '-':
            case '.':
            case '/':
            case '0':
            case '1':
            case '2':
            case '3':
            case '4':
            case '5':
            case '6':
            case '7':
            case '8':
            case '9':
            case ':':
            case ';':
            case '<':
            case '=':
            case '>':
            case '?':
            case '@':
            case 'A':
            case 'B':
            case 'C':
            case 'D':
            case 'E':
            case 'F':
            case 'G':
            case 'H':
            case 'I':
            case 'J':
            case 'K':
            case 'L':
            case 'M':
            case 'N':
            case 'O':
            case 'P':
            case 'Q':
            case 'R':
            case 'S':
            case 'T':
            case 'U':
            case 'V':
            case 'W':
            case 'X':
            case 'Y':
            case 'Z':
            case '[':
            case '\\':
            case ']':
            case '^':
            case '_':
            case '`':
            case 'a':
            case 'b':
            case 'c':
            case 'd':
            case 'e':
            case 'f':
            case 'g':
            case 'h':
            case 'i':
            case 'j':
            case 'k':
            case 'l':
            case 'm':
            case 'n':
            case 'o':
            case 'p':
            case 'q':
            case 'r':
            case 's':
            case 't':
            case 'u':
            case 'v':
            case 'w':
            case 'x':
            case 'y':
            case 'z':
            case '{':
            case '|':
            case '}':
            case '~':
            	{
            		alt4=1;
            	}
                break;

            }

            switch (alt4)
            {
        	case 1:
        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1684:23: SQ_CHAR
        	    {
        	        /* 1684:23: SQ_CHAR */
        	        mSQ_CHAR(ctx );
        	        if  (HASEXCEPTION())
        	        {
        	            goto ruleSINGLE_QUOTEDEx;
        	        }



        	    }
        	    break;

        	default:
        	    goto loop4;	/* break out of the loop */
        	    break;
            }
        }
        loop4: ; /* Jump out to here if this rule does not match */


        MATCHC('\'');
        if  (HASEXCEPTION())
        {
            goto ruleSINGLE_QUOTEDEx;
        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleSINGLE_QUOTEDEx; /* Prevent compiler warnings */
    ruleSINGLE_QUOTEDEx: ;

}
// $ANTLR end SINGLE_QUOTED

//   Comes from: 1686:18: ( ' ' .. '&' | '(' .. '[' | ']' .. '~' | '\\\\\\'' | '\\\\\\\\' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start SQ_CHAR
 *
 * Looks to match the characters the constitute the token SQ_CHAR
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mSQ_CHAR(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    {
        //  /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1686:18: ( ' ' .. '&' | '(' .. '[' | ']' .. '~' | '\\\\\\'' | '\\\\\\\\' )

        ANTLR3_UINT32 alt5;

        alt5=5;

        switch ( LA(1) )
        {
        case ' ':
        case '!':
        case '"':
        case '#':
        case '$':
        case '%':
        case '&':
        	{
        		alt5=1;
        	}
            break;
        case '(':
        case ')':
        case '*':
        case '+':
        case ',':
        case '-':
        case '.':
        case '/':
        case '0':
        case '1':
        case '2':
        case '3':
        case '4':
        case '5':
        case '6':
        case '7':
        case '8':
        case '9':
        case ':':
        case ';':
        case '<':
        case '=':
        case '>':
        case '?':
        case '@':
        case 'A':
        case 'B':
        case 'C':
        case 'D':
        case 'E':
        case 'F':
        case 'G':
        case 'H':
        case 'I':
        case 'J':
        case 'K':
        case 'L':
        case 'M':
        case 'N':
        case 'O':
        case 'P':
        case 'Q':
        case 'R':
        case 'S':
        case 'T':
        case 'U':
        case 'V':
        case 'W':
        case 'X':
        case 'Y':
        case 'Z':
        case '[':
        	{
        		alt5=2;
        	}
            break;
        case ']':
        case '^':
        case '_':
        case '`':
        case 'a':
        case 'b':
        case 'c':
        case 'd':
        case 'e':
        case 'f':
        case 'g':
        case 'h':
        case 'i':
        case 'j':
        case 'k':
        case 'l':
        case 'm':
        case 'n':
        case 'o':
        case 'p':
        case 'q':
        case 'r':
        case 's':
        case 't':
        case 'u':
        case 'v':
        case 'w':
        case 'x':
        case 'y':
        case 'z':
        case '{':
        case '|':
        case '}':
        case '~':
        	{
        		alt5=3;
        	}
            break;
        case '\\':
        	{
        		switch ( LA(2) )
        		{
        		case '\'':
        			{
        				alt5=4;
        			}
        		    break;
        		case '\\':
        			{
        				alt5=5;
        			}
        		    break;

        		default:
        		    CONSTRUCTEX();
        		    EXCEPTION->type         = ANTLR3_NO_VIABLE_ALT_EXCEPTION;
        		    EXCEPTION->message      = (void *)"";
        		    EXCEPTION->decisionNum  = 5;
        		    EXCEPTION->state        = 4;


        		    goto ruleSQ_CHAREx;

        		}

        	}
            break;

        default:
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_NO_VIABLE_ALT_EXCEPTION;
            EXCEPTION->message      = (void *)"";
            EXCEPTION->decisionNum  = 5;
            EXCEPTION->state        = 0;


            goto ruleSQ_CHAREx;

        }

        switch (alt5)
        {
    	case 1:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1686:20: ' ' .. '&'
    	    {
    	        MATCHRANGE(' ', '&');
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleSQ_CHAREx;
    	        }


    	    }
    	    break;
    	case 2:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1686:31: '(' .. '['
    	    {
    	        MATCHRANGE('(', '[');
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleSQ_CHAREx;
    	        }


    	    }
    	    break;
    	case 3:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1686:42: ']' .. '~'
    	    {
    	        MATCHRANGE(']', '~');
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleSQ_CHAREx;
    	        }


    	    }
    	    break;
    	case 4:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1686:53: '\\\\\\''
    	    {
    	        MATCHS(lit_55);
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleSQ_CHAREx;
    	        }




    	    }
    	    break;
    	case 5:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1686:62: '\\\\\\\\'
    	    {
    	        MATCHS(lit_54);
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleSQ_CHAREx;
    	        }




    	    }
    	    break;

        }
    }

    // This is where rules clean up and exit
    //
    goto ruleSQ_CHAREx; /* Prevent compiler warnings */
    ruleSQ_CHAREx: ;

}
// $ANTLR end SQ_CHAR

//   Comes from: 1689:18: ( '0' .. '9' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start NUMERIC
 *
 * Looks to match the characters the constitute the token NUMERIC
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mNUMERIC(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1689:18: ( '0' .. '9' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
    {
        if ( ((LA(1) >= '0') && (LA(1) <= '9')) )
        {
            CONSUME();
        }
        else
        {
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

            LRECOVER();
            goto ruleNUMERICEx;
        }


    }


    // This is where rules clean up and exit
    //
    goto ruleNUMERICEx; /* Prevent compiler warnings */
    ruleNUMERICEx: ;

}
// $ANTLR end NUMERIC

//   Comes from: 1690:22: ( 'a' .. 'z' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start LOWER_ALPHA
 *
 * Looks to match the characters the constitute the token LOWER_ALPHA
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mLOWER_ALPHA(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1690:22: ( 'a' .. 'z' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
    {
        if ( ((LA(1) >= 'a') && (LA(1) <= 'z')) )
        {
            CONSUME();
        }
        else
        {
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

            LRECOVER();
            goto ruleLOWER_ALPHAEx;
        }


    }


    // This is where rules clean up and exit
    //
    goto ruleLOWER_ALPHAEx; /* Prevent compiler warnings */
    ruleLOWER_ALPHAEx: ;

}
// $ANTLR end LOWER_ALPHA

//   Comes from: 1691:22: ( 'A' .. 'Z' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start UPPER_ALPHA
 *
 * Looks to match the characters the constitute the token UPPER_ALPHA
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mUPPER_ALPHA(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1691:22: ( 'A' .. 'Z' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
    {
        if ( ((LA(1) >= 'A') && (LA(1) <= 'Z')) )
        {
            CONSUME();
        }
        else
        {
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

            LRECOVER();
            goto ruleUPPER_ALPHAEx;
        }


    }


    // This is where rules clean up and exit
    //
    goto ruleUPPER_ALPHAEx; /* Prevent compiler warnings */
    ruleUPPER_ALPHAEx: ;

}
// $ANTLR end UPPER_ALPHA

//   Comes from: 1692:24: ( LOWER_ALPHA | UPPER_ALPHA | NUMERIC | '_' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start ALPHA_NUMERIC
 *
 * Looks to match the characters the constitute the token ALPHA_NUMERIC
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mALPHA_NUMERIC(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1692:24: ( LOWER_ALPHA | UPPER_ALPHA | NUMERIC | '_' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
    {
        if ( ((LA(1) >= '0') && (LA(1) <= '9')) || ((LA(1) >= 'A') && (LA(1) <= 'Z')) || LA(1) == '_' || ((LA(1) >= 'a') && (LA(1) <= 'z')) )
        {
            CONSUME();
        }
        else
        {
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

            LRECOVER();
            goto ruleALPHA_NUMERICEx;
        }


    }


    // This is where rules clean up and exit
    //
    goto ruleALPHA_NUMERICEx; /* Prevent compiler warnings */
    ruleALPHA_NUMERICEx: ;

}
// $ANTLR end ALPHA_NUMERIC

//   Comes from: 1693:12: ( UPPER_ALPHA ( ALPHA_NUMERIC )* )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start UPPER_WORD
 *
 * Looks to match the characters the constitute the token UPPER_WORD
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mUPPER_WORD(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = UPPER_WORD;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1693:12: ( UPPER_ALPHA ( ALPHA_NUMERIC )* )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1693:14: UPPER_ALPHA ( ALPHA_NUMERIC )*
    {
        /* 1693:14: UPPER_ALPHA ( ALPHA_NUMERIC )* */
        mUPPER_ALPHA(ctx );
        if  (HASEXCEPTION())
        {
            goto ruleUPPER_WORDEx;
        }



        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1693:26: ( ALPHA_NUMERIC )*

        for (;;)
        {
            int alt6=2;
            switch ( LA(1) )
            {
            case '0':
            case '1':
            case '2':
            case '3':
            case '4':
            case '5':
            case '6':
            case '7':
            case '8':
            case '9':
            case 'A':
            case 'B':
            case 'C':
            case 'D':
            case 'E':
            case 'F':
            case 'G':
            case 'H':
            case 'I':
            case 'J':
            case 'K':
            case 'L':
            case 'M':
            case 'N':
            case 'O':
            case 'P':
            case 'Q':
            case 'R':
            case 'S':
            case 'T':
            case 'U':
            case 'V':
            case 'W':
            case 'X':
            case 'Y':
            case 'Z':
            case '_':
            case 'a':
            case 'b':
            case 'c':
            case 'd':
            case 'e':
            case 'f':
            case 'g':
            case 'h':
            case 'i':
            case 'j':
            case 'k':
            case 'l':
            case 'm':
            case 'n':
            case 'o':
            case 'p':
            case 'q':
            case 'r':
            case 's':
            case 't':
            case 'u':
            case 'v':
            case 'w':
            case 'x':
            case 'y':
            case 'z':
            	{
            		alt6=1;
            	}
                break;

            }

            switch (alt6)
            {
        	case 1:
        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
        	    {
        	        if ( ((LA(1) >= '0') && (LA(1) <= '9')) || ((LA(1) >= 'A') && (LA(1) <= 'Z')) || LA(1) == '_' || ((LA(1) >= 'a') && (LA(1) <= 'z')) )
        	        {
        	            CONSUME();
        	        }
        	        else
        	        {
        	            CONSTRUCTEX();
        	            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
        	            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

        	            LRECOVER();
        	            goto ruleUPPER_WORDEx;
        	        }


        	    }
        	    break;

        	default:
        	    goto loop6;	/* break out of the loop */
        	    break;
            }
        }
        loop6: ; /* Jump out to here if this rule does not match */


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleUPPER_WORDEx; /* Prevent compiler warnings */
    ruleUPPER_WORDEx: ;

}
// $ANTLR end UPPER_WORD

//   Comes from: 1694:12: ( LOWER_ALPHA ( ALPHA_NUMERIC )* )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start LOWER_WORD
 *
 * Looks to match the characters the constitute the token LOWER_WORD
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mLOWER_WORD(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = LOWER_WORD;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1694:12: ( LOWER_ALPHA ( ALPHA_NUMERIC )* )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1694:14: LOWER_ALPHA ( ALPHA_NUMERIC )*
    {
        /* 1694:14: LOWER_ALPHA ( ALPHA_NUMERIC )* */
        mLOWER_ALPHA(ctx );
        if  (HASEXCEPTION())
        {
            goto ruleLOWER_WORDEx;
        }



        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1694:26: ( ALPHA_NUMERIC )*

        for (;;)
        {
            int alt7=2;
            switch ( LA(1) )
            {
            case '0':
            case '1':
            case '2':
            case '3':
            case '4':
            case '5':
            case '6':
            case '7':
            case '8':
            case '9':
            case 'A':
            case 'B':
            case 'C':
            case 'D':
            case 'E':
            case 'F':
            case 'G':
            case 'H':
            case 'I':
            case 'J':
            case 'K':
            case 'L':
            case 'M':
            case 'N':
            case 'O':
            case 'P':
            case 'Q':
            case 'R':
            case 'S':
            case 'T':
            case 'U':
            case 'V':
            case 'W':
            case 'X':
            case 'Y':
            case 'Z':
            case '_':
            case 'a':
            case 'b':
            case 'c':
            case 'd':
            case 'e':
            case 'f':
            case 'g':
            case 'h':
            case 'i':
            case 'j':
            case 'k':
            case 'l':
            case 'm':
            case 'n':
            case 'o':
            case 'p':
            case 'q':
            case 'r':
            case 's':
            case 't':
            case 'u':
            case 'v':
            case 'w':
            case 'x':
            case 'y':
            case 'z':
            	{
            		alt7=1;
            	}
                break;

            }

            switch (alt7)
            {
        	case 1:
        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
        	    {
        	        if ( ((LA(1) >= '0') && (LA(1) <= '9')) || ((LA(1) >= 'A') && (LA(1) <= 'Z')) || LA(1) == '_' || ((LA(1) >= 'a') && (LA(1) <= 'z')) )
        	        {
        	            CONSUME();
        	        }
        	        else
        	        {
        	            CONSTRUCTEX();
        	            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
        	            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

        	            LRECOVER();
        	            goto ruleLOWER_WORDEx;
        	        }


        	    }
        	    break;

        	default:
        	    goto loop7;	/* break out of the loop */
        	    break;
            }
        }
        loop7: ; /* Jump out to here if this rule does not match */


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleLOWER_WORDEx; /* Prevent compiler warnings */
    ruleLOWER_WORDEx: ;

}
// $ANTLR end LOWER_WORD

//   Comes from: 1731:27: ( '.' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DOT
 *
 * Looks to match the characters the constitute the token DOT
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDOT(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1731:27: ( '.' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1731:29: '.'
    {
        MATCHC('.');
        if  (HASEXCEPTION())
        {
            goto ruleDOTEx;
        }


    }


    // This is where rules clean up and exit
    //
    goto ruleDOTEx; /* Prevent compiler warnings */
    ruleDOTEx: ;

}
// $ANTLR end DOT

//   Comes from: 1729:27: ( 'E' | 'e' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start EXPONENT
 *
 * Looks to match the characters the constitute the token EXPONENT
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mEXPONENT(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1729:27: ( 'E' | 'e' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
    {
        if ( LA(1) == 'E' || LA(1) == 'e' )
        {
            CONSUME();
        }
        else
        {
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

            LRECOVER();
            goto ruleEXPONENTEx;
        }


    }


    // This is where rules clean up and exit
    //
    goto ruleEXPONENTEx; /* Prevent compiler warnings */
    ruleEXPONENTEx: ;

}
// $ANTLR end EXPONENT

//   Comes from: 1730:27: ( '/' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start SLASH
 *
 * Looks to match the characters the constitute the token SLASH
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mSLASH(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1730:27: ( '/' )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1730:29: '/'
    {
        MATCHC('/');
        if  (HASEXCEPTION())
        {
            goto ruleSLASHEx;
        }


    }


    // This is where rules clean up and exit
    //
    goto ruleSLASHEx; /* Prevent compiler warnings */
    ruleSLASHEx: ;

}
// $ANTLR end SLASH

//   Comes from: 1732:18: ( ( NUMERIC )+ )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start DECIMAL
 *
 * Looks to match the characters the constitute the token DECIMAL
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mDECIMAL(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1732:18: ( ( NUMERIC )+ )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1732:20: ( NUMERIC )+
    {
        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1732:20: ( NUMERIC )+
        {
            int cnt8=0;

            for (;;)
            {
                int alt8=2;
        	switch ( LA(1) )
        	{
        	case '0':
        	case '1':
        	case '2':
        	case '3':
        	case '4':
        	case '5':
        	case '6':
        	case '7':
        	case '8':
        	case '9':
        		{
        			alt8=1;
        		}
        	    break;

        	}

        	switch (alt8)
        	{
        	    case 1:
        	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
        	        {
        	            if ( ((LA(1) >= '0') && (LA(1) <= '9')) )
        	            {
        	                CONSUME();
        	            }
        	            else
        	            {
        	                CONSTRUCTEX();
        	                EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
        	                EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

        	                LRECOVER();
        	                goto ruleDECIMALEx;
        	            }


        	        }
        	        break;

        	    default:

        		if ( cnt8 >= 1 )
        		{
        		    goto loop8;
        		}
        		/* mismatchedSetEx()
        		 */
        		CONSTRUCTEX();
        		EXCEPTION->type = ANTLR3_EARLY_EXIT_EXCEPTION;
        		EXCEPTION->name = (void *)ANTLR3_EARLY_EXIT_NAME;


        		goto ruleDECIMALEx;
        	}
        	cnt8++;
            }
            loop8: ;	/* Jump to here if this rule does not match */
        }

    }


    // This is where rules clean up and exit
    //
    goto ruleDECIMALEx; /* Prevent compiler warnings */
    ruleDECIMALEx: ;

}
// $ANTLR end DECIMAL

//   Comes from: 1736:3: ( PLUS_TOK | MINUS_TOK )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start SIGN
 *
 * Looks to match the characters the constitute the token SIGN
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mSIGN(pTptpLexer ctx, bool& pos)
{
	ANTLR3_UINT32	_type;


    {
        //  /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1736:3: ( PLUS_TOK | MINUS_TOK )

        ANTLR3_UINT32 alt9;

        alt9=2;

        switch ( LA(1) )
        {
        case '+':
        	{
        		alt9=1;
        	}
            break;
        case '-':
        	{
        		alt9=2;
        	}
            break;

        default:
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_NO_VIABLE_ALT_EXCEPTION;
            EXCEPTION->message      = (void *)"";
            EXCEPTION->decisionNum  = 9;
            EXCEPTION->state        = 0;


            goto ruleSIGNEx;

        }

        switch (alt9)
        {
    	case 1:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1736:5: PLUS_TOK
    	    {
    	        /* 1736:5: PLUS_TOK */
    	        mPLUS_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleSIGNEx;
    	        }



    	        {
    	             pos = true;
    	        }


    	    }
    	    break;
    	case 2:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1737:5: MINUS_TOK
    	    {
    	        /* 1737:5: MINUS_TOK */
    	        mMINUS_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleSIGNEx;
    	        }



    	        {
    	             pos = false;
    	        }


    	    }
    	    break;

        }
    }

    // This is where rules clean up and exit
    //
    goto ruleSIGNEx; /* Prevent compiler warnings */
    ruleSIGNEx: ;

}
// $ANTLR end SIGN

//   Comes from: 1745:3: ( ( ( SIGN[pos] )? num= DECIMAL | ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? | ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL ) )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start NUMBER
 *
 * Looks to match the characters the constitute the token NUMBER
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mNUMBER(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

      bool pos = true;
      bool posE = true;

    pANTLR3_COMMON_TOKEN num;
    pANTLR3_COMMON_TOKEN den;
    pANTLR3_COMMON_TOKEN e;


    num = NULL;
    den = NULL;
    e = NULL;

    _type	    = NUMBER;


    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1745:3: ( ( ( SIGN[pos] )? num= DECIMAL | ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? | ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL ) )
    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1745:5: ( ( SIGN[pos] )? num= DECIMAL | ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? | ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL )
    {
        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1745:5: ( ( SIGN[pos] )? num= DECIMAL | ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? | ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL )
        {
            int alt15=3;
            alt15 = cdfa15.predict(ctx, RECOGNIZER, ISTREAM, &cdfa15);
            if  (HASEXCEPTION())
            {
                goto ruleNUMBEREx;
            }

            switch (alt15)
            {
        	case 1:
        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1745:7: ( SIGN[pos] )? num= DECIMAL
        	    {
        	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1745:7: ( SIGN[pos] )?
        	        {
        	            int alt10=2;
        	            switch ( LA(1) )
        	            {
        	                case '+':
        	                case '-':
        	                	{
        	                		alt10=1;
        	                	}
        	                    break;
        	            }

        	            switch (alt10)
        	            {
        	        	case 1:
        	        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1745:7: SIGN[pos]
        	        	    {
        	        	        /* 1745:7: SIGN[pos] */
        	        	        mSIGN(ctx , pos);
        	        	        if  (HASEXCEPTION())
        	        	        {
        	        	            goto ruleNUMBEREx;
        	        	        }



        	        	    }
        	        	    break;

        	            }
        	        }

        	        /* 1745:7: ( SIGN[pos] )? num= DECIMAL */
        	        {
        	            ANTLR3_MARKER numStart1051 = GETCHARINDEX();
        	        mDECIMAL(ctx );
        	            if  (HASEXCEPTION())
        	            {
        	                goto ruleNUMBEREx;
        	            }

        	            num = LEXSTATE->tokFactory->newToken(LEXSTATE->tokFactory);
        	            num->setType(num, ANTLR3_TOKEN_INVALID);
        	            num->setStartIndex(num, numStart1051);
        	            num->setStopIndex(num, GETCHARINDEX()-1);
        	            num->input = INPUT;
        	        }


        	        {
        	             std::stringstream ss;
        	                    ss << ( pos ? "" : "-" ) << AntlrInput::tokenText(num);
        	                    std::string str = ss.str();
        	                    if (str.find(".") == std::string::npos)
        	                    {
        	                      PARSER_STATE->d_tmp_expr = SOLVER->mkInteger(str);
        	                    }
        	                    else
        	                    {
        	                      PARSER_STATE->d_tmp_expr = SOLVER->mkReal(str);
        	                    }

        	        }


        	    }
        	    break;
        	case 2:
        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1758:7: ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )?
        	    {
        	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1758:7: ( SIGN[pos] )?
        	        {
        	            int alt11=2;
        	            switch ( LA(1) )
        	            {
        	                case '+':
        	                case '-':
        	                	{
        	                		alt11=1;
        	                	}
        	                    break;
        	            }

        	            switch (alt11)
        	            {
        	        	case 1:
        	        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1758:7: SIGN[pos]
        	        	    {
        	        	        /* 1758:7: SIGN[pos] */
        	        	        mSIGN(ctx , pos);
        	        	        if  (HASEXCEPTION())
        	        	        {
        	        	            goto ruleNUMBEREx;
        	        	        }



        	        	    }
        	        	    break;

        	            }
        	        }

        	        /* 1758:7: ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? */
        	        {
        	            ANTLR3_MARKER numStart1073 = GETCHARINDEX();
        	        mDECIMAL(ctx );
        	            if  (HASEXCEPTION())
        	            {
        	                goto ruleNUMBEREx;
        	            }

        	            num = LEXSTATE->tokFactory->newToken(LEXSTATE->tokFactory);
        	            num->setType(num, ANTLR3_TOKEN_INVALID);
        	            num->setStartIndex(num, numStart1073);
        	            num->setStopIndex(num, GETCHARINDEX()-1);
        	            num->input = INPUT;
        	        }


        	        /* 1758:7: ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? */
        	        mDOT(ctx );
        	        if  (HASEXCEPTION())
        	        {
        	            goto ruleNUMBEREx;
        	        }



        	        /* 1758:7: ( SIGN[pos] )? num= DECIMAL DOT den= DECIMAL ( EXPONENT ( SIGN[posE] )? e= DECIMAL )? */
        	        {
        	            ANTLR3_MARKER denStart1079 = GETCHARINDEX();
        	        mDECIMAL(ctx );
        	            if  (HASEXCEPTION())
        	            {
        	                goto ruleNUMBEREx;
        	            }

        	            den = LEXSTATE->tokFactory->newToken(LEXSTATE->tokFactory);
        	            den->setType(den, ANTLR3_TOKEN_INVALID);
        	            den->setStartIndex(den, denStart1079);
        	            den->setStopIndex(den, GETCHARINDEX()-1);
        	            den->input = INPUT;
        	        }


        	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1758:46: ( EXPONENT ( SIGN[posE] )? e= DECIMAL )?
        	        {
        	            int alt13=2;
        	            switch ( LA(1) )
        	            {
        	                case 'E':
        	                case 'e':
        	                	{
        	                		alt13=1;
        	                	}
        	                    break;
        	            }

        	            switch (alt13)
        	            {
        	        	case 1:
        	        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1758:47: EXPONENT ( SIGN[posE] )? e= DECIMAL
        	        	    {
        	        	        /* 1758:47: EXPONENT ( SIGN[posE] )? e= DECIMAL */
        	        	        mEXPONENT(ctx );
        	        	        if  (HASEXCEPTION())
        	        	        {
        	        	            goto ruleNUMBEREx;
        	        	        }



        	        	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1758:56: ( SIGN[posE] )?
        	        	        {
        	        	            int alt12=2;
        	        	            switch ( LA(1) )
        	        	            {
        	        	                case '+':
        	        	                case '-':
        	        	                	{
        	        	                		alt12=1;
        	        	                	}
        	        	                    break;
        	        	            }

        	        	            switch (alt12)
        	        	            {
        	        	        	case 1:
        	        	        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1758:56: SIGN[posE]
        	        	        	    {
        	        	        	        /* 1758:56: SIGN[posE] */
        	        	        	        mSIGN(ctx , posE);
        	        	        	        if  (HASEXCEPTION())
        	        	        	        {
        	        	        	            goto ruleNUMBEREx;
        	        	        	        }



        	        	        	    }
        	        	        	    break;

        	        	            }
        	        	        }

        	        	        /* 1758:47: EXPONENT ( SIGN[posE] )? e= DECIMAL */
        	        	        {
        	        	            ANTLR3_MARKER eStart1090 = GETCHARINDEX();
        	        	        mDECIMAL(ctx );
        	        	            if  (HASEXCEPTION())
        	        	            {
        	        	                goto ruleNUMBEREx;
        	        	            }

        	        	            e = LEXSTATE->tokFactory->newToken(LEXSTATE->tokFactory);
        	        	            e->setType(e, ANTLR3_TOKEN_INVALID);
        	        	            e->setStartIndex(e, eStart1090);
        	        	            e->setStopIndex(e, GETCHARINDEX()-1);
        	        	            e->input = INPUT;
        	        	        }


        	        	    }
        	        	    break;

        	            }
        	        }

        	        {

        	                    std::string snum = AntlrInput::tokenText(num);
        	                    std::string sden = AntlrInput::tokenText(den);
        	                    size_t exp = (e == NULL ? 0 : AntlrInput::tokenToUnsigned(e));
        	                    PARSER_STATE->d_tmp_expr = PARSER_STATE->mkDecimal(snum, sden, pos, exp, posE);

        	        }


        	    }
        	    break;
        	case 3:
        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1765:7: ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL
        	    {
        	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1765:7: ( SIGN[pos] )?
        	        {
        	            int alt14=2;
        	            switch ( LA(1) )
        	            {
        	                case '+':
        	                case '-':
        	                	{
        	                		alt14=1;
        	                	}
        	                    break;
        	            }

        	            switch (alt14)
        	            {
        	        	case 1:
        	        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1765:7: SIGN[pos]
        	        	    {
        	        	        /* 1765:7: SIGN[pos] */
        	        	        mSIGN(ctx , pos);
        	        	        if  (HASEXCEPTION())
        	        	        {
        	        	            goto ruleNUMBEREx;
        	        	        }



        	        	    }
        	        	    break;

        	            }
        	        }

        	        /* 1765:7: ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL */
        	        {
        	            ANTLR3_MARKER numStart1114 = GETCHARINDEX();
        	        mDECIMAL(ctx );
        	            if  (HASEXCEPTION())
        	            {
        	                goto ruleNUMBEREx;
        	            }

        	            num = LEXSTATE->tokFactory->newToken(LEXSTATE->tokFactory);
        	            num->setType(num, ANTLR3_TOKEN_INVALID);
        	            num->setStartIndex(num, numStart1114);
        	            num->setStopIndex(num, GETCHARINDEX()-1);
        	            num->input = INPUT;
        	        }


        	        /* 1765:7: ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL */
        	        mSLASH(ctx );
        	        if  (HASEXCEPTION())
        	        {
        	            goto ruleNUMBEREx;
        	        }



        	        /* 1765:7: ( SIGN[pos] )? num= DECIMAL SLASH den= DECIMAL */
        	        {
        	            ANTLR3_MARKER denStart1120 = GETCHARINDEX();
        	        mDECIMAL(ctx );
        	            if  (HASEXCEPTION())
        	            {
        	                goto ruleNUMBEREx;
        	            }

        	            den = LEXSTATE->tokFactory->newToken(LEXSTATE->tokFactory);
        	            den->setType(den, ANTLR3_TOKEN_INVALID);
        	            den->setStartIndex(den, denStart1120);
        	            den->setStopIndex(den, GETCHARINDEX()-1);
        	            den->input = INPUT;
        	        }


        	        {
        	             std::stringstream ss;
        	                    ss << ( pos ? "" : "-" );
        	                    ss << AntlrInput::tokenText(num) << "/" << AntlrInput::tokenText(den);
        	                    PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());

        	        }


        	    }
        	    break;

            }
        }

        {
             if(PARSER_STATE->cnf() || PARSER_STATE->fof()) {
                    // We're in an unsorted context, so put a conversion around it
                    PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
                  }

        }


    }

	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleNUMBEREx; /* Prevent compiler warnings */
    ruleNUMBEREx: ;

    num = NULL;
    den = NULL;
    e = NULL;

}
// $ANTLR end NUMBER

//   Comes from: 1786:3: ( '%' (~ ( '\\n' | '\\r' ) )* | '/*' ( options {greedy=false; } : . )* '*/' )
/** \brief Lexer rule generated by ANTLR3
 *
 * $ANTLR start COMMENT
 *
 * Looks to match the characters the constitute the token COMMENT
 * from the attached input stream.
 *
 *
 * \remark
 *  - lexer->error == ANTLR3_TRUE if an exception was thrown.
 */
static ANTLR3_INLINE
void mCOMMENT(pTptpLexer ctx)
{
	ANTLR3_UINT32	_type;

    _type	    = COMMENT;


    {
        //  /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1786:3: ( '%' (~ ( '\\n' | '\\r' ) )* | '/*' ( options {greedy=false; } : . )* '*/' )

        ANTLR3_UINT32 alt18;

        alt18=2;

        switch ( LA(1) )
        {
        case '%':
        	{
        		alt18=1;
        	}
            break;
        case '/':
        	{
        		alt18=2;
        	}
            break;

        default:
            CONSTRUCTEX();
            EXCEPTION->type         = ANTLR3_NO_VIABLE_ALT_EXCEPTION;
            EXCEPTION->message      = (void *)"";
            EXCEPTION->decisionNum  = 18;
            EXCEPTION->state        = 0;


            goto ruleCOMMENTEx;

        }

        switch (alt18)
        {
    	case 1:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1786:5: '%' (~ ( '\\n' | '\\r' ) )*
    	    {
    	        MATCHC('%');
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleCOMMENTEx;
    	        }


    	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1786:9: (~ ( '\\n' | '\\r' ) )*

    	        for (;;)
    	        {
    	            int alt16=2;
    	            {
    	               /* dfaLoopbackState(k,edges,eotPredictsAlt,description,stateNumber,semPredState)
    	                */
    	                int LA16_0 = LA(1);
    	                if ( (((LA16_0 >= 0x0000) && (LA16_0 <= '\t')) || ((LA16_0 >= 0x000B) && (LA16_0 <= '\f')) || ((LA16_0 >= 0x000E) && (LA16_0 <= 0xFFFF))))
    	                {
    	                    alt16=1;
    	                }

    	            }
    	            switch (alt16)
    	            {
    	        	case 1:
    	        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:
    	        	    {
    	        	        if ( ((LA(1) >= 0x0000) && (LA(1) <= '\t')) || ((LA(1) >= 0x000B) && (LA(1) <= '\f')) || ((LA(1) >= 0x000E) && (LA(1) <= 0xFFFF)) )
    	        	        {
    	        	            CONSUME();
    	        	        }
    	        	        else
    	        	        {
    	        	            CONSTRUCTEX();
    	        	            EXCEPTION->type         = ANTLR3_MISMATCHED_SET_EXCEPTION;
    	        	            EXCEPTION->name         = (void *)ANTLR3_MISMATCHED_SET_NAME;

    	        	            LRECOVER();
    	        	            goto ruleCOMMENTEx;
    	        	        }


    	        	    }
    	        	    break;

    	        	default:
    	        	    goto loop16;	/* break out of the loop */
    	        	    break;
    	            }
    	        }
    	        loop16: ; /* Jump out to here if this rule does not match */


    	        {
    	             SKIP();
    	        }


    	    }
    	    break;
    	case 2:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1787:5: '/*' ( options {greedy=false; } : . )* '*/'
    	    {
    	        MATCHS(lit_56);
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleCOMMENTEx;
    	        }




    	        // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1787:11: ( options {greedy=false; } : . )*

    	        for (;;)
    	        {
    	            int alt17=2;
    	            {
    	               /* dfaLoopbackState(k,edges,eotPredictsAlt,description,stateNumber,semPredState)
    	                */
    	                int LA17_0 = LA(1);
    	                if ( (LA17_0 == '*'))
    	                {
    	                    {
    	                       /* dfaLoopbackState(k,edges,eotPredictsAlt,description,stateNumber,semPredState)
    	                        */
    	                        int LA17_1 = LA(2);
    	                        if ( (LA17_1 == '/'))
    	                        {
    	                            alt17=2;
    	                        }
    	                        else if ( (((LA17_1 >= 0x0000) && (LA17_1 <= '.')) || ((LA17_1 >= '0') && (LA17_1 <= 0xFFFF))))
    	                        {
    	                            alt17=1;
    	                        }

    	                    }
    	                }
    	                else if ( (((LA17_0 >= 0x0000) && (LA17_0 <= ')')) || ((LA17_0 >= '+') && (LA17_0 <= 0xFFFF))))
    	                {
    	                    alt17=1;
    	                }

    	            }
    	            switch (alt17)
    	            {
    	        	case 1:
    	        	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1787:39: .
    	        	    {
    	        	        MATCHANY();
    	        	        if  (HASEXCEPTION())
    	        	        {
    	        	            goto ruleCOMMENTEx;
    	        	        }


    	        	    }
    	        	    break;

    	        	default:
    	        	    goto loop17;	/* break out of the loop */
    	        	    break;
    	            }
    	        }
    	        loop17: ; /* Jump out to here if this rule does not match */


    	        MATCHS(lit_57);
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleCOMMENTEx;
    	        }




    	        {
    	             SKIP();
    	        }


    	    }
    	    break;

        }
    }
	LEXSTATE->type = _type;
    // This is where rules clean up and exit
    //
    goto ruleCOMMENTEx; /* Prevent compiler warnings */
    ruleCOMMENTEx: ;

}
// $ANTLR end COMMENT

/** This is the entry point in to the lexer from an object that
 *  wants to generate the next token, such as a pCOMMON_TOKEN_STREAM
 */
static void
mTokens(pTptpLexer ctx)
{
    {
        //  /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:8: ( T__63 | T__64 | T__65 | T__66 | T__67 | T__68 | T__69 | T__70 | T__71 | T__72 | T__73 | T__74 | T__75 | T__76 | T__77 | T__78 | T__79 | T__80 | T__81 | T__82 | T__83 | T__84 | T__85 | T__86 | T__87 | T__88 | T__89 | T__90 | T__91 | T__92 | T__93 | T__94 | COMMA_TOK | DOT_TOK | LPAREN_TOK | RPAREN_TOK | LBRACK_TOK | RBRACK_TOK | COLON_TOK | ARROW_TOK | SUBTYPE_TOK | OR_TOK | NOT_TOK | FORALL_TOK | EXISTS_TOK | LAMBDA_TOK | CHOICE_TOK | DEF_DESC_TOK | AND_TOK | IFF_TOK | IMPLIES_TOK | REVIMPLIES_TOK | REVIFF_TOK | REVOR_TOK | REVAND_TOK | TIMES_TOK | PLUS_TOK | MINUS_TOK | APP_TOK | TH1_UN_A | TH1_UN_E | TRUE_TOK | FALSE_TOK | EQUAL_TOK | DISEQUAL_TOK | CNF_TOK | FOF_TOK | THF_TOK | TFF_TOK | TYPE_TOK | INCLUDE_TOK | DEFINED_SYMBOL | WHITESPACE | DISTINCT_OBJECT | LOWER_WORD_SINGLE_QUOTED | SINGLE_QUOTED | UPPER_WORD | LOWER_WORD | NUMBER | COMMENT )

        ANTLR3_UINT32 alt19;

        alt19=80;

        alt19 = cdfa19.predict(ctx, RECOGNIZER, ISTREAM, &cdfa19);
        if  (HASEXCEPTION())
        {
            goto ruleTokensEx;
        }

        switch (alt19)
        {
    	case 1:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:10: T__63
    	    {
    	        /* 1:10: T__63 */
    	        mT__63(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 2:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:16: T__64
    	    {
    	        /* 1:16: T__64 */
    	        mT__64(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 3:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:22: T__65
    	    {
    	        /* 1:22: T__65 */
    	        mT__65(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 4:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:28: T__66
    	    {
    	        /* 1:28: T__66 */
    	        mT__66(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 5:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:34: T__67
    	    {
    	        /* 1:34: T__67 */
    	        mT__67(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 6:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:40: T__68
    	    {
    	        /* 1:40: T__68 */
    	        mT__68(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 7:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:46: T__69
    	    {
    	        /* 1:46: T__69 */
    	        mT__69(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 8:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:52: T__70
    	    {
    	        /* 1:52: T__70 */
    	        mT__70(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 9:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:58: T__71
    	    {
    	        /* 1:58: T__71 */
    	        mT__71(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 10:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:64: T__72
    	    {
    	        /* 1:64: T__72 */
    	        mT__72(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 11:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:70: T__73
    	    {
    	        /* 1:70: T__73 */
    	        mT__73(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 12:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:76: T__74
    	    {
    	        /* 1:76: T__74 */
    	        mT__74(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 13:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:82: T__75
    	    {
    	        /* 1:82: T__75 */
    	        mT__75(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 14:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:88: T__76
    	    {
    	        /* 1:88: T__76 */
    	        mT__76(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 15:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:94: T__77
    	    {
    	        /* 1:94: T__77 */
    	        mT__77(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 16:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:100: T__78
    	    {
    	        /* 1:100: T__78 */
    	        mT__78(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 17:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:106: T__79
    	    {
    	        /* 1:106: T__79 */
    	        mT__79(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 18:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:112: T__80
    	    {
    	        /* 1:112: T__80 */
    	        mT__80(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 19:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:118: T__81
    	    {
    	        /* 1:118: T__81 */
    	        mT__81(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 20:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:124: T__82
    	    {
    	        /* 1:124: T__82 */
    	        mT__82(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 21:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:130: T__83
    	    {
    	        /* 1:130: T__83 */
    	        mT__83(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 22:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:136: T__84
    	    {
    	        /* 1:136: T__84 */
    	        mT__84(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 23:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:142: T__85
    	    {
    	        /* 1:142: T__85 */
    	        mT__85(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 24:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:148: T__86
    	    {
    	        /* 1:148: T__86 */
    	        mT__86(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 25:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:154: T__87
    	    {
    	        /* 1:154: T__87 */
    	        mT__87(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 26:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:160: T__88
    	    {
    	        /* 1:160: T__88 */
    	        mT__88(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 27:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:166: T__89
    	    {
    	        /* 1:166: T__89 */
    	        mT__89(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 28:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:172: T__90
    	    {
    	        /* 1:172: T__90 */
    	        mT__90(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 29:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:178: T__91
    	    {
    	        /* 1:178: T__91 */
    	        mT__91(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 30:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:184: T__92
    	    {
    	        /* 1:184: T__92 */
    	        mT__92(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 31:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:190: T__93
    	    {
    	        /* 1:190: T__93 */
    	        mT__93(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 32:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:196: T__94
    	    {
    	        /* 1:196: T__94 */
    	        mT__94(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 33:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:202: COMMA_TOK
    	    {
    	        /* 1:202: COMMA_TOK */
    	        mCOMMA_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 34:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:212: DOT_TOK
    	    {
    	        /* 1:212: DOT_TOK */
    	        mDOT_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 35:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:220: LPAREN_TOK
    	    {
    	        /* 1:220: LPAREN_TOK */
    	        mLPAREN_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 36:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:231: RPAREN_TOK
    	    {
    	        /* 1:231: RPAREN_TOK */
    	        mRPAREN_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 37:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:242: LBRACK_TOK
    	    {
    	        /* 1:242: LBRACK_TOK */
    	        mLBRACK_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 38:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:253: RBRACK_TOK
    	    {
    	        /* 1:253: RBRACK_TOK */
    	        mRBRACK_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 39:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:264: COLON_TOK
    	    {
    	        /* 1:264: COLON_TOK */
    	        mCOLON_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 40:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:274: ARROW_TOK
    	    {
    	        /* 1:274: ARROW_TOK */
    	        mARROW_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 41:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:284: SUBTYPE_TOK
    	    {
    	        /* 1:284: SUBTYPE_TOK */
    	        mSUBTYPE_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 42:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:296: OR_TOK
    	    {
    	        /* 1:296: OR_TOK */
    	        mOR_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 43:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:303: NOT_TOK
    	    {
    	        /* 1:303: NOT_TOK */
    	        mNOT_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 44:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:311: FORALL_TOK
    	    {
    	        /* 1:311: FORALL_TOK */
    	        mFORALL_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 45:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:322: EXISTS_TOK
    	    {
    	        /* 1:322: EXISTS_TOK */
    	        mEXISTS_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 46:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:333: LAMBDA_TOK
    	    {
    	        /* 1:333: LAMBDA_TOK */
    	        mLAMBDA_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 47:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:344: CHOICE_TOK
    	    {
    	        /* 1:344: CHOICE_TOK */
    	        mCHOICE_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 48:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:355: DEF_DESC_TOK
    	    {
    	        /* 1:355: DEF_DESC_TOK */
    	        mDEF_DESC_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 49:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:368: AND_TOK
    	    {
    	        /* 1:368: AND_TOK */
    	        mAND_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 50:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:376: IFF_TOK
    	    {
    	        /* 1:376: IFF_TOK */
    	        mIFF_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 51:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:384: IMPLIES_TOK
    	    {
    	        /* 1:384: IMPLIES_TOK */
    	        mIMPLIES_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 52:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:396: REVIMPLIES_TOK
    	    {
    	        /* 1:396: REVIMPLIES_TOK */
    	        mREVIMPLIES_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 53:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:411: REVIFF_TOK
    	    {
    	        /* 1:411: REVIFF_TOK */
    	        mREVIFF_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 54:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:422: REVOR_TOK
    	    {
    	        /* 1:422: REVOR_TOK */
    	        mREVOR_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 55:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:432: REVAND_TOK
    	    {
    	        /* 1:432: REVAND_TOK */
    	        mREVAND_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 56:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:443: TIMES_TOK
    	    {
    	        /* 1:443: TIMES_TOK */
    	        mTIMES_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 57:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:453: PLUS_TOK
    	    {
    	        /* 1:453: PLUS_TOK */
    	        mPLUS_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 58:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:462: MINUS_TOK
    	    {
    	        /* 1:462: MINUS_TOK */
    	        mMINUS_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 59:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:472: APP_TOK
    	    {
    	        /* 1:472: APP_TOK */
    	        mAPP_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 60:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:480: TH1_UN_A
    	    {
    	        /* 1:480: TH1_UN_A */
    	        mTH1_UN_A(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 61:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:489: TH1_UN_E
    	    {
    	        /* 1:489: TH1_UN_E */
    	        mTH1_UN_E(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 62:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:498: TRUE_TOK
    	    {
    	        /* 1:498: TRUE_TOK */
    	        mTRUE_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 63:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:507: FALSE_TOK
    	    {
    	        /* 1:507: FALSE_TOK */
    	        mFALSE_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 64:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:517: EQUAL_TOK
    	    {
    	        /* 1:517: EQUAL_TOK */
    	        mEQUAL_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 65:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:527: DISEQUAL_TOK
    	    {
    	        /* 1:527: DISEQUAL_TOK */
    	        mDISEQUAL_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 66:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:540: CNF_TOK
    	    {
    	        /* 1:540: CNF_TOK */
    	        mCNF_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 67:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:548: FOF_TOK
    	    {
    	        /* 1:548: FOF_TOK */
    	        mFOF_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 68:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:556: THF_TOK
    	    {
    	        /* 1:556: THF_TOK */
    	        mTHF_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 69:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:564: TFF_TOK
    	    {
    	        /* 1:564: TFF_TOK */
    	        mTFF_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 70:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:572: TYPE_TOK
    	    {
    	        /* 1:572: TYPE_TOK */
    	        mTYPE_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 71:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:581: INCLUDE_TOK
    	    {
    	        /* 1:581: INCLUDE_TOK */
    	        mINCLUDE_TOK(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 72:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:593: DEFINED_SYMBOL
    	    {
    	        /* 1:593: DEFINED_SYMBOL */
    	        mDEFINED_SYMBOL(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 73:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:608: WHITESPACE
    	    {
    	        /* 1:608: WHITESPACE */
    	        mWHITESPACE(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 74:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:619: DISTINCT_OBJECT
    	    {
    	        /* 1:619: DISTINCT_OBJECT */
    	        mDISTINCT_OBJECT(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 75:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:635: LOWER_WORD_SINGLE_QUOTED
    	    {
    	        /* 1:635: LOWER_WORD_SINGLE_QUOTED */
    	        mLOWER_WORD_SINGLE_QUOTED(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 76:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:660: SINGLE_QUOTED
    	    {
    	        /* 1:660: SINGLE_QUOTED */
    	        mSINGLE_QUOTED(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 77:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:674: UPPER_WORD
    	    {
    	        /* 1:674: UPPER_WORD */
    	        mUPPER_WORD(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 78:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:685: LOWER_WORD
    	    {
    	        /* 1:685: LOWER_WORD */
    	        mLOWER_WORD(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 79:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:696: NUMBER
    	    {
    	        /* 1:696: NUMBER */
    	        mNUMBER(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;
    	case 80:
    	    // /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-21/src/parser/tptp/Tptp.g:1:703: COMMENT
    	    {
    	        /* 1:703: COMMENT */
    	        mCOMMENT(ctx );
    	        if  (HASEXCEPTION())
    	        {
    	            goto ruleTokensEx;
    	        }



    	    }
    	    break;

        }
    }


    goto ruleTokensEx; /* Prevent compiler warnings */
ruleTokensEx: ;
}

/* =========================================================================
 * Lexer matching rules end.
 * =========================================================================
 */
/* End of Lexer code
 * ================================================
 * ================================================
 */


/* End of code
 * =============================================================================
 */

Generated by: GCOVR (Version 3.2)