The [Fabius function](http://en.wikipedia.org/wiki/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$$

[![Fabius graph][1]][1]

The function $F$ assumes rational values at [dyadic rational](http://en.wikipedia.org/wiki/Dyadic_rational) arguments. In particular, it is known [$\!^{[1]}$](http://web.archive.org/web/20170207221142/http://1130caca0d7b5a4061c64d8e3b4a4e1d.2368764.n4.nabble.com/file/n2/Rvachev.pdf)[$\!^{[2]}$](http://arxiv.org/abs/1609.07999) 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)(2n+1)} \, \sum_{m=0}^{n-1} \binom{2n+1}{2m} \, c_m.\tag4$$
The values $F\left(2^{-n}\right) $ appear as [A272755](http://oeis.org/A272755) / [A272757](http://oeis.org/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](https://gist.githubusercontent.com/VladimirReshetnikov/2d439ecfcc8ff23367d4a0b4a47a4a86/raw/997900be2c083bf4f87d4ab903982dc05d263b9b/gistfile1.txt))_

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

  [1]: https://i.sstatic.net/RGqBP.png