We present a new approach for goal-directed theorem 
proving with equality which integrates Basic Ordered 
Paramodulation into a Model Elimination framework.
In order to be able to use orderings and to restrict
the applications of equations to non-variable positions, 
the goal-directed tableau construction is combined with 
bottom-up completion where only positive literals are 
overlapped.  The resulting calculus thus keeps the best 
properties of completion while giving up only part of the 
goal-directedness.