The problem and axiom files are organized as follows:
benchmark/
README.md ... this file
lisp/ ... problem & axiom files in S-expression format
README.md ... about the S-expression format
axioms/ ... axiom files
problems/ ... problem files
chart/ ... problems from 'Chart-shiki' exercise books
univ/ ... problems from university entrance exams
imo/ ... problems from International Mathematical Olympiads
tptp/ ... problem and axiom files in TPTP THF format
README.md ... about the THF format encoding of the problems
axioms.ax ... the axiom file including all axioms and type definitions
problems/ ... problems in THF format
chart/ ... problems from 'Chart-shiki' exercise books
univ/ ... problems from university entrance exams
imo/ ... problems from International Mathematical Olympiads
to appear