Let $\cal A$ be the (noncommutative) unitary $\mathbb Z$-algebra defined by three generators $a,b,c$ and four relations $a^2=a,b^2=b,c^2=c,(a+b+c)^2=a+b+c$. Is it true that $ab\neq 0$ in $A$ ?
This question is natural in the context of an older question here on MSE.
My thoughts : The following two relations follow easily from the axioms :
$$ \begin{array}{lcl} cb &=& -(ab+ac+ba+bc+ca) \\ cab &=& ca+ab+2(ba+ac+bc)+aba+abc+aca+bac+bca \\ \end{array}\tag{1} $$
Denote by $W$ the set of words on $a,b,c$ (they are called monomials in the algebra $\cal A$). We order $W$ with the shortlex $a<b<c$ ordering (which we denote by $\prec$). The two relations above express $cb$ or $cab$ in terms of $\prec$-smaller monomials. Iterating those two relations and using induction on $\prec$ ,any monomial can be transformed in $\cal A$ into a term whose monomials do not contain any of $aa,bb,cc,cb,cab$. Denote by $W'$ the set of all monomials satisfying this condition. We therefore have a surjection $s : {\cal A}' \to {\cal A}$ where ${\cal A}'=\oplus_{w\in W'} {\mathbb Z}w$.
Conjecture 1. The mapping $s$ is bijective, in other words $W'$ is a $\mathbb Z$-basis for $\cal A$.
Note that the action of $a$ or $b$ on $W'$ is trivial to describe : for any monomial $w\in W'$, if $w$ does not start with an $a$ then $aw$ stays in $W'$, and $aw=w$ otherwise. Similarly for $b$.
The action of $c$ is more complicated. Using the two relations in (1) and induction on $\prec$ again, we see that there is a unique $\mathbb Z$-linear map $C:{\cal A}' \to {\cal A}'$ such that $C(1)=c,C(a)=ca$ and
$$ \left\lbrace\begin{array}{lcl} C(abw) &=& (Ca+ab+2(ba+aC+bC)+aba+abC+aCa+baC+bCa)w \ ( \ \text{if} \ bw\in W') \\ C(acw) &=& cacw \ ( \ \text{if} \ acw\in W') \\ C(bw) &=& -(ab+aC+ba+bC+Ca)w \ ( \ \text{if} \ bw\in W') \\ C(cw) &=& cw \ ( \ \text{if} \ cw\in W') \end{array}\right.\tag{2} $$
Indeed, any monomial distinct from $1$ or $a$ starts with exactly one of $ab$, $ac$, $b$ or $c$. It is not clear however (at least to me) how to show that
Conjecture 1 (equivalent form). This $C$ satisfies $C^2=C$ and $(a+b+C)^2=a+b+C$.
Your Conjecture 1 is indeed true. It can be proved using diamond lemma techniques and the proof is sketched in Section 2.1 of the paper
Essentially, using the diamond lemma, it turns out to suffice to check that the two ways to reduce $ccab$ and $cabb$ using (either by first reducing $cc$ or $bb$, or by first using your identity for $cab$) are equal, and this is a straightforward computation.
(This answer was adapted from darij grinberg's comments on the question.)