more contributors;

updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);

updated TPTP parser to conform to version 5.4.0; clarified abstract syntax for 'let' in TPTP_Syntax (and in the parser); improved parsing of 'let' (in TFF) -- previously it wasn't looking at the structure of the definition; fixed bug when parsing 'let' (in TFF and THF) -- was only keeping the first quantified variable, and ignoring the rest; added comments to remind that 'let' support for THF is currently broken in TPTP;

included axiom formulas (removing a FIXME) in the imported problem; turned tests into asserts; changed problem to one which actually succeeds using z3;

updated syntax to use 'ML_file' rather than 'uses';

now allowing numeric identifiers to be used in 'file' annotations; more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;

get_file_list now returns files sorted by size;

brought up to date with TPTP_Proof;

using richer annotation from formula annotations in proof;

extracting more info from formula annotation in proof;

corrected syntax filter;

reading tptp status code;

improved handling of nonstandard problem names;

merged

merged