We can now detect skolem escape and occurs-check and classify them as
insoluble, but because we don't do anything with irreducible
constraints (as of today) the tests still don't pass