<p>Answering this to get this question off the unanswered queue.</p>
<p>As mentioned in the related question linked, a simple automaton-based algorithm for answering first-order queries in Presburger arithmetic (and some extensions) has worst-case running time about 2↑↑n, where n is the number of quantifier alternations in the query. It has both been implemented and provides useful results. Find more about it <a href="https://arxiv.org/abs/1603.06017" rel="nofollow noreferrer">here</a></p>
Are there any algorithms that run in (2 ↑ ↑ n)?
<p>I’m wondering whether there are any algorithms that use so much time that they must be represented using <a href="https://en.wikipedia.org/wiki/Knuth%27s_up-arrow_notation" rel="nofollow noreferrer">Knuth up-arrow notation</a>.</p>

<p>Required: Use more than one up-arrow for time complexity.</p>

<p>Bonus points: </p>

<ul>
<li><p>Have the algorithm be useful.</p></li>
<li><p>Have the algorithm be useful and optimized</p></li>
</ul>

<p>Sister question on CS: (recommendation from @Amy)
<a href="https://cs.stackexchange.com/questions/94184/are-there-any-algorithms-that-run-in-2-">https://cs.stackexchange.com/questions/94184/are-there-any-algorithms-that-run-in-2-</a>↑-↑-n</p>