As an application of the theorem above, we can prove that $E_1\colon y^2=x^3-x$ has only finitely many rational solutions. Indeed, the discriminant of $E_1$ , $\Delta=64$ , is only divisible by $p=2$ , which is a prime of (bad) multiplicative reduction. Therefore $R_{E_1}=0$ . Moreover, the Nagell-Lutz theorem implies that the only torsion points on $E_1$ are those of order $2$ . Hence, the only rational points on $E_1$ are: $$\{ \mathcal{O}, (0,0),(1,0),(-1,0)\}.$$