4 ms·

"This license does not allow this Software to be used in a commercial context. Users wishing to use the Software in a commercial context should contact the copy

"This license does not allow this Software to be used in a commercial context. Users wishing to use the Software in a commercial context should contact the copyright holder for an alternative licence. 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++.

analognoise 8y ago
Thanks for saving me time!
nickpsecurity 8y ago
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.
1123581321 8y ago
Can you explain the last sentence? Are you saying it’s bad software, so it’s not worth paying for? Or is the commercial license generally frowned upon for an open source project?
- Soft 8y ago
  According to OSI [1], it is not open source if it cannot be used freely in commercial context. [1]: https://opensource.org/faq#commercial https://opensource.org/faq#commercial
loup-vaillant 8y ago
> The Licencee may not distribute the Software. > 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.
- grumdan 8y ago
  Just to give you a flavor of the way the main Vampire author does things: Until one or two years ago, not even a binary was freely available on the vampire website, and one had to contact them by email to ask for one; source code was definitely not distributed in any form.
- poizan42 8y ago
  You are mixing things up a bit, the alternatives you want are z3, cvc4, spass and e. Coq and TLA+ are proof assistents / formal specification languages, not smt solvers/theorem provers. 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.
  - loup-vaillant 8y ago
    Oh. Noted, thanks.

analognoise 8y ago

Thanks for saving me time!

nickpsecurity 8y ago

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.

1123581321 8y ago

Can you explain the last sentence? Are you saying it’s bad software, so it’s not worth paying for? Or is the commercial license generally frowned upon for an open source project?

Soft 8y ago
According to OSI [1], it is not open source if it cannot be used freely in commercial context. [1]: https://opensource.org/faq#commercial https://opensource.org/faq#commercial

loup-vaillant 8y ago

> The Licencee may not distribute the Software. > 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.

grumdan 8y ago
Just to give you a flavor of the way the main Vampire author does things: Until one or two years ago, not even a binary was freely available on the vampire website, and one had to contact them by email to ask for one; source code was definitely not distributed in any form.
poizan42 8y ago
You are mixing things up a bit, the alternatives you want are z3, cvc4, spass and e. Coq and TLA+ are proof assistents / formal specification languages, not smt solvers/theorem provers. 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.
- loup-vaillant 8y ago
  Oh. Noted, thanks.