2019-08-08 22:30:40 (GMT)
This preprint compares 14 provers for FO and HO logics on benchmarks obtained from HOL4. I didn't read the details but the result table shows that Zipperposition isn't too bad, and Leo 3 very versatile!
2019-08-09 8:26:0 (GMT)
I am very excited to see these benchmarks at CASC! In the paper, they provided exactly the axioms necessary to solve each problem. I wish they had used some kind of premise selection to create larger problems. But I suppose that's what we'll see at CASC Large Theory Batch division.