Indeed, there is a closed form for this integral: $$I=\frac{\pi^2}3\ln^32-\frac25\ln^52+\frac{\pi^2}2\zeta(3)+\frac{99}{16}\zeta(5)-\frac{21}4\zeta(3)\ln^22\\-12\operatorname{Li}_4\left(\frac12\right)\ln2-12\operatorname{Li}_5\left(\frac12\right).$$

$$\frac{\pi^2}{24}-\frac{2\pi}3+\frac1{36\sqrt{2}}\left[5\pi^2+12\left(4+\ln\left(\frac{1+\sqrt2}2\right)\right)\left(\pi-2\ln\left(1+\sqrt2\right)\right)-48\operatorname{Li}_2\left(\sqrt2-1\right)\right]$$

Definitions $x\text{ is even} := \exists y[y+y=x]$ $x\text{ is odd} := \exists y[y+y+1=x]$ Axioms $\forall x[S(x) \ne 0]$ $\forall x \forall y[S(x)=S(y) \implies x=y]$ $\forall x[x+0=x]$ $\forall x \forall y[x+S(y)=S(x+y)]$ $[\varphi(0) \land [\forall x[\varphi(x) \implies \varphi(S(x))]]] ...