You are looking at historical revision 6719 of this page. It may differ significantly from its current revision.
This egg is for doing predicate calculus, to see whether a statement in predicate calculs is logically valid or not. The algorithm is guaranteed to terminate if the statement can be proven. The algorithm is resolution based.