It is further prohibited to use this Software or a substantial portion of it in a competition or a similar competetive event"
No thanks, you can keep your 150k lines of C++.
> The Licensee may not modify, disassemble, translate, reverse engineer, or decompile the Software.
Clearly proprietary software. I didn't expect that from something advertised in an academic looking PDF. Back to Coq or TLA+, I guess.
And actually in my experience with using the sledgehammer tool in Isabelle, Vampire does not fare very well when it comes to real world problems.
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.