r2_literal.py -- independent verification run 2, OWR-14299911-020 (literal brute force)
[L1-L4] products of trees: metric, Lemma 2.1, Lemma 2.3, Proposition 2.4, Lemma 2.6(a)
    P6                         |V|=  6  polytopes=  21 (= products of subtrees)  steps=   30  triples=  1152  (0.0 s)
    K1,5                       |V|=  6  polytopes=  37 (= products of subtrees)  steps=   85  triples=  1152  (0.0 s)
    spider(3,2,1)              |V|=  7  polytopes=  34 (= products of subtrees)  steps=   60  triples=  1911  (0.0 s)
    K1,3 x P3                  |V|= 12  polytopes=  66 (= products of subtrees)  steps=  156  triples= 12816  (0.1 s)
    P2 x spider(2,1,1)         |V|= 10  polytopes=  51 (= products of subtrees)  steps=  112  triples=  6600  (0.1 s)
    P2^4                       |V|= 16  polytopes=  81 (= products of subtrees)  steps=  216  triples= 37632  (0.5 s)
    K1,3 x P4                  |V|= 16  polytopes= 110 (= products of subtrees)  steps=  282  triples= 37632  (0.5 s)
    P5 x P3                    |V|= 15  polytopes=  90 (= products of subtrees)  steps=  210  triples= 29475  (0.4 s)
    rtree6 x K1,2              |V|= 18  polytopes= 180 (= products of subtrees)  steps=  534  triples= 21744  (0.8 s)
    P7 x K1,4                  |V|= 35  polytopes= 560 (= products of subtrees)  steps= 1848  triples= 42280  (3.3 s)
    spider(3,3) x K1,3 x P2    |V|= 56  polytopes= 924 (= products of subtrees)  steps= 3262  triples= 67648  (6.3 s)
    P4 x P4 x K1,2             |V|= 48  polytopes= 600 (= products of subtrees)  steps= 2040  triples= 57984  (4.2 s)
    rtree8 x K1,3              |V|= 32  polytopes= 891 (= products of subtrees)  steps= 3580  triples= 38656  (4.8 s)
    P6 x K1,3 x P2             |V|= 48  polytopes= 693 (= products of subtrees)  steps= 2397  triples= 57984  (5.4 s)
    spider(2,2,2) x K1,5       |V|= 42  polytopes=1332 (= products of subtrees)  steps= 5502  triples= 50736  (7.1 s)
    total triples for Proposition 2.4: 465402; control "TP = hyp" fails on 465117 of them
[L5] Lemma 2.6(a), TP <= 2 TS, in graphs that are not median (literal TP)
    C5         |V|= 5 polytopes= 16 triples=  400  max TP/TS=2.000  (median: no)
    C6         |V|= 6 polytopes= 19 triples=  792  max TP/TS=2.000  (median: no)
    C7         |V|= 7 polytopes= 29 triples= 1421  max TP/TS=2.000  (median: no)
    K2,3       |V|= 5 polytopes= 12 triples=  400  max TP/TS=2.000  (median: no)
    K4         |V|= 4 polytopes= 15 triples=  176  max TP/TS=2.000  (median: no)
    Petersen   |V|=10 polytopes= 78 triples= 5600  max TP/TS=2.000  (median: no)
    G(8,0.3)   |V|= 8 polytopes= 42 triples= 2368  max TP/TS=2.000  (median: no)
[L6] Remark 2.5 (Genevois): TP = 2 #(DW classes separating two points) in median graphs that are not products of trees
    L-shape(3 squares)       |V|= 8 median,  4 hyperplanes, polytopes=  31, triples=  3648: TP = 2 #DW: OK
    T-shape(5 squares)       |V|=12 median,  6 hyperplanes, polytopes=  71, triples= 14256: TP = 2 #DW: OK
    squares-at-vertex(3)     |V|=10 median,  6 hyperplanes, polytopes=  79, triples=  7600: TP = 2 #DW: OK
    Q3 + square on an edge   |V|=10 median,  4 hyperplanes, polytopes=  42, triples=  7600: TP = 2 #DW: OK
    two squares + path       |V|= 9 median,  6 hyperplanes, polytopes=  49, triples=  5346: TP = 2 #DW: OK
[L7] Section 6, upper bound: the family of Proposition 4.1 on non-convex geodesic segments
    d=1,n=3 in P3xP3           segments convex: [False]  |F|= 3  literal TP= 4 = 2d(n-1)L= 4  TS= 4 >= (N-1)L= 2
    d=1,n=5 in P3xP3           segments convex: [False]  |F|= 5  literal TP= 8 = 2d(n-1)L= 8  TS= 8 >= (N-1)L= 4
    d=2,n=2 ladder x ladder    segments convex: [False, False]  |F|= 4  literal TP= 8 = 2d(n-1)L= 8  TS= 8 >= (N-1)L= 6
    d=2,n=2 ladder x P3        segments convex: [False, True]  |F|= 4  literal TP= 8 = 2d(n-1)L= 8  TS= 8 >= (N-1)L= 6
[L8] Proposition 4.1 with k < d: the family in the k long factors, extra factors of small diameter (literal TP)
    k=1 n=3 in P3 x K1,3              |V|=12 polytopes= 66  |F|=3  literal TP= 4 = 2k(n-1)L  TS= 4  bounds: True
    k=1 n=5 in P5 x P2 x K1,2         |V|=30 polytopes=270  |F|=5  literal TP= 8 = 2k(n-1)L  TS= 8  bounds: True
    k=2 n=2 in P3 x P3 x K1,3         |V|=36 polytopes=396  |F|=4  literal TP= 8 = 2k(n-1)L  TS= 8  bounds: True
    k=2 n=2 in spider(2, 1) x P3 x P2 |V|=24 polytopes=180  |F|=4  literal TP= 8 = 2k(n-1)L  TS= 8  bounds: True
[C] negative controls
    reading "u any vertex": max TP(x,{},y) on P3 x P3 = 2 (<= 2, so TP(X) would be 0); diameter = 4
    Held-Karp TS = brute force over permutations on 300 triples; a corrupted TS differs on 253 of them
TOTAL: 1059061 checks, 0 failures (running time 34.1 s)
ALL CHECKS PASSED
