Theorem proving with ordering and equality constrained clauses
scientific article; zbMATH DE number 792836