semantic test of the MAIN-6 data (105 files, 8107 + 1059 boxes): 40800 (alpha, u) samples (40000 random, 800 on four extremisers for u across [U_LO, U_HI]); 11s
claims by the step of the proof that makes them: {'L0 TC+': 3317, 'L0 TC-': 285, 'L0 cut': 34, 'L1 A4': 1590, 'L1 TC+': 1030, 'L1 TC-': 16, 'L1 TCS A4': 49, 'L1 TCS cut': 16, 'L1 cut': 403, 'L2 A5': 2222, 'L2 TC+': 446, 'L2 TC-': 4, 'L2 TCS A5': 1171, 'L2 TCS cut': 95, 'L2 cut': 3, 'L3 TCS A6': 975, 'lpv': 29143, 'two': 1}
no claim (near-sphere test outside [q6, q5], or box file not yet delivered; gaps would be listed here): {'A6 outside [q6,q5]': 373, 'A4 outside [q6,q5]': 407, 'A5 outside [q6,q5]': 794}
smallest relative slack (T - E|L|)/T per step: {'L0 TC+': '4.133e-03', 'L0 TC-': '4.973e-02', 'L0 cut': '2.940e-02', 'L1 A4': '4.685e-08', 'L1 TC+': '2.143e-03', 'L1 TC-': '7.944e-02', 'L1 TCS A4': '1.947e-03', 'L1 TCS cut': '1.730e-02', 'L1 cut': '1.291e-02', 'L2 A5': '-6.330e-16', 'L2 TC+': '1.367e-03', 'L2 TC-': '6.349e-02', 'L2 TCS A5': '-5.048e-16', 'L2 TCS cut': '1.481e-02', 'L2 cut': '3.404e-02', 'L3 TCS A6': '6.252e-09', '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 -6.330e-16, u - u5 = 2.934e-01, u6 - u = 3.279e-02, |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 6.252e-09, u - u5 = 3.262e-01, u6 - u = 3.962e-08, |alpha| = [0.408311 0.408261 0.408255 0.408254 0.408217 0.408192]
violations: 0
RESULT: PASS (0 samples fell in slabs whose files are not yet delivered)

real	0m11.469s
user	0m11.304s
sys	0m0.725s
DONE-K5SEM
