(A) phi satisfies all 45 inequalities; values of w = floor(excess(phi)): {-1: 10, 0: 33, 1: 2} (c = -w in the form R h <= c)
    inequalities that are tight at phi: 24
(B) the fifteen inequalities used in the proof (short diagonal | tips | inequality):
    ( 1) short (1, 1, 4) (0, 1, 5) | tips (1, 0, 5) (0, 2, 4) | +x >= 0
    ( 2) short (1, 2, 3) (0, 2, 4) | tips (1, 1, 4) (0, 3, 3) | +y -x >= 0
    ( 3) short (1, 3, 2) (0, 3, 3) | tips (1, 2, 3) (0, 4, 2) | +z -y >= 0
    ( 4) short (2, 4, 0) (1, 4, 1) | tips (2, 3, 1) (1, 5, 0) | +d -c >= 0
    ( 5) short (2, 3, 1) (1, 4, 1) | tips (2, 4, 0) (1, 3, 2) | +d +c -z >= 1
    ( 6) short (1, 0, 5) (0, 1, 5) | tips (1, 1, 4) (0, 0, 6) | -x >= 0
    ( 7) short (1, 1, 4) (0, 2, 4) | tips (1, 2, 3) (0, 1, 5) | +x -y >= 0
    ( 8) short (1, 2, 3) (0, 3, 3) | tips (1, 3, 2) (0, 2, 4) | +y -z >= 0
    ( 9) short (2, 3, 1) (1, 3, 2) | tips (2, 2, 2) (1, 4, 1) | +z +c -d -e >= 0
    (10) short (3, 1, 2) (2, 1, 3) | tips (3, 0, 3) (2, 2, 2) | +a +b -e >= 1
    (11) short (3, 2, 1) (2, 2, 2) | tips (3, 1, 2) (2, 3, 1) | +e +f -c -b >= -1
    (12) short (2, 4, 0) (2, 3, 1) | tips (3, 3, 0) (1, 4, 1) | +c -d >= 0
    (13) short (3, 1, 2) (3, 0, 3) | tips (4, 0, 2) (2, 1, 3) | +b -a >= 0
    (14) short (4, 2, 0) (4, 1, 1) | tips (5, 1, 0) (3, 2, 1) | +g -f >= 0
    (15) short (5, 1, 0) (5, 0, 1) | tips (6, 0, 0) (4, 1, 1) | -g >= 0
    1/2[(1)+(2)+(3)+(4)+(5)] reads  d >= 1/2;  1/2[(6)+(7)+(8)+(9)+(10)+(12)+(13)] + (11)+(14)+(15) reads  -d >= -1/2.
    Hence h[1,4,1] = 1/2 on P: P contains no integral point.
(C) 20 certificates verified: every coordinate of a point of P equals the coordinate of phi; P = {phi}.
(D) integer points of P with interior values in [-4,5]: 0 (search nodes: 190)
