theorem :: XPRIMES0:423

not 423 is prime