Is a certain conditional rewrite system, which is a linearization of Combinatory Logic extended with surjective pairing, confluent?

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

Is the following semi-equational conditional term rewriting system (a linearization of Combinatory Logic extended with surjective pairing) confluent:

$$\begin{aligned} Ix & \rightarrow & x\\ Kxy & \rightarrow & x\\ Sxyz & \rightarrow & (xz)(yz)\\ D_{1}(Dxy) & \rightarrow & x\\ D_{2}(Dxy) & \rightarrow & y\\ x \leftrightarrow^* y \Rightarrow D(D_{1}x)(D_{2}y)& \rightarrow & x\\ x \leftrightarrow^* y \Rightarrow D(D_{1}x)(D_{2}y)& \rightarrow &y \end{aligned}$$

If yes, does an effective normal form strategy exist for it? See [Vrijer, 1991].