Optional use of quantifiers in unification, no quantifier failures for normalization. Fixes in unify.
Print Report and Contradiction exceptions. Show sort of unnamed variables.
More tests. Test results are not yet checked (just demonstrate what is produced).
Error reporting fix, milestone update.