semantic test of the MAIN-5 data: 50600 (alpha, u) samples (50000 random, 600 on the three extremisers for u across [U_LO, U_HI]); 11s
claims by the step of the proof that makes them: {'A3': 2016, 'TC+': 1094, 'TC4S A5': 1492, 'TCN A4': 2323, 'TCN TC4+': 964, 'TCN TC4-': 9, 'TCN c1': 24, 'TCS A4': 2792, 'TCS c1': 383, 'c1': 294, 'cell': 2522, 'lpv': 36529, 'minus SG': 23, 'minus TC': 134, 'two': 1}
no claim (near-sphere test outside [q5, q4]; any gap would be listed here too): {'A5 outside': 544, 'A3 outside [q5,q4]': 643, 'A4 outside': 1176}
smallest relative slack (T - E|L|)/T per step: {'A3': '2.102e-08', 'TC+': '4.755e-03', 'TC4S A5': '3.752e-09', 'TCN A4': '-7.535e-16', 'TCN TC4+': '1.333e-03', 'TCN TC4-': '6.003e-02', 'TCN c1': '3.781e-02', 'TCS A4': '-8.779e-16', 'TCS c1': '2.099e-02', 'c1': '2.658e-03', 'cell': '6.342e-02', 'lpv': '2.954e-03', 'minus SG': '1.281e-01', 'minus TC': '8.493e-02', 'two': '6.900e-02'}
where the smallest slack of each near-sphere step occurs (u - u4, u5 - u, sorted |alpha_i| > 1e-3):
   A3: slack 2.102e-08, u - u4 = 8.937e-08, u5 - u = 3.682e-01, |alpha| = [0.577448 0.577368 0.577235]
   TC4S A5: slack 3.752e-09, u - u4 = 3.682e-01, u5 - u = 1.387e-08, |alpha| = [0.447257 0.44723  0.44722  0.447205 0.447157]
   TCN A4: slack -7.535e-16, u - u4 = 2.498e-01, u5 - u = 1.184e-01, |alpha| = [0.5 0.5 0.5 0.5]
   TCS A4: slack -8.779e-16, u - u4 = 1.998e-01, u5 - u = 1.684e-01, |alpha| = [0.5 0.5 0.5 0.5]
violations: 0
RESULT: PASS
