Deciding the E+-class by an a posteriori, liftable order Original Research Article

We show that the E+-class can be decided by resolution using a liftable order, when the order is applied a posteriori. This is a surprising result, because the decision procedure for the E+-class was one of the motivations for the study of non-liftable orders. Also surprising is the behaviour of the resolution process. Initially the maximal depth at which a variable occurs can increase, but it will not increase more than a certain bound. We do not make use of any type of saturation rule in our resolution strategy.