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