The characteristic-two Gröbner basis conjecture for $\mathfrak{U}_{\mathbb{K}}(sl^+_n)$

Assume $p=2$ and $n\ge4$. For a sequence $i=(i_1,\dots,i_l)$, let $a_{i,k}=a_{i_1,k}\dots a_{i_l,k}$; write $i..j$ for the consecutive sequence from $i$ to $j$, and let $L_l[m]$ be the shifted set of permutations defined in the source. Characteristic-two Gröbner basis conjecture. The displayed union

$$\begin{aligned} &\left\{a_{ik}^2\mid 1\le i\le n-1,\ k\in\mathbb{N}_0\right\}\cup\left\{\sum_{i\in L_l[m]}a_{ik}^2\mid k\in\mathbb{N}_0,\ l+m\le n\right\}\\ &\cup\left\{[a_{i+m-1,k},a_{i..i+m,k}]+[a_{i+m-1,k},a_{i+m..i,k}]\mid 1\le i\le n-m-1,\ k\in\mathbb{N}_0\right\}\\ &\cup\left\{a_lb_k+b_ka_l+a_kb_ka_k\dots a_{l-1},\ b_la_k+a_kb_l+b_ka_kb_k\dots b_{l-1}\mid\right\} \end{aligned}$$

is a Gröbner basis of $\mathfrak{U}_{\mathbb{K}}(sl^+_n)$. The source presents this as a conjecture based on computer computations and gives no resolution evidence.