It doesn't aim to be a fully featured prover (like Prover9, E and others) but rather an "educational toy", to show a simple implementation of concepts practically used in automated reasoning (being written in one week for a course assignment).
Many things can be improved - for example, ProcessorTest needs a lot of refactoring.
The program can be started using the script teepee or executing the JAR file directly.
Note: on page 4 of the article the problems PLA001-1.p, PLA002-1.p and PLA003-1.p are reported to be satisfiable, which is wrong! I think that's because I considered only clauses marked as "negated conjecture" to belong to the set of support - indeed not using the set-of-support strategy (not using the -sos flag) correctly reports "unsatisfiable".
The archive with sources and binaries.
The JAR-only archive.
An introductory article (in Italian).
