|Description:|| Devised by Konstantin Korovin, is a general purpose theorem prover for first-order logic based an
instantiation calculus Inst-Gen. It incorporates a QBF solving mode which
is based on a translation of QBF into the effectively propositional fragment
of first-order logic (EPR). The basic translation follows , and it is also
implemented a dedicated Skolemization procedure with several optimization.
 Seidl, M., Lonsing, F., Biere, A.: qbf2epr: A Tool for Generating EPR Formulas from QBF. PAAR@ IJCAR 21 (2012) 139–148