'!'=72 '!='=75 '$false'=79 '$less'=80 '$true'=78 '&'=70 '('=38 ')'=40 '*'=63 ','=39 '.'=41 ':'=61 ':='=77 '<='=66 '<=>'=64 '<~>'=67 '='=76 '=>'=65 '>'=62 '?'=73 'Could'=24 'Finite'=34 'Found!'=36 'Model'=35 'Satisfiable!'=22 'TRYING'=31 'Virtual'=29 'WARNING!'=23 '['=32 ']'=33 'assumption'=50 'axiom'=46 'conjecture'=47 'corollary'=53 'declare_'=45 'definition'=49 'distinct_domain'=43 'fi_domain'=57 'fi_functors'=58 'fi_predicates'=59 'finite_domain'=44 'fof'=37 'hypothesis'=48 'lemma'=51 'limit:'=28 'memory.'=30 'negated_conjecture'=54 'not'=25 'plain'=55 'resource'=27 'set'=26 'tff'=42 'theorem'=52 'type'=56 'unknown'=60 '|'=71 '~&'=69 '~'=74 '~|'=68 RULE_ALPHA_NUMERIC=13 RULE_ANY_OTHER=21 RULE_DOLLAR_ID=9 RULE_DOUBLE_DOLLAR_ID=10 RULE_DOUBLE_QUOTE=12 RULE_ID=16 RULE_INT=15 RULE_LITERAL=5 RULE_LOWER_WORD_ID=6 RULE_ML_COMMENT=18 RULE_SIGN=14 RULE_SIGNED_LITERAL=7 RULE_SINGLE_COMMENT=4 RULE_SINGLE_QUOTE=8 RULE_SL_COMMENT=19 RULE_STRING=17 RULE_UPPER_WORD_ID=11 RULE_WS=20 T__22=22 T__23=23 T__24=24 T__25=25 T__26=26 T__27=27 T__28=28 T__29=29 T__30=30 T__31=31 T__32=32 T__33=33 T__34=34 T__35=35 T__36=36 T__37=37 T__38=38 T__39=39 T__40=40 T__41=41 T__42=42 T__43=43 T__44=44 T__45=45 T__46=46 T__47=47 T__48=48 T__49=49 T__50=50 T__51=51 T__52=52 T__53=53 T__54=54 T__55=55 T__56=56 T__57=57 T__58=58 T__59=59 T__60=60 T__61=61 T__62=62 T__63=63 T__64=64 T__65=65 T__66=66 T__67=67 T__68=68 T__69=69 T__70=70 T__71=71 T__72=72 T__73=73 T__74=74 T__75=75 T__76=76 T__77=77 T__78=78 T__79=79 T__80=80