Does natural deduction scale beyond first-order propositional logic with a small number of variables? It seems to me that it would have bad exponential blowup, checking all the cases.