[例 １０: 4 < |S|]

4 < |S| においても、S の数字のラベルを適切に貼り替えれば
□(0123) が言えます。

よって 4 < |S| なる S は T = {0, 1, 2, 3} 上の三角乗法系を
部分系として含みます。

いま {0, 1, 2, 3} 以外の数 4 をとり
△(04a) ＞→ b を考えると、a = {1, 2, 3} の３つの選び方それぞれに
対して {0, 1, 2, 3, 4} と異なる数 b_a が必要です。
それらを b = {5, 6, 7} とすると S の基数は最低でも 8 <= |S| 必要なことが分かります。

実際は |S| = 8 に三角乗法が定義できます。
上の考察から □(0145)、□(0246)、□(0347) と定義し
△(124) ＞→ 7、△(134) ＞→ 6、△(234) ＞→ 5 を導きます。
さらに □(0167)、□(0257)、□(0356)、□(1256)、□(1357)、□(2367) が導けます。
最後に □(4567) を追加して定義を完成します。

この定義が結合法則 >>59 および頂点を保つ縮約公理 >>60 と
矛盾しないことはコンピュータにより確かめました。

コンピュータさんは |S| = 8 だとしばし考え込む感じです。
まあ私のプログラムが効率等あまり考えないヘボなのも原因ですが。
しかし結合法則 >>59 より (a, b, c, x, y, z) 〜 n^6 の
６重ループを本質的には回さなければならない（と思う）ので
これは時間がかかっても仕方ないと思われます。

とくに次の |S| = 16 だと 64 倍以上も時間がかかってしまうので
より効率の良い無矛盾性チェックのアルゴリズムがあるといいなあ。