Existence and termination of flips

Let $X$ be a $\mathbb{Q}$-factorial projective variety with only terminal singularities, and let $\varphi:X\rightarrow Y$ be a small contraction.

Flip conjecture. There exists a unique birational map $\phi:X\dashrightarrow X^+$ to a $\mathbb{Q}$-factorial projective variety $X^+$ with only terminal singularities, together with a small contraction $\varphi^+:X^+\rightarrow Y$, such that

$$\begin{array}{ccc} X & \dashrightarrow^{\phi} & X^+ \\ \downarrow\scriptstyle{\varphi} & & \downarrow\scriptstyle{\varphi^+} \\ & Y & \end{array}$$

is commutative and $K_{X^+}$ is $\varphi^+$-ample. The map $\phi$ is called the flip of $\varphi$. Moreover, there is no infinite sequence of flips.

This is the existence and termination assertion for flips in the minimal model program. The supplied text states it as a single conjectural package, but gives no evidence of its resolution; its status is therefore recorded as open.