CIRCUITSAT ∈ DTIME(2^n/n^c) ⟹ NP ≠ EXP? $\mathsf{EXP}\not\subseteq \mathsf{DTIME}(2^{n})$ and $\mathrm{CIRCUITSAT}\in \mathsf{DTIME}({2^{n}})$ holds and so why does $\mathsf{NP}\neq \mathsf{EXP}$ not hold while we know $\mathsf{NP}\subseteq \mathsf{DTIME}({2^{n}})\implies \mathsf{NP}\neq \mathsf{EXP}$?

Does $\mathrm{CIRCUITSAT}$ in any of $\mathsf{DTIME}(\frac{2^{n}}{n^c})$, $\mathsf{DTIME}({2^{\sqrt n}})$ or $\mathsf{DTIME}({2^{(\log n)^2}})$ $\implies \mathsf{NP}\neq \mathsf{EXP}$?
$\mathsf{CircuitSat\in DTIME(2^n)}$ does not imply $\mathsf{NP\subseteq DTIME(2^n)}$ since the reduction might increase the input's size. Suppose for example that $L\in NP$ and the reduction from $L$ to $\mathsf{CircuitSat}$ maps strings of length $n$ to strings of length $n^c$ (for all $n\in\mathbb{N}$), then applying the reduction and using a naive exponential time algorithm for circuit sat yields a $2^{n^c}$ time algorithm for $L$.

If however you can place an NP-complete problem in a subexponential time class, e.g. $n^{\log n}$, then $NP\neq EXP$, since $n^{O(\log n)}$ is closed under polynomial transformations, i.e. $n\mapsto n^c$.