In this paper, we consider the knowledge problems of deduction and static equivalence in the formal analysis of security protocols. We extend a recent result that developed a decision procedure for these problems in the non-disjoint combination \(R \cup E\) , where R is a subterm \(E\) -convergent term rewrite system (TRS) and \(E\) is a restricted form of permutative theory. Here, we consider the same combination problem but replace the subterm \(E\) -convergent TRS with a superclass of subterm \(E\) -convergent, called contracting \(E\) -convergent. We show that the previous decision procedure can be extended to obtain a new algorithm for this larger class of combined theories. We also explore the gap between the contracting TRSs, for which deduction and static-equivalence are decidable, and a larger superclass called graph-embedded for which these problems are undecidable. This gap is of interest since one would like to get closer to graph-embedded and still maintain decidability of the above “knowledge problems.” We show that at least one way of weakening the restrictions of the contracting definition will not work, as it leads to undecidability results for deduction and static equivalence. We also show that a subset of the graph-embedded rules is still sufficient to obtain undecidability.