files: 6  CPU seconds: 2456
stats: {'diagrams': 2400, 'oriented': 10294, 'multi': 8400, 'positive': 251, 'sharp0': 251, 'sharp1': 4480, 'mingap_nonpos': 2, 'sigmin': -10, 'sigmax': 10, 'maxcomp': 6, 'morton_eq': 10294, 'bracket_checked': 0}
    10294 checked, 0 failed : diagram is connected, reduced, alternating
    10294 checked, 0 failed : reduced alternating => A-adequate and B-adequate
    10294 checked, 0 failed : sA + sB = n + 2
    10294 checked, 0 failed : Goeritz signature: two colourings agree
    10294 checked, 0 failed : nullity 0 (non-split alternating)
    10294 checked, 0 failed : Lemma 4 (Traczyk): sigma = n+ - sA + 1 = sB - n- - 1
    10294 checked, 0 failed : MFW: w - s + 1 <= min deg_l P
    10294 checked, 0 failed : MFW: max deg_l P <= w + s - 1
    10294 checked, 0 failed : Lemma 2 (Morton): max deg_m P <= n - s + 1
    10294 checked, 0 failed : Lemma 1: min deg_t V >= min deg_l P - max deg_m P / 2
    10294 checked, 0 failed : Lemma 3 (KMT): min deg_t V = (3w - n - 2 sA + 2)/4
    10294 checked, 0 failed : (J): min deg_t V = sigma/2 - n-
    10294 checked, 0 failed : max deg_t V = sigma/2 + n+
    10294 checked, 0 failed : Lemma 5: sA = s + n- (mod 2), |sA - s| <= n-
    10043 checked, 0 failed : Lemma 5: n- >= 1 => sA <= s + n- - 2
    10294 checked, 0 failed : d_- integer >= 0, >= 1 if n- >= 1
    10294 checked, 0 failed : identity sigma - d_- = w - s + 1 + d_-
    10294 checked, 0 failed : THEOREM A: min deg_l P <= sigma - d_-
    10294 checked, 0 failed : mirror form: sigma + d_+ <= max deg_l P
    10294 checked, 0 failed : (I1): sigma >= min deg_l P
    10294 checked, 0 failed : equality in (I1) iff D positive
    10294 checked, 0 failed : d_- = s_+(D) - 1 (Ito's s_+), d_+ = s_-(D) - 1
    10294 checked, 0 failed : Ito Prop.1 + Traczyk: sigma = w - s + 2 s_+ - 1
    10294 checked, 0 failed : Kauffman-bound form of (I2): sigma - n- = w - sA + 1 <= min deg_l P
TOTAL FAILURES: 0
