The `hardest´ natural decidable theory

Since mid-seventies it was an open problem as to whether there exist natural decidable theories requiring time (lower bound) exceeding any linearly growing towers of 2s to decide. It was conjectured that all natural decidable theories can be decided (upper bound) within time bounded by a tower of 2s growing linearly with the length of input. Although it happens to be true for the majority of non-elementary theories (Rabin's S2S, theory of term algebras, extended regular expressions, etc), the conjecture fails. We demonstrate that a modest fragment of L.Henkin's theory of propositional types (1963) has the tower of 2s growing *exponentially* with the length of input as a lower bound. This new unprecedentedly high lower bound allows us to considerably improve the known lower bounds and to settle the new ones for other theories