semantic test of the MAIN-6 data (48 files, 1739 + 1059 boxes): 40800 (alpha, u) samples (40000 random, 800 on four extremisers for u across [U_LO, U_HI]); 5s
claims by the step of the proof that makes them: {'L0 TC+': 1249, 'L0 TC-': 57, 'L0 cut': 4, 'L1 A4': 1291, 'L1 TC+': 314, 'L1 TC-': 13, 'L1 TCS A4': 46, 'L1 TCS cut': 15, 'L1 cut': 351, 'L2 A5': 428, 'L2 TC+': 98, 'L2 TC-': 3, 'L2 TCS A5': 1019, 'L2 TCS cut': 55, 'L2 cut': 1, 'L3 TCS A6': 29, 'lpv': 18115, 'nobox': 17711, 'two': 1}
no claim (near-sphere test outside [q6, q5], or box file not yet delivered; gaps would be listed here): {'no box (file not delivered)': 17711, 'A4 outside [q6,q5]': 407, 'A5 outside [q6,q5]': 403}
smallest relative slack (T - E|L|)/T per step: {'L0 TC+': '6.589e-03', 'L0 TC-': '5.305e-02', 'L0 cut': '2.940e-02', 'L1 A4': '4.685e-08', 'L1 TC+': '5.440e-03', 'L1 TC-': '9.354e-02', 'L1 TCS A4': '1.947e-03', 'L1 TCS cut': '1.730e-02', 'L1 cut': '1.345e-02', 'L2 A5': '-5.046e-16', 'L2 TC+': '6.029e-03', 'L2 TC-': '6.349e-02', 'L2 TCS A5': '-5.048e-16', 'L2 TCS cut': '2.637e-02', 'L2 cut': '5.712e-02', 'L3 TCS A6': '2.289e-04', 'lpv': '6.625e-03', 'two': '4.491e-01'}
where the smallest slack of each near-sphere step occurs (u - u5, u6 - u, sorted |alpha_i| > 1e-3):
   L1 A4: slack 4.685e-08, u - u5 = 3.042e-07, u6 - u = 3.262e-01, |alpha| = [0.500174 0.500019 0.49991  0.499896]
   L1 TCS A4: slack 1.947e-03, u - u5 = 4.375e-05, u6 - u = 3.261e-01, |alpha| = [0.528377 0.527286 0.487027 0.453423]
   L2 A5: slack -5.046e-16, u - u5 = 5.729e-02, u6 - u = 2.689e-01, |alpha| = [0.447214 0.447214 0.447214 0.447214 0.447214]
   L2 TCS A5: slack -5.048e-16, u - u5 = 1.138e-02, u6 - u = 3.148e-01, |alpha| = [0.447214 0.447214 0.447214 0.447214 0.447214]
   L3 TCS A6: slack 2.289e-04, u - u5 = 3.220e-01, u6 - u = 4.204e-03, |alpha| = [0.409283 0.408793 0.408584 0.407945 0.407727 0.407152 0.001106]
violations: 0
RESULT: PASS (17711 samples fell in slabs whose files are not yet delivered)

real	0m4.905s
user	0m5.499s
sys	0m0.188s
