Decoding the $E^+$-Class by an A Posteriori, Liftable Order
Hans de Nivelle

Abstract:
We show that the $E^+$­class can be decided by a liftable order, when it is
applied a posteriori. This is a surprising result, because 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 variable depth of
the clauses may grow, but it will not grow deeper than a certain bound.
We do not make use of any type of saturation rule in our completeness proof.