Is the extension of Combinatory Logic by Boolean constants confluent?

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

Consider the following extension of Combinatory Logic with constants $T$ (true), $F$ (false), $C$ (conditional):

$$\begin{aligned} Ix & \rightarrow & x\\ Kxy & \rightarrow & x\\ Sxyz & \rightarrow & (xz)(yz)\\ CTxy & \rightarrow & x\\ CFxy & \rightarrow & y\\ x \leftrightarrow^* y \Rightarrow Czxy & \rightarrow & x \end{aligned}$$

Is this (non-terminating) semi-equational'' (or natural'', as such are called in [Toyama, 1991]) conditional rewrite system confluent? Note that if we take the above system plus the rule $x \leftrightarrow^* y \Rightarrow Czxy \rightarrow y$, the resulting conditional rewrite system is confluent (cf. [Toyama, 1991]).