TPTP v9.1.0

[Geoff Sutcliffe]

================================================================================

                   The TPTP Problem Library, Release v9.1.0
                   ----------------------------------------

                                Geoff Sutcliffe
                                ge...@tptp.org

The TPTP  (Thousands  of Problems  for Theorem  Provers)  Problem Library  is a
library  of  test problems for  automated theorem proving  (ATP)  systems.  The
principal motivation for the TPTP  is to support the testing and evaluation  of
ATP systems,  to help ensure that  performance results  accurately reflect  the
capabilities of the ATP system being considered.

TPTP v9.1.0 is now available at:
    http://tptp.org/TPTP
The TPTP-v9.0.0.tgz file  contains the  library,  including utilities and basic
documentation. Full documentation is online at:
    http://tptp.org/TPTP/TR/TPTPTR.shtml

========================== What's New in this Release ==========================

Changes from v9.0.0 to v9.1.0 for THF problems
  9 new problems, in the domains PHI PUZ.

Changes from v9.0.0 to v9.1.0 for TFF problems
181 new problems, in the domains ARI CSR DAT LCL PUZ SWW SWX SYO.

Changes from v9.0.0 to v9.1.0 for FOF problems
168 new problems, in the domains LCL PUZ SEV SWX.

In SyntaxBNF:
- (TPTP version.internal development number)
- Added <tff_quantifier>. Added <hash> (for epsilon terms) to <thf_quantifier> and
        <tff_quantifier>. Changed <tff_quantified_formula> to use <tff_quantifier>.
- Removed axiom_of_choice as an <intro_type>
- Renamed <inference_parents> to <parents>
  <inference_record>     :== inference(<inference_rule>,<useful_info>,<parents>)
- Aligned introduced and creator with inferred
  <internal_source>      :== introduced(<intro_type>,<useful_info>,<parents>)
  <creator_source>       :== creator(<creator_name>,<useful_info>,<parents>)
- Moved <hash> to <fof_quantifier> so it's available in all languages.
- Removed ()s around <thf_defined_infix> and <thf_infix_unary>
- Removed ()s around <tff_defined_infix> and <tff_infix_unary>
- Fixed typo in <ntf_domain_type>
- Converted <source> and it's descendents to grammar rules. That required adding a grammar rule
  for <intro_type>.
- Changed <file_name> to <atomic_word>, to allow non-quoted filenames.
- Linearised <thf_formula_list>, <tff_arguments>, <fof_formula_tuple_list>, <parent_list>,
  <info_items>, <general_terms>.
- Replaced <null> by <nothing> to avoid conflicts in Java parsers
- Allow only <unsigned_integer> in a <name>
- Reordered numerics to make lex/yacc happy, including some renaming and factoring
- Reverted <name> to allow <integer>, because lex/yacc stuff hurts.
- Moved <hash> to <tff_quantifier> and set <thf_quantifier> to use <tff_quantifier>.
  This means epsilon terms are quantified formulae (yak) available in only TFF (really TXF, which
  is cool).
- Changed <parent_details> to use <general_term>
================================================================================