theorem :: XPRIMES0:1253

not 1253 is prime