src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML
author sultana
Wed, 04 Apr 2012 16:29:16 +0100
changeset 47357 15e579392a68
parent 47316 15428dd82b54
child 47358 26c4e431ef05
permissions -rw-r--r--
refactored tptp yacc to bring close to official spec;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     1
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     2
(******************************************************************)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     3
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     4
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     5
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     6
(******************************************************************)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     7
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     8
(*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     9
  This file is produced from the parser generated by ML-Yacc from the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    10
  source files tptp.lex and tptp.yacc.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    11
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    12
signature TPTP_TOKENS =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    13
sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    14
type ('a,'b) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    15
type svalue
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
    16
val LET_TT:  'a * 'a -> (svalue,'a) token
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
    17
val LET_FT:  'a * 'a -> (svalue,'a) token
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
    18
val LET_FF:  'a * 'a -> (svalue,'a) token
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
    19
val LET_TF:  'a * 'a -> (svalue,'a) token
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    20
val ITE_T:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    21
val ITE_F:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    22
val CNF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    23
val FOF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    24
val TFF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    25
val THF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    26
val LET_TERM:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    27
val SUBTYPE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    28
val ATOMIC_SYSTEM_WORD: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    29
val ATOMIC_DEFINED_WORD: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    30
val DEP_PROD:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    31
val DEP_SUM:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    32
val GENTZEN_ARROW:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    33
val TIMES:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    34
val PLUS:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    35
val OPERATOR_EXISTS:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    36
val OPERATOR_FORALL:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    37
val DEFIN_CHOICE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    38
val INDEF_CHOICE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    39
val DUD:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    40
val DISTINCT_OBJECT: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    41
val COMMENT: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    42
val LOWER_WORD: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    43
val UPPER_WORD: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    44
val SINGLE_QUOTED: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    45
val DOT_DECIMAL: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    46
val UNSIGNED_INTEGER: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    47
val SIGNED_INTEGER: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    48
val RATIONAL: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    49
val REAL: (string) *  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    50
val DTFF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    51
val DFOT:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    52
val DCNF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    53
val DFOF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    54
val DTHF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    55
val EOF:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    56
val VLINE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    57
val TOK_TYPE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    58
val TOK_TRUE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    59
val TOK_RAT:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    60
val TOK_REAL:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    61
val TOK_INT:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    62
val TOK_O:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    63
val TOK_I:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    64
val TOK_FALSE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    65
val TILDE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    66
val RPAREN:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    67
val RBRKT:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    68
val QUESTION:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    69
val PPLUS:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    70
val PERIOD:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    71
val NOR:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    72
val XOR:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    73
val NEQUALS:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    74
val NAND:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    75
val MMINUS:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    76
val MAP_TO:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    77
val LPAREN:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    78
val LBRKT:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    79
val LAMBDA:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    80
val INCLUDE:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    81
val IMPLIES:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    82
val IFF:  'a * 'a -> (svalue,'a) token
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
    83
val FI:  'a * 'a -> (svalue,'a) token
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    84
val ARROW:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    85
val LET:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    86
val EXCLAMATION:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    87
val EQUALS:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    88
val COMMA:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    89
val COLON:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    90
val CARET:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    91
val AT_SIGN:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    92
val AMPERSAND:  'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    93
end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    94
signature TPTP_LRVALS=
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    95
sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    96
structure Tokens : TPTP_TOKENS
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    97
structure ParserData:PARSER_DATA
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    98
sharing type ParserData.Token.token = Tokens.token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    99
sharing type ParserData.svalue = Tokens.svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   100
end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   101
functor TPTPLexFun(structure Tokens: TPTP_TOKENS)=
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   102
   struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   103
    structure UserDeclarations =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   104
      struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   105
(*  Title:      HOL/TPTP/TPTP_Parser/tptp.lex
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   106
    Author:     Nik Sultana, Cambridge University Computer Laboratory
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   107
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   108
 Notes:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   109
 * Omit %full in definitions to restrict alphabet to ascii.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   110
 * Could include %posarg to ensure that start counting character positions from
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   111
   0, but it would punish performance.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   112
 * %s AF F COMMENT; -- could improve by making stateful.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   113
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   114
 Acknowledgements:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   115
 * Geoff Sutcliffe for help with TPTP.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   116
 * Timothy Bourke for his tips on getting ML-Yacc working with Poly/ML.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   117
 * An early version of this was ported from the specification shipped with
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   118
   Leo-II, written by Frank Theiss.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   119
 * Some boilerplate bits were taken from the ml-yacc/ml-lex manual by Roger Price.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   120
 * Jasmin Blanchette and Makarius Wenzel for help with Isabelle integration.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   121
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   122
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   123
structure T = Tokens
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   124
type pos = int             (* Position in file *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   125
type lineNo = int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   126
type svalue = T.svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   127
type ('a,'b) token = ('a,'b) T.token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   128
type lexresult = (svalue,pos) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   129
type lexarg = string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   130
type arg = lexarg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   131
val col = Unsynchronized.ref 0;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   132
val linep = Unsynchronized.ref 1;         (* Line pointer *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   133
val eolpos = Unsynchronized.ref 0;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   134
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   135
val badCh : string * string * int * int -> unit = fn
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   136
    (file_name, bad, line, col) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   137
    TextIO.output(TextIO.stdOut, file_name ^ "["
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   138
          ^ Int.toString line ^ "." ^ Int.toString col
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   139
          ^ "] Invalid character \"" ^ bad ^ "\"\n");
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   140
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   141
val eof = fn file_name =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   142
  let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   143
    val result = T.EOF (!linep,!col);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   144
    val _ = linep := 0;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   145
  in result end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   146
(*here could check whether file ended prematurely:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   147
 see if have open brackets, or if we're in some state other than INITIAL*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   148
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   149
val count_commentlines : string -> unit = fn str =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   150
  let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   151
    val str' = String.explode str
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   152
    val newlines = List.filter (fn x => x = #"\n") str'
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   153
  in linep := (!linep) + (List.length newlines) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   154
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   155
end (* end of user routines *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   156
exception LexError (* raised if illegal leaf action tried *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   157
structure Internal =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   158
	struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   159
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   160
datatype yyfinstate = N of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   161
type statedata = {fin : yyfinstate list, trans: string}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   162
(* transition & final state table *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   163
val tab = let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   164
val s = [ 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   165
 (0, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   166
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   167
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   168
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   169
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   170
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   171
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   172
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   173
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   174
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   175
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   176
 (1, 
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   177
"\000\000\000\000\000\000\000\000\000\144\146\000\000\145\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   178
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   179
\\144\140\134\000\102\090\089\083\082\081\080\078\077\072\070\057\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   180
\\048\048\048\048\048\048\048\048\048\048\045\000\039\037\036\033\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   181
\\030\029\029\029\029\029\029\029\029\029\029\029\029\029\029\029\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   182
\\029\029\029\029\029\029\029\029\029\029\029\028\000\027\026\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   183
\\000\007\007\023\007\007\020\007\007\013\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   184
\\007\007\007\007\008\007\007\007\007\007\007\000\006\000\003\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   185
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   186
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   187
 (3, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   188
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   189
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   190
\\000\000\000\000\000\000\005\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   191
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   192
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   193
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   194
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   195
\\000\000\000\000\000\000\000\000\000\000\000\000\004\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   196
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   197
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   198
 (7, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   199
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   200
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   201
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   202
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   203
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   204
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   205
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   206
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   207
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   208
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   209
 (8, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   210
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   211
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   212
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   213
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   214
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   215
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   216
\\000\007\007\007\007\007\011\007\009\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   217
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   218
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   219
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   220
 (9, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   221
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   222
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   223
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   224
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   225
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   226
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   227
\\000\007\007\007\007\007\010\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   228
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   229
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   230
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   231
 (11, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   232
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   233
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   234
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   235
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   236
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   237
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   238
\\000\007\007\007\007\007\012\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   239
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   240
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   241
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   242
 (13, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   243
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   244
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   245
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   246
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   247
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   248
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   249
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\014\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   250
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   251
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   252
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   253
 (14, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   254
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   255
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   256
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   257
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   258
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   259
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   260
\\000\007\007\015\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   261
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   262
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   263
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   264
 (15, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   265
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   266
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   267
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   268
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   269
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   270
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   271
\\000\007\007\007\007\007\007\007\007\007\007\007\016\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   272
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   273
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   274
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   275
 (16, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   276
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   277
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   278
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   279
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   280
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   281
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   282
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   283
\\007\007\007\007\007\017\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   284
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   285
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   286
 (17, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   287
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   288
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   289
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   290
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   291
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   292
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   293
\\000\007\007\007\018\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   294
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   295
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   296
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   297
 (18, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   298
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   299
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   300
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   301
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   302
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   303
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   304
\\000\007\007\007\007\019\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   305
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   306
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   307
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   308
 (20, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   309
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   310
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   311
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   312
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   313
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   314
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   315
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\021\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   316
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   317
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   318
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   319
 (21, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   320
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   321
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   322
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   323
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   324
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   325
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   326
\\000\007\007\007\007\007\022\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   327
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   328
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   329
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   330
 (23, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   331
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   332
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   333
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   334
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   335
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   336
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   337
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\024\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   338
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   339
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   340
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   341
 (24, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   342
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   343
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   344
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   345
\\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   346
\\000\007\007\007\007\007\007\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   347
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   348
\\000\007\007\007\007\007\025\007\007\007\007\007\007\007\007\007\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   349
\\007\007\007\007\007\007\007\007\007\007\007\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   350
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   351
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   352
 (29, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   353
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   354
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   355
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   356
\\029\029\029\029\029\029\029\029\029\029\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   357
\\000\029\029\029\029\029\029\029\029\029\029\029\029\029\029\029\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   358
\\029\029\029\029\029\029\029\029\029\029\029\000\000\000\000\029\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   359
\\000\029\029\029\029\029\029\029\029\029\029\029\029\029\029\029\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   360
\\029\029\029\029\029\029\029\029\029\029\029\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   361
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   362
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   363
 (30, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   364
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   365
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   366
\\000\000\000\000\000\000\000\000\000\000\000\032\000\031\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   367
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   368
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   369
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   370
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   371
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   372
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   373
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   374
 (33, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   375
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   376
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   377
\\000\000\000\000\000\000\000\000\000\000\035\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   378
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\034\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   379
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   380
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   381
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   382
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   383
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   384
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   385
 (37, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   386
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   387
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   388
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   389
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\038\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   390
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   391
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   392
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   393
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   394
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   395
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   396
 (39, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   397
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   398
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   399
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   400
\\000\000\000\000\000\000\000\000\000\000\000\000\044\042\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   401
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   402
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   403
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   404
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\040\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   405
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   406
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   407
 (40, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   408
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   409
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   410
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   411
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\041\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   412
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   413
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   414
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   415
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   416
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   417
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   418
 (42, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   419
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   420
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   421
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   422
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\043\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   423
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   424
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   425
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   426
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   427
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   428
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   429
 (45, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   430
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   431
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   432
\\000\000\000\000\000\000\000\000\000\000\000\000\000\047\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   433
\\000\000\000\000\000\000\000\000\000\000\000\000\000\046\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   434
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   435
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   436
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   437
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   438
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   439
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   440
 (48, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   441
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   442
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   443
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\051\049\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   444
\\048\048\048\048\048\048\048\048\048\048\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   445
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   446
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   447
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   448
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   449
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   450
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   451
 (49, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   452
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   453
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   454
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   455
\\050\050\050\050\050\050\050\050\050\050\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   456
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   457
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   458
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   459
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   460
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   461
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   462
 (51, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   463
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   464
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   465
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   466
\\052\052\052\052\052\052\052\052\052\052\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   467
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   468
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   469
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   470
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   471
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   472
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   473
 (52, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   474
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   475
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   476
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   477
\\052\052\052\052\052\052\052\052\052\052\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   478
\\000\000\000\000\000\053\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   479
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   480
\\000\000\000\000\000\053\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   481
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   482
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   483
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   484
 (53, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   485
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   486
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   487
\\000\000\000\000\000\000\000\000\000\000\000\055\000\055\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   488
\\054\054\054\054\054\054\054\054\054\054\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   489
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   490
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   491
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   492
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   493
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   494
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   495
 (54, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   496
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   497
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   498
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   499
\\054\054\054\054\054\054\054\054\054\054\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   500
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   501
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   502
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   503
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   504
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   505
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   506
 (55, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   507
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   508
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   509
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   510
\\056\056\056\056\056\056\056\056\056\056\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   511
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   512
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   513
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   514
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   515
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   516
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   517
 (57, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   518
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   519
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   520
\\000\000\000\000\000\000\000\000\000\000\058\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   521
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   522
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   523
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   524
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   525
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   526
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   527
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   528
 (58, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   529
"\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   530
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   531
\\058\058\058\058\058\058\058\058\058\058\059\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   532
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   533
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   534
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   535
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   536
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   537
\\058"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   538
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   539
 (59, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   540
"\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   541
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   542
\\058\058\058\058\058\058\058\058\058\058\059\058\058\058\058\060\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   543
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   544
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   545
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   546
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   547
\\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\058\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   548
\\058"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   549
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   550
 (60, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   551
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   552
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   553
\\000\000\000\000\000\064\000\000\000\000\000\000\000\000\000\061\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   554
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   555
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   556
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   557
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   558
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   559
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   560
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   561
 (61, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   562
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   563
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   564
\\000\000\000\000\000\000\000\000\000\000\062\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   565
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   566
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   567
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   568
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   569
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   570
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   571
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   572
 (62, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   573
"\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   574
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   575
\\062\062\062\062\062\062\062\062\062\062\063\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   576
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   577
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   578
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   579
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   580
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   581
\\062"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   582
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   583
 (63, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   584
"\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   585
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   586
\\062\062\062\062\062\062\062\062\062\062\063\062\062\062\062\060\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   587
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   588
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   589
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   590
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   591
\\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\062\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   592
\\062"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   593
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   594
 (64, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   595
"\064\064\064\064\064\064\064\064\064\064\000\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   596
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   597
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\065\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   598
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   599
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   600
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   601
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   602
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   603
\\064"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   604
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   605
 (65, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   606
"\064\064\064\064\064\064\064\064\064\064\000\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   607
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   608
\\064\064\064\064\064\064\064\064\064\064\066\064\064\064\064\065\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   609
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   610
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   611
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   612
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   613
\\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\064\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   614
\\064"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   615
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   616
 (66, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   617
"\066\066\066\066\066\066\066\066\066\066\062\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   618
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   619
\\066\066\066\066\066\066\066\066\066\066\069\066\066\066\066\067\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   620
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   621
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   622
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   623
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   624
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   625
\\066"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   626
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   627
 (67, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   628
"\066\066\066\066\066\066\066\066\066\066\062\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   629
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   630
\\066\066\066\066\066\066\066\066\066\066\068\066\066\066\066\067\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   631
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   632
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   633
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   634
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   635
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   636
\\066"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   637
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   638
 (69, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   639
"\066\066\066\066\066\066\066\066\066\066\062\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   640
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   641
\\066\066\066\066\066\066\066\066\066\066\069\066\066\066\066\065\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   642
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   643
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   644
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   645
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   646
\\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\066\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   647
\\066"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   648
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   649
 (70, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   650
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   651
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   652
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   653
\\071\071\071\071\071\071\071\071\071\071\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   654
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   655
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   656
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   657
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   658
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   659
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   660
 (72, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   661
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   662
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   663
\\000\000\000\000\000\000\000\000\000\000\000\000\000\075\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   664
\\074\074\074\074\074\074\074\074\074\074\000\000\000\000\073\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   665
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   666
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   667
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   668
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   669
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   670
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   671
 (74, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   672
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   673
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   674
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\051\049\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   675
\\074\074\074\074\074\074\074\074\074\074\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   676
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   677
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   678
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   679
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   680
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   681
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   682
 (75, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   683
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   684
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   685
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   686
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\076\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   687
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   688
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   689
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   690
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   691
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   692
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   693
 (78, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   694
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   695
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   696
\\000\000\000\000\000\000\000\000\000\000\000\079\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   697
\\074\074\074\074\074\074\074\074\074\074\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   698
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   699
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   700
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   701
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   702
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   703
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   704
 (83, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   705
"\000\000\000\000\000\000\000\000\000\084\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   706
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   707
\\084\000\000\000\000\000\000\000\084\084\000\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   708
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   709
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   710
\\084\084\084\084\084\084\084\084\084\084\084\084\088\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   711
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   712
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   713
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   714
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   715
 (84, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   716
"\000\000\000\000\000\000\000\000\000\084\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   717
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   718
\\084\000\000\000\000\000\000\087\084\084\000\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   719
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   720
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   721
\\084\084\084\084\084\084\084\084\084\084\084\084\085\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   722
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   723
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   724
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   725
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   726
 (85, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   727
"\000\000\000\000\000\000\000\000\000\084\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   728
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   729
\\084\000\000\000\000\000\000\086\084\084\000\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   730
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   731
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   732
\\084\084\084\084\084\084\084\084\084\084\084\084\085\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   733
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   734
\\084\084\084\084\084\084\084\084\084\084\084\084\084\084\084\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   735
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   736
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   737
 (90, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   738
"\090\090\090\090\090\090\090\090\090\090\000\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   739
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   740
\\090\090\090\090\090\101\090\090\090\090\090\090\090\090\090\091\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   741
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   742
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   743
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   744
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   745
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   746
\\090"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   747
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   748
 (91, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   749
"\090\090\090\090\090\090\090\090\090\090\000\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   750
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   751
\\090\090\090\090\090\101\090\090\090\090\092\090\090\090\090\091\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   752
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   753
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   754
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   755
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   756
\\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\090\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   757
\\090"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   758
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   759
 (92, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   760
"\092\092\092\092\092\092\092\092\092\092\062\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   761
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   762
\\092\092\092\092\092\096\092\092\092\092\095\092\092\092\092\093\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   763
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   764
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   765
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   766
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   767
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   768
\\092"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   769
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   770
 (93, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   771
"\092\092\092\092\092\092\092\092\092\092\062\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   772
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   773
\\092\092\092\092\092\096\092\092\092\092\094\092\092\092\092\093\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   774
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   775
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   776
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   777
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   778
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   779
\\092"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   780
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   781
 (95, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   782
"\092\092\092\092\092\092\092\092\092\092\062\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   783
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   784
\\092\092\092\092\092\096\092\092\092\092\095\092\092\092\092\091\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   785
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   786
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   787
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   788
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   789
\\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\092\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   790
\\092"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   791
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   792
 (96, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   793
"\096\096\096\096\096\096\096\096\096\096\062\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   794
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   795
\\096\096\096\096\096\096\096\096\096\096\099\096\096\096\096\097\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   796
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   797
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   798
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   799
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   800
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   801
\\096"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   802
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   803
 (97, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   804
"\096\096\096\096\096\096\096\096\096\096\062\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   805
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   806
\\096\096\096\096\096\096\096\096\096\096\098\096\096\096\096\097\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   807
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   808
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   809
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   810
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   811
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   812
\\096"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   813
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   814
 (99, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   815
"\096\096\096\096\096\096\096\096\096\096\062\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   816
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   817
\\096\096\096\096\096\096\096\096\096\096\099\096\096\096\096\100\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   818
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   819
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   820
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   821
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   822
\\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\096\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   823
\\096"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   824
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   825
 (100, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   826
"\101\101\101\101\101\101\101\101\101\101\000\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   827
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   828
\\101\101\101\101\101\101\101\101\101\101\096\101\101\101\101\100\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   829
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   830
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   831
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   832
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   833
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   834
\\101"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   835
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   836
 (101, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   837
"\101\101\101\101\101\101\101\101\101\101\000\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   838
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   839
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\100\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   840
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   841
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   842
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   843
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   844
\\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\101\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   845
\\101"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   846
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   847
 (102, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   848
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   849
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   850
\\000\000\000\000\132\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   851
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   852
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   853
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   854
\\000\103\103\129\103\103\125\103\103\119\103\103\109\103\103\103\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   855
\\103\103\103\103\104\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   856
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   857
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   858
 (103, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   859
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   860
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   861
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   862
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   863
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   864
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   865
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   866
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   867
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   868
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   869
 (104, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   870
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   871
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   872
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   873
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   874
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   875
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   876
\\000\103\103\103\103\103\107\103\105\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   877
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   878
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   879
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   880
 (105, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   881
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   882
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   883
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   884
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   885
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   886
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   887
\\000\103\103\103\103\103\106\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   888
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   889
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   890
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   891
 (107, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   892
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   893
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   894
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   895
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   896
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   897
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   898
\\000\103\103\103\103\103\108\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   899
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   900
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   901
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   902
 (109, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   903
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   904
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   905
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   906
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   907
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   908
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   909
\\000\103\103\103\103\110\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   910
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   911
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   912
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   913
 (110, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   914
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   915
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   916
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   917
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   918
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   919
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   920
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   921
\\103\103\103\103\111\103\103\103\103\103\103\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   922
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   923
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   924
 (111, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   925
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   926
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   927
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   928
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   929
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   930
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\112\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   931
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   932
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   933
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   934
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   935
 (112, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   936
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   937
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   938
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   939
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   940
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   941
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   942
\\000\103\103\103\103\103\116\103\103\103\103\103\103\103\103\103\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   943
\\103\103\103\103\113\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   944
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   945
),
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   946
 (113, 
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   947
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   948
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   949
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   950
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   951
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   952
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   953
\\000\103\103\103\103\103\115\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   954
\\103\103\103\103\114\103\103\103\103\103\103\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   955
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   956
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   957
 (116, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   958
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   959
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   960
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   961
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   962
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   963
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   964
\\000\103\103\103\103\103\118\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   965
\\103\103\103\103\117\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   966
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   967
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   968
 (119, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   969
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   970
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   971
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   972
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   973
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   974
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   975
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   976
\\103\103\103\103\120\103\103\103\103\103\103\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   977
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   978
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   979
 (120, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   980
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   981
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   982
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   983
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   984
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   985
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   986
\\000\103\103\103\103\121\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   987
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   988
\\000"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   989
),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   990
 (121, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   991
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   992
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   993
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   994
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   995
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   996
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\122\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
   997
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   998
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   999
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1000
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1001
 (122, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1002
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1003
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1004
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1005
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1006
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1007
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1008
\\000\103\103\103\103\103\124\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1009
\\103\103\103\103\123\103\103\103\103\103\103\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1010
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1011
),
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1012
 (125, 
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1013
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1014
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1015
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1016
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1017
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1018
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1019
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\126\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1020
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1021
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1022
),
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1023
 (126, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1024
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1025
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1026
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1027
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1028
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1029
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1030
\\000\103\103\103\103\103\128\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1031
\\103\103\103\103\127\103\103\103\103\103\103\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1032
\\000"
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1033
),
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1034
 (129, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1035
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1036
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1037
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1038
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1039
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1040
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1041
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\130\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1042
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1043
\\000"
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1044
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1045
 (130, 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1046
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1047
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1048
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1049
\\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1050
\\000\103\103\103\103\103\103\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1051
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1052
\\000\103\103\103\103\103\131\103\103\103\103\103\103\103\103\103\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1053
\\103\103\103\103\103\103\103\103\103\103\103\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1054
\\000"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1055
),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1056
 (132, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1057
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1058
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1059
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1060
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1061
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1062
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1063
\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1064
\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1065
\\000"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1066
),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1067
 (133, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1068
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1069
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1070
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1071
\\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1072
\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1073
\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\133\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1074
\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1075
\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1076
\\000"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1077
),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1078
 (134, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1079
"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1080
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1081
\\135\135\000\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1082
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1083
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1084
\\135\135\135\135\135\135\135\135\135\135\135\135\139\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1085
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1086
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1087
\\135"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1088
),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1089
 (135, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1090
"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1091
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1092
\\135\135\138\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1093
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1094
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1095
\\135\135\135\135\135\135\135\135\135\135\135\135\136\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1096
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1097
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1098
\\135"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1099
),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1100
 (136, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1101
"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1102
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1103
\\135\135\137\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1104
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1105
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1106
\\135\135\135\135\135\135\135\135\135\135\135\135\136\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1107
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1108
\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1109
\\135"
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1110
),
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1111
 (140, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1112
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1113
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1114
\\000\143\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1115
\\000\000\000\000\000\000\000\000\000\000\000\000\000\142\141\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1116
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1117
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1118
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1119
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1120
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1121
),
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1122
 (144, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1123
"\000\000\000\000\000\000\000\000\000\144\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1124
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1125
\\144\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1126
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1127
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1128
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1129
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1130
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1131
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1132
),
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1133
 (145, 
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1134
"\000\000\000\000\000\000\000\000\000\000\146\000\000\000\000\000\
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1135
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1136
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1137
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1138
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1139
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1140
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1141
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1142
\\000"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1143
),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1144
(0, "")]
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1145
fun f x = x 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1146
val s = map f (rev (tl (rev s))) 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1147
exception LexHackingError 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1148
fun look ((j,x)::r, i: int) = if i = j then x else look(r, i) 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1149
  | look ([], i) = raise LexHackingError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1150
fun g {fin=x, trans=i} = {fin=x, trans=look(s,i)} 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1151
in Vector.fromList(map g 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1152
[{fin = [], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1153
{fin = [(N 2)], trans = 1},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1154
{fin = [(N 2)], trans = 1},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1155
{fin = [(N 84)], trans = 3},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1156
{fin = [(N 71)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1157
{fin = [(N 61)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1158
{fin = [(N 86)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1159
{fin = [(N 283)], trans = 7},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1160
{fin = [(N 283)], trans = 8},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1161
{fin = [(N 283)], trans = 9},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1162
{fin = [(N 186),(N 283)], trans = 7},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1163
{fin = [(N 283)], trans = 11},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1164
{fin = [(N 198),(N 283)], trans = 7},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1165
{fin = [(N 283)], trans = 13},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1166
{fin = [(N 283)], trans = 14},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1167
{fin = [(N 283)], trans = 15},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1168
{fin = [(N 283)], trans = 16},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1169
{fin = [(N 283)], trans = 17},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1170
{fin = [(N 283)], trans = 18},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1171
{fin = [(N 206),(N 283)], trans = 7},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1172
{fin = [(N 283)], trans = 20},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1173
{fin = [(N 283)], trans = 21},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1174
{fin = [(N 190),(N 283)], trans = 7},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1175
{fin = [(N 283)], trans = 23},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1176
{fin = [(N 283)], trans = 24},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1177
{fin = [(N 194),(N 283)], trans = 7},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1178
{fin = [(N 25)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1179
{fin = [(N 80)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1180
{fin = [(N 50)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1181
{fin = [(N 157)], trans = 29},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1182
{fin = [(N 23)], trans = 30},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1183
{fin = [(N 15)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1184
{fin = [(N 12)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1185
{fin = [(N 78)], trans = 33},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1186
{fin = [(N 21)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1187
{fin = [(N 315)], trans = 0},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1188
{fin = [(N 38)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1189
{fin = [(N 31)], trans = 37},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1190
{fin = [(N 48)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1191
{fin = [], trans = 39},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1192
{fin = [], trans = 40},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1193
{fin = [(N 68)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1194
{fin = [(N 41)], trans = 42},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1195
{fin = [(N 45)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1196
{fin = [(N 309)], trans = 0},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1197
{fin = [(N 27)], trans = 45},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1198
{fin = [(N 36)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1199
{fin = [(N 318)], trans = 0},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1200
{fin = [(N 126)], trans = 48},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1201
{fin = [], trans = 49},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1202
{fin = [(N 104)], trans = 49},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1203
{fin = [], trans = 51},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1204
{fin = [(N 119)], trans = 52},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1205
{fin = [], trans = 53},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1206
{fin = [(N 119)], trans = 54},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1207
{fin = [], trans = 55},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1208
{fin = [(N 119)], trans = 55},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1209
{fin = [], trans = 57},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1210
{fin = [], trans = 58},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1211
{fin = [], trans = 59},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1212
{fin = [(N 182)], trans = 60},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1213
{fin = [], trans = 61},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1214
{fin = [], trans = 62},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1215
{fin = [], trans = 63},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1216
{fin = [(N 182)], trans = 64},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1217
{fin = [(N 182)], trans = 65},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1218
{fin = [(N 182)], trans = 66},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1219
{fin = [(N 182)], trans = 67},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1220
{fin = [(N 182)], trans = 66},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1221
{fin = [(N 182)], trans = 69},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1222
{fin = [(N 73)], trans = 70},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1223
{fin = [(N 130)], trans = 70},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1224
{fin = [], trans = 72},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1225
{fin = [(N 55)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1226
{fin = [(N 123)], trans = 74},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1227
{fin = [(N 58)], trans = 75},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1228
{fin = [(N 306)], trans = 0},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1229
{fin = [(N 29)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1230
{fin = [(N 300)], trans = 78},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1231
{fin = [(N 76)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1232
{fin = [(N 302)], trans = 0},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1233
{fin = [(N 82)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1234
{fin = [(N 52)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1235
{fin = [], trans = 83},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1236
{fin = [], trans = 84},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1237
{fin = [], trans = 85},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1238
{fin = [(N 151)], trans = 84},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1239
{fin = [(N 151)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1240
{fin = [], trans = 85},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1241
{fin = [(N 9)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1242
{fin = [(N 182)], trans = 90},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1243
{fin = [(N 182)], trans = 91},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1244
{fin = [(N 182)], trans = 92},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1245
{fin = [(N 182)], trans = 93},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1246
{fin = [(N 182)], trans = 92},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1247
{fin = [(N 182)], trans = 95},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1248
{fin = [(N 182)], trans = 96},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1249
{fin = [(N 182)], trans = 97},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1250
{fin = [(N 182)], trans = 96},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1251
{fin = [(N 182)], trans = 99},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1252
{fin = [(N 182)], trans = 100},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1253
{fin = [(N 182)], trans = 101},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1254
{fin = [], trans = 102},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1255
{fin = [(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1256
{fin = [(N 298)], trans = 104},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1257
{fin = [(N 298)], trans = 105},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1258
{fin = [(N 211),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1259
{fin = [(N 298)], trans = 107},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1260
{fin = [(N 231),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1261
{fin = [(N 298)], trans = 109},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1262
{fin = [(N 298)], trans = 110},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1263
{fin = [(N 298)], trans = 111},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1264
{fin = [(N 298)], trans = 112},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1265
{fin = [(N 298)], trans = 113},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1266
{fin = [(N 277),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1267
{fin = [(N 253),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1268
{fin = [(N 298)], trans = 116},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1269
{fin = [(N 269),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1270
{fin = [(N 261),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1271
{fin = [(N 298)], trans = 119},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1272
{fin = [(N 298)], trans = 120},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1273
{fin = [(N 298)], trans = 121},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1274
{fin = [(N 298)], trans = 122},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1275
{fin = [(N 245),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1276
{fin = [(N 238),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1277
{fin = [(N 298)], trans = 125},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1278
{fin = [(N 298)], trans = 126},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1279
{fin = [(N 226),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1280
{fin = [(N 216),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1281
{fin = [(N 298)], trans = 129},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1282
{fin = [(N 298)], trans = 130},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1283
{fin = [(N 221),(N 298)], trans = 103},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1284
{fin = [], trans = 132},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1285
{fin = [(N 291)], trans = 133},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1286
{fin = [], trans = 134},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1287
{fin = [], trans = 135},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1288
{fin = [], trans = 136},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1289
{fin = [(N 95)], trans = 135},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1290
{fin = [(N 95)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1291
{fin = [], trans = 136},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1292
{fin = [(N 33)], trans = 140},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1293
{fin = [(N 312)], trans = 0},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1294
{fin = [(N 64)], trans = 0},
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1295
{fin = [(N 18)], trans = 0},
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1296
{fin = [(N 2)], trans = 144},
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1297
{fin = [(N 7)], trans = 145},
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1298
{fin = [(N 7)], trans = 0}])
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1299
end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1300
structure StartStates =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1301
	struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1302
	datatype yystartstate = STARTSTATE of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1303
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1304
(* start state definitions *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1305
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1306
val INITIAL = STARTSTATE 1;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1307
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1308
end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1309
type result = UserDeclarations.lexresult
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1310
	exception LexerError (* raised if illegal leaf action tried *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1311
end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1312
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1313
fun makeLexer yyinput =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1314
let	val yygone0=1
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1315
	val yyb = Unsynchronized.ref "\n" 		(* buffer *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1316
	val yybl = Unsynchronized.ref 1		(*buffer length *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1317
	val yybufpos = Unsynchronized.ref 1		(* location of next character to use *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1318
	val yygone = Unsynchronized.ref yygone0	(* position in file of beginning of buffer *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1319
	val yydone = Unsynchronized.ref false		(* eof found yet? *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1320
	val yybegin = Unsynchronized.ref 1		(*Current 'start state' for lexer *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1321
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1322
	val YYBEGIN = fn (Internal.StartStates.STARTSTATE x) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1323
		 yybegin := x
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1324
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1325
fun lex (yyarg as (file_name:string)) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1326
let fun continue() : Internal.result = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1327
  let fun scan (s,AcceptingLeaves : Internal.yyfinstate list list,l,i0) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1328
	let fun action (i,nil) = raise LexError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1329
	| action (i,nil::l) = action (i-1,l)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1330
	| action (i,(node::acts)::l) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1331
		case node of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1332
		    Internal.N yyk => 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1333
			(let fun yymktext() = substring(!yyb,i0,i-i0)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1334
			     val yypos = i0+ !yygone
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1335
			open UserDeclarations Internal.StartStates
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1336
 in (yybufpos := i; case yyk of 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1337
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1338
			(* Application actions *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1339
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1340
  104 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.RATIONAL(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1341
| 119 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.REAL(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1342
| 12 => (col:=yypos-(!eolpos); T.INDEF_CHOICE(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1343
| 123 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.SIGNED_INTEGER(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1344
| 126 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.UNSIGNED_INTEGER(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1345
| 130 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOT_DECIMAL(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1346
| 15 => (col:=yypos-(!eolpos); T.DEFIN_CHOICE(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1347
| 151 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.SINGLE_QUOTED(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1348
| 157 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.UPPER_WORD(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1349
| 18 => (col:=yypos-(!eolpos); T.OPERATOR_FORALL(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1350
| 182 => let val yytext=yymktext() in col:=yypos-(!eolpos); count_commentlines yytext;T.COMMENT(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1351
| 186 => (col:=yypos-(!eolpos); T.THF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1352
| 190 => (col:=yypos-(!eolpos); T.FOF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1353
| 194 => (col:=yypos-(!eolpos); T.CNF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1354
| 198 => (col:=yypos-(!eolpos); T.TFF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1355
| 2 => let val yytext=yymktext() in col:=(!col)+size yytext; continue ()  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1356
| 206 => (col:=yypos-(!eolpos); T.INCLUDE(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1357
| 21 => (col:=yypos-(!eolpos); T.OPERATOR_EXISTS(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1358
| 211 => (col:=yypos-(!eolpos); T.DTHF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1359
| 216 => (col:=yypos-(!eolpos); T.DFOF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1360
| 221 => (col:=yypos-(!eolpos); T.DCNF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1361
| 226 => (col:=yypos-(!eolpos); T.DFOT(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1362
| 23 => (col:=yypos-(!eolpos); T.AT_SIGN(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1363
| 231 => (col:=yypos-(!eolpos); T.DTFF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1364
| 238 => (col:=yypos-(!eolpos); T.ITE_F(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1365
| 245 => (col:=yypos-(!eolpos); T.ITE_T(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1366
| 25 => (col:=yypos-(!eolpos); T.CARET(!linep,!col))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1367
| 253 => (col:=yypos-(!eolpos); T.LET_TF(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1368
| 261 => (col:=yypos-(!eolpos); T.LET_FF(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1369
| 269 => (col:=yypos-(!eolpos); T.LET_FT(!linep,!col))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1370
| 27 => (col:=yypos-(!eolpos); T.COLON(!linep,!col))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1371
| 277 => (col:=yypos-(!eolpos); T.LET_TT(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1372
| 283 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col) end
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1373
| 29 => (col:=yypos-(!eolpos); T.COMMA(!linep,!col))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1374
| 291 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.ATOMIC_SYSTEM_WORD(yytext,!linep,!col) end
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1375
| 298 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.ATOMIC_DEFINED_WORD(yytext,!linep,!col) end
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1376
| 300 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1377
| 302 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1378
| 306 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1379
| 309 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1380
| 31 => (col:=yypos-(!eolpos); T.EQUALS(!linep,!col))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1381
| 312 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1382
| 315 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1383
| 318 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1384
| 33 => (col:=yypos-(!eolpos); T.EXCLAMATION(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1385
| 36 => (col:=yypos-(!eolpos); T.LET(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1386
| 38 => (col:=yypos-(!eolpos); T.ARROW(!linep,!col))
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 47316
diff changeset
  1387
| 41 => (col:=yypos-(!eolpos); T.FI(!linep,!col))
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1388
| 45 => (col:=yypos-(!eolpos); T.IFF(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1389
| 48 => (col:=yypos-(!eolpos); T.IMPLIES(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1390
| 50 => (col:=yypos-(!eolpos); T.LBRKT(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1391
| 52 => (col:=yypos-(!eolpos); T.LPAREN(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1392
| 55 => (col:=yypos-(!eolpos); T.MAP_TO(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1393
| 58 => (col:=yypos-(!eolpos); T.MMINUS(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1394
| 61 => (col:=yypos-(!eolpos); T.NAND(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1395
| 64 => (col:=yypos-(!eolpos); T.NEQUALS(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1396
| 68 => (col:=yypos-(!eolpos); T.XOR(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1397
| 7 => let val yytext=yymktext() in linep:=(!linep)+1;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1398
                   eolpos:=yypos+size yytext; continue () end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1399
| 71 => (col:=yypos-(!eolpos); T.NOR(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1400
| 73 => (col:=yypos-(!eolpos); T.PERIOD(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1401
| 76 => (col:=yypos-(!eolpos); T.PPLUS(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1402
| 78 => (col:=yypos-(!eolpos); T.QUESTION(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1403
| 80 => (col:=yypos-(!eolpos); T.RBRKT(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1404
| 82 => (col:=yypos-(!eolpos); T.RPAREN(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1405
| 84 => (col:=yypos-(!eolpos); T.TILDE(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1406
| 86 => (col:=yypos-(!eolpos); T.VLINE(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1407
| 9 => (col:=yypos-(!eolpos); T.AMPERSAND(!linep,!col))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1408
| 95 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DISTINCT_OBJECT(yytext,!linep,!col) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1409
| _ => raise Internal.LexerError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1410
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1411
		) end )
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset