Is the satisfiablity of ordering constraints (lpo) in conjunction with predicates like irreducibility by a fixed rewrite system or membership in a regular tree language decidable?

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

Satisfiability of ordering constraints (lpo) for total precedences has been shown decidable in [Hubert Comon, 1998]. Is the satisfiablity of total lpo ordering constraints together with the constraint $Irr(x)$, expressing that $x$ is not reducible by some fixed rewrite system, decidable? This would imply decidability of the confluence of ordered rewriting (see RTALooP entry ordered).

Besides the irreducibility predicate the following related predicates are of interest: \begin{itemize}

1. membership in a fixed regular tree language

2. a predicate expressing that a fixed symbol does not occur in a term. \end{itemize}