# Use Tseytin transformation to find $T(\phi)$, where $\phi\equiv¬(((P → Q) ∧ (Q → R)) → (P → R))$

Use Tseytin transformation to find $$T(\phi):$$ $$\phi\equiv¬(((P → Q) ∧ (Q → R)) → (P → R))$$

I did find an example on wiki for Tseytin transformation, and try to follow it to solve this, but not sure if this is right. Here is my attempts:

Consider $$\phi$$ as following, that have six subformulas:

$$\underbrace{¬\underbrace{(\underbrace{(\underbrace{(P → Q)}_{A} ∧ \underbrace{(Q → R)}_{B})}_{D} → \underbrace{(P → R)}_{C})}_{E}}_{F}$$

That $$T(\phi)$$ have seven clauses:

\begin{align} &A\leftrightarrow P → Q\\ \land&B\leftrightarrow Q → R\\ \land&C\leftrightarrow P → R\\ \land&D\leftrightarrow A\land B\\ \land&E\leftrightarrow D\to C\\ \land&F\leftrightarrow \neg E\\ \land&F\\ \end{align}

Transform each clause into CNF we have:

\begin{align} &(\neg P\lor Q\lor\neg A)\land(P\lor A)\land(\neg Q\lor A)\\ \land&(\neg Q\lor R\lor\neg B)\land(Q\lor B)\land(\neg R\lor B)\\ \land&(\neg P\lor R\lor\neg C)\land(P\lor C)\land(\neg R\lor C)\\ \land&(\neg A\lor\neg B\lor D)\land(A\lor\neg D)\land(B\lor\neg D)\\ \land&(\neg D\lor C\lor\neg E)\land(D\lor E)\land(\neg C\lor E)\\ \land&(E\lor\neg F)\land(\neg E\lor F)\\ \land&F\\ \end{align}

Could someone verify this, Thanks for your help.