80 = (2 |^ 4) * (5 |^ 1) by Lm5;
hence not 79 satisfies_Sierpinski_problem_105 by XPRIMES1:2, XPRIMES1:5; :: thesis: verum