theorem :: XPRIMES0:801

not 801 is prime