Are the existential fragment or the positive fragment of the theory of one-step rewriting decidable?

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

For a given signature $\Sigma$ and rewrite system $R$, the theory of one-step rewriting by $R$ is the first order theory of the model comprising all $\Sigma$-ground-terms, and the binary predicate \textit{$x$ rewrites to $y$ in one rewrite step of $R$}.

It is well-known that the full first-order theory is undecidable, even for strong restrictions on the class of rewrite systems (see RTALooP entry one-step-theory). Is the existential fragment of this theory (in other words: satisfiability of quantifier-free formulas) decidable? Is the positive fragment (arbitrary quantification, but no negation or implications) decidable?

It is known that the positive existential fragment is decidable [Treinen, 1996], and there are decidability results for the full existential fragment in case of restricted classes of rewrite systems [Treinen, 1996].