Given the current goal, possible generate (local and global) axioms.
Check whether the formulas in the given goal are satisfiable, and if yes generate a model.
Try to determine in which state a given goal is.
Apply this plugin to the given goal.
Check whether all inequalities present for the given constants are already implied by the type