ayane v3.0.2

Theorem prover for first-order logic with equality.

Requires Java 13. A Linux version of OpenJDK (which is free, doesn't require an Oracle commercial license) can be obtained by following the steps at https://www.linuxuprising.com/2019/04/install-latest-openjdk-12-11-or-8-in.html except that after apt-add-repository it is also necessary to sudo apt-get update.

Ancillary scripts are in Python 3, though are not necessary to run the prover itself. If you do have Python, you can run build.py to generate a Unix or Windows shell script that provides a short command; the shell script contains the absolute path to the jar, so can be moved to any desired location.