Enter a pair of atomic formulas into the text-boxes below, and
click `Unify' to begin. Click each equation to apply the
corresponding transformation. Any term (except predicate/function
applications) starting with a capital is
considered to be a variable, anything else is a constant.

I haven't thoroughly tested the parser, so it may well behave...*erratically*. Particularly
if you start putting whitespace in odd places. I'll fix it up
eventually. In the meantime, let me know if anything goes
catastrophically awry.

I haven't thoroughly tested the parser, so it may well behave...