The resolution (and paramodulation) inference systems are 
theorem proving procedures for first-order logic (with 
equality), but they can run exponentially long for subclasses 
which have polynomial time decision procedures, as in the case 
of SLD resolution and the Knuth-Bendix completion procedure, 
both in the ground case.Specialized methods run in polynomial 
time, but have not been extended to the full first--order case.  
We show a form of Paramodulation which does not copy literals, 
which runs in polynomial time for the ground case of the 
following four subclasses: Horn Clauses with any selection 
rule, any set of Unit Equalities (this includes Completion),
Equational Horn Clauses with a certain selection rule, and 
Conditional Narrowing.