That's true. However, it might still be worthwhile given it appears to dominate competitions in many categories: https://web.archive.org/web/20190318010151/htt

That's true. However, it might still be worthwhile given it appears to dominate competitions in many categories: https://web.archive.org/web/20190318010151/http://tptp.cs.miami.edu/~tptp/CASC/ https://web.archive.org/web/20190318010151/http://tptp.cs.mi... As in, many people might be willing to get a license to get results some other prover weren't getting. It doesn't take a lot of complexity to choke one or explode its resource use.