The Fabius function is a smooth monotone function $F:[0,1]\to[0,1]$, satisfying functional equations $$F(0)=0, \quad F(1-x)=1-F(x)\tag1$$ and $$F'(x) = 2 \,F(2 x) \quad \text{for} \,\, 0<x<1/2.\tag2$$

The function $F$ assumes rational values at dyadic rational arguments. In particular, it is known $\!^{[1]}$$\!^{[2]}$ that $$F\left(2^{-n}\right) = \frac1{2^{\binom{n+1}2}} \, \sum_{m=0}^{\lfloor n/2\rfloor}\binom n {2m} \, c_m,\tag3$$ where $c_m$ are defined by the recurrence $$c_0 = 1, \quad c_n = \frac1{4^n - 1} \, \sum_{m=0}^{n-1} \binom{2n}{2m} \, \frac{c_m}{2 n - 2 m + 1}.\tag4$$ The values $F\left(2^{-n}\right) $ appear as A272755 / A272757 in the OEIS.

Let $$a_n = F\left(2^{-n}\right) \, 2^{\binom {n-1}2} \, (2n)! \, \prod_{m=1}^{\lfloor n/2\rfloor}\left(4^m - 1\right).\tag5$$ This sequence begins $$1, \, 5, \, 15, \, 1001, \, 5985, \, 2853675, \, 26261235, \, 72808620885, \, 915304354965 \, ...\tag6$$ (see more terms here)

I conjecture that all terms of this sequence are integers. How can we prove (disprove) this conjecture?