theorem :: XPRIMES0:780

not 780 is prime