Busy Beaver Equivalent for the Untyped Lambda Calculus In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus:

Over all terms in the ULC composed of n abstractions, variables and applications, which has the longest normal form?

This could be defined in a couple ways: we could consider only strongly normalizing ULC terms, or we could look for the longest normal form over all replacements.

Clearly, this function is not computable for arbitrarily large n, for the same reason as for the standard Busy Beaver function. However, I am interested in whether anything is known about this function for small values of n. What values is it known for? What bounds exists for higher n? For what n is the value known to be independent of ZFC?
Sequence https://oeis.org/A333479 in the On-Line Encyclopedia of Integer Sequences mostly answers your question. The question of shortest term for which lack of a normal form cannot be proven in ZFC remains open, but one candidate is the 213 bit Laver program presented in https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc