Tseytin transformation example I am trying to understand Tseytin transformation and I can't really find any reliable info on the internet.
I pretty much understand the steps until I get to the point I have to convert all substitutions to CNF.
If I have this formula (wikipedia example)
$\phi :=((p\lor q)\land r)\to (\neg s)$
then substitued formula would be:
${T(\phi ):=(x1\leftrightarrow \neg s)\land (x2\leftrightarrow p\lor q) \land (x3\leftrightarrow x2\land r)\land (x4\leftrightarrow x3\to x1) \land x4}$
What I don't understand is, that when converting this to CNF, do I keep the new variables? Would the resulting formula in CNF be this?
${T(\phi ):=(p \lor q \lor \neg x1) \land (p \lor \neg q \lor x1) \land (\neg p \lor q \lor \neg x1) \land (\neg p \lor \neg q \lor \neg x1) \land (x1 \lor r \lor \neg x2) \land (x1 \lor \neg r \lor x2) \land (\neg x1 \lor r \lor \neg x2) \land (\neg x1 \lor \neg r \lor \neg x2) \land (s \lor \neg x3) \land (\neg s \lor x3) \land (x2 \lor x3 \lor \neg x4) \land (x2 \lor \neg x3 \lor x4) \land (\neg x2 \lor x3 \lor \neg x4) \land (\neg x2 \lor \neg x3 \lor \neg x4) \land x4}$
Is this final CNF formula? Don't I need to resolve introduced variables x(1..4) back to variables from original formula? 
 A: Your expression can be depicted as a logical circuit similar to this one:

The four new auxiliary variables help to directly derive the clauses of the CNF:

$x_1 = \lnot s$

$$(s \lor x_1) \land (\lnot s \lor \lnot x_1)$$

$x_2 = p \lor q$

$$(\lnot p \lor x_2) \land (\lnot q \lor x_2) \land (p \lor q \lor \lnot x_2)$$

$x_3 = r \land x_2$

$$(r \lor \lnot x_3) \land (x_2 \lor \lnot x_3) \land (\lnot r \lor \lnot x_2 \lor x_3)$$

$x_4 = x_1 \land \lnot x_3$

$$(x_1 \lor \lnot x_4) \land (\lnot x_3 \lor \lnot x_4) \land (\lnot x_1 \lor x_3 \lor x_4)$$
As witten in the question, the final clause to tie $\phi$ to true, just consists of the single literal $x_4$.
If you translate the CNF clauses in DIMACS format and feed this collection of clauses to a SAT solver, it will return either UNSAT (= no solution exists), UNKNOWN (= no solution found) or a number of solutions. Each solution assigns either true or false to any of the variables. As you are just interested in the primary input variables, you can ignore the assignments to the four switching variables.
Note:
For your example expression, Tseytin transformation does not really pay off. The expression can be expressed as CNF with just two clauses:
$$(\lnot p  \lor \lnot r  \lor \lnot s  \lor \lnot \phi) \land (\lnot q  \lor \lnot r  \lor \lnot s  \lor \lnot \phi)$$
