HeerHugo 0.3 is a propositional theorem prover that tries to prove (large) propositions a contradiction. Typical examples, in the syntax of HeerHugo are p&~p (contradiction), p|(q->(abcd<->s)) (satisfiable). The input is put in a file Ain, and the output is put in a file Aout. By adapting the file parameters.h a number of compile time options can be set, such as the maximum number of proposition letters (which has been set to over 150.000.000 for some experiments using an adapted version of HeerHugo). The tool (gzipped tar file) together with an accompanying paper (postscript or pdf) are available. The software can be used free of charge but it comes without any guarantee.
The proper reference to HeerHugo is: J.F. Groote and J.P. Warners. The propositional formula checker HeerHugo. Journal of Automated Reasoning, 24:101-125, 2000.
It is allowed to use HeerHugo for research purposes. If it is intended to use the code of HeerHugo version 0.3 for commercial purposes, which will not meet any objections from my side, it is important to know that the firm Logikkonsult NP AB (www.lk.se) claims that HeerHugo partly falls under Swedish Patent No. 467 076, U.S. Patent NO. 5 276 897 and European Patent No. 0403 454.