Are universality and inclusion of AC-recognizable languages decidable?

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

An AC-tree automaton as defined by [Ohsaki, 2002] is given by a signature $\Sigma$, a set of AC-axioms (that is, associativity and commutativity) for some function symbols of $\Sigma$, and a set of rewrite rules $R$ of the form

$$\begin{aligned} f(q_1,\ldots,q_n) & \rightarrow & q\\ f(q_1,\ldots,q_n) & \rightarrow & f(p_1,\ldots,p_n)\\ q & \rightarrow & p \end{aligned}$$

where the $q$'s and $p$'s are state symbols. Such an automaton accepts a term $t$ iff it rewrites $t$ modulo the given AC-axioms to some final state. $L(A)$ denotes the language recognized by an AC-tree automaton $A$; a language $L$ is called AC-recognizable iff $L=L(A)$ for some AC-tree automaton $A$.

Are the following questions decidable? \begin{itemize}

1. Universality: Given an AC-tree automaton $A$, is $L(A)$ equal to the set of all ground terms over the given signature $\Sigma$?

2. Inclusion: Given AC-tree automata $A$ and $B$, is $L(A)$ a subset of $L(B)$? \end{itemize}

It has been shown [Ohsaki, 2002] that emptiness of AC-recognizable languages is decidable. Furthermore, as a consequence of the results of [Ohsaki, 2002], universality and inclusion are decidable if transition rules of the form $f(q_1,\ldots,q_n) \rightarrow f(p_1,\ldots,p_n)$ are not allowed (this is the sub-class of so-called regular AC tree-automata). However, both questions are still open in the general case.

Recorded progress.

The inclusion problem of AC-tree automata is undecidable~[Ohsaki, 2002]. Decidability of universality is still an open question.