Is there a notion of ``complete theory'' for which contextual deduction is complete for refutation of ground clauses?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

In [U. Reddy] a rewriting-like mechanism for clausal reasoning called contextual deduction'' was proposed. It specializes ordered resolution'' by using pattern matching in place of unification, only instantiating clauses to match existing clauses. Does contextual deduction always terminate? (In [U. Reddy] it was taken to be obvious, but that is not clear; see also [U. Reddy].) It was shown in [U. Reddy] that the mechanism is complete for refuting ground clauses using a theory that contains all its strong-ordered'' resolvents. Is there a notion of complete theory'' (like containing all strong-ordered resolvents not provable by contextual refutation) for which contextual deduction is complete for refutation of ground clauses?

Contextual deduction as defined in [U. Reddy] does not terminate. Bronsard and Reddy have gone on to solve this [U. Reddy] by using a more restricted, decidable mechanism. A completeness proof, incorporating equational inference with complete systems, is given in [U. Reddy].