This is the GRUNGE benchmark for evaluating large-theory ATPs working in different formalisms - FOF, TF0, TF1, TH0 and TH1.
The benchmark is based on the HOL4 standard library - https://github.com/HOL-Theorem-Prover/HOL .
For details see https://arxiv.org/abs/1903.02539 :
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban: GRUNGE: A Grand Unified ATP Challenge. CADE 2019: 123-141
The HOL4 licence applies to all files.