-za pøidané formule). Velikost výsledné formule je polynomiální vùèi pùvodní:
-¾ádný literál (výskyt promìnné) pùvodní klauzule neduplikujeme, a v nejhor¹ím
-pøípadì zùstane ka¾dý pùvodní literál v klauzuli sám s nìjakými dvìma pøidanými
-(klauzule o tøech pøidaných mù¾eme vypustit) -- tedy poèet literálu se
-maximálnì ztrojnásobí.
+za pøidané formule). Velikost výsledné formule je tím pádem polynomiální vùèi pùvodní:
+v ka¾dém kroku se pøidají jen dva literály, tedy celkem {\it èas na pøevod}$\cdot
+2$ nových.
+
+\>Platí-li:
+\itemize\ibull
+\:$\alpha \Rightarrow$ zvolíme $x = 0$ (zajistí splnìní druhé poloviny nové formule),
+\:$\beta \Rightarrow$ zvolíme $x = 1$ (zajistí splnìní první poloviny nové formule),
+\:$\alpha ,\beta / \lnot\alpha ,\lnot\beta \Rightarrow$ zvolíme $x = 0/1$ (je nám to
+ jedno, celkové øe¹ení nám to neovlivní).
+\endlist