theorem :: XPRIMES0:129

not 129 is prime