The immense success of SAT solvers motivates us to investigate solving of even harder decision problems. In this sense, Quantified Boolean Formula (QBFs) can be seen as a natural successor of SAT. QBFs, as a PSPACE-complete problem, provide us with a much stronger formalism but at the same time, represent a much more difficult computational challenge. In this talk we will look at QBF from both practical and theoretical perspective. First we will discuss an algorithm that solves QBF by a gradual expansion to SAT and invokes a SAT solver in a blackbox fashion. In the second part of the talk we will look at a calculus that corresponds to this solver and calculi that represent different existing solving techniques. We will show that these calculi can be exponentially separated while reusing some well-known results from circuit complexity.