CASC is the premier Automated Theorem Prover competition performed annually at the Conference on Automated Deduction (CADE). The 2017 event has finished on the 9th of August this year.
During this conference provers are faced with a set of problems and a time limit of 5 minutes (300 seconds) per problem. When the competition is over, the timings for each problem are taken to produce performance plots.
Here we see the results from the general first order formulas (FOF) division. 11 ATP systems participated, Vampire 4.2 was the winner in this division having solved over 450 problems from the set.
It is clear from this plot that the timings for each prover were independently sorted in increasing order and plotted over the same axes.
What is puzzling is the shape of the graph: for most provers most of the problems were really easy (solved within 50 seconds) and only a small proportion of problems were difficult yet solvable within the time limit (i.e. about 5% for Vampire 4.2 and less than 10% for Vampire 4.0, the 2016 winner). On the remaining problems (there were 500 problems altogether) the prover failed. Is there an intuitively simple explanation of why the difficulty distribution is so skewed towards "easy" problems not for one but for all provers?